Morphisms of descent data for pushouts
Content created by Vojtěch Štěpančík.
Created on 2024-05-31.
Last modified on 2024-05-31.
module synthetic-homotopy-theory.morphisms-descent-data-pushouts where
Imports
open import foundation.commuting-squares-of-homotopies open import foundation.commuting-squares-of-maps open import foundation.dependent-pair-types open import foundation.equality-dependent-function-types open import foundation.equivalences open import foundation.function-types open import foundation.fundamental-theorem-of-identity-types open import foundation.homotopies open import foundation.homotopy-induction open import foundation.identity-types open import foundation.span-diagrams open import foundation.structure-identity-principle open import foundation.torsorial-type-families open import foundation.universe-levels open import foundation.whiskering-homotopies-composition open import synthetic-homotopy-theory.descent-data-pushouts
Idea
Given descent data for
pushouts (PA, PB, PS) and
(QA, QB, QS), a
morphism¶
between them is a pair of fiberwise maps
hA : (a : A) → PA a → QA a
hB : (b : B) → PB b → QB b
equipped with a family of homotopies making
hA(fs)
PA(fs) --------> QA(fs)
| |
PS s | | QS s
| |
∨ ∨
PB(gs) --------> QB(gs)
hB(gs)
commute for every s : S.
For any two morphisms (hA, hB, hS) and (kA, kB, kS), we can define the type
of
homotopies¶
between them as the type of triples (HA, HB, HS), where HA and HB are
fiberwise homotopies
HA : (a : A) → hA a ~ kA a
HB : (b : B) → hB b ~ kB b,
and HS is a coherence datum showing that for all s : S, the square of
homotopies
HB(gs) ·r PS s
hB(gs) ∘ PS s ---------------> kB(gs) ∘ PS s
| |
hS s | | tS s
| |
∨ ∨
QS s ∘ hA(fs) ---------------> QS s ∘ kA(fs)
QS s ·l HA(fs)
commutes. This coherence
datum may be seen as a filler of the diagram one gets by gluing the squares hS
and tS along the common vertical maps
tA(fs)
________
/ ∨
PA(fs) QA(fs)
| \________∧ |
| hA(fs) |
| |
PS s | | QS s
| tB(gs) |
| ________ |
∨ / ∨ ∨
PB(gs) QB(gs).
\________∧
hB(gs)
The front and back faces are hS s and tS s, and the top and bottom faces are
HA(fs) and HB(gs), respectively. HS then expresses that going along the
front face and then the top face is homotopic to first going along the bottom
face and then the back face.
We then show that homotopies characterize the identity types of morphisms of descent data.
Definitions
Morphisms of descent data for pushouts
Note that the descent data arguments cannot be inferred when calling
left-map-hom-descent-data-pushout and the like, since Agda cannot infer the
proofs of is-equiv of their gluing maps.
module _ {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} (P : descent-data-pushout 𝒮 l4) (Q : descent-data-pushout 𝒮 l5) where hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) hom-descent-data-pushout = Σ ( (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a → left-family-descent-data-pushout Q a) ( λ hA → Σ ( (b : codomain-span-diagram 𝒮) → right-family-descent-data-pushout P b → right-family-descent-data-pushout Q b) ( λ hB → (s : spanning-type-span-diagram 𝒮) → coherence-square-maps ( hA (left-map-span-diagram 𝒮 s)) ( map-family-descent-data-pushout P s) ( map-family-descent-data-pushout Q s) ( hB (right-map-span-diagram 𝒮 s)))) module _ (h : hom-descent-data-pushout) where left-map-hom-descent-data-pushout : (a : domain-span-diagram 𝒮) → left-family-descent-data-pushout P a → left-family-descent-data-pushout Q a left-map-hom-descent-data-pushout = pr1 h right-map-hom-descent-data-pushout : (b : codomain-span-diagram 𝒮) → right-family-descent-data-pushout P b → right-family-descent-data-pushout Q b right-map-hom-descent-data-pushout = pr1 (pr2 h) coherence-hom-descent-data-pushout : (s : spanning-type-span-diagram 𝒮) → coherence-square-maps ( left-map-hom-descent-data-pushout (left-map-span-diagram 𝒮 s)) ( map-family-descent-data-pushout P s) ( map-family-descent-data-pushout Q s) ( right-map-hom-descent-data-pushout (right-map-span-diagram 𝒮 s)) coherence-hom-descent-data-pushout = pr2 (pr2 h)
The identity morphism of descent data for pushouts
module _ {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} (P : descent-data-pushout 𝒮 l4) where id-hom-descent-data-pushout : hom-descent-data-pushout P P pr1 id-hom-descent-data-pushout a = id pr1 (pr2 id-hom-descent-data-pushout) b = id pr2 (pr2 id-hom-descent-data-pushout) s = refl-htpy
Composition of morphisms of descent data for pushouts
module _ {l1 l2 l3 l4 l5 l6 : Level} {𝒮 : span-diagram l1 l2 l3} (P : descent-data-pushout 𝒮 l4) (Q : descent-data-pushout 𝒮 l5) (R : descent-data-pushout 𝒮 l6) (g : hom-descent-data-pushout Q R) (f : hom-descent-data-pushout P Q) where comp-hom-descent-data-pushout : hom-descent-data-pushout P R pr1 comp-hom-descent-data-pushout a = left-map-hom-descent-data-pushout Q R g a ∘ left-map-hom-descent-data-pushout P Q f a pr1 (pr2 comp-hom-descent-data-pushout) b = right-map-hom-descent-data-pushout Q R g b ∘ right-map-hom-descent-data-pushout P Q f b pr2 (pr2 comp-hom-descent-data-pushout) s = pasting-horizontal-coherence-square-maps ( left-map-hom-descent-data-pushout P Q f ( left-map-span-diagram 𝒮 s)) ( left-map-hom-descent-data-pushout Q R g ( left-map-span-diagram 𝒮 s)) ( map-family-descent-data-pushout P s) ( map-family-descent-data-pushout Q s) ( map-family-descent-data-pushout R s) ( right-map-hom-descent-data-pushout P Q f ( right-map-span-diagram 𝒮 s)) ( right-map-hom-descent-data-pushout Q R g ( right-map-span-diagram 𝒮 s)) ( coherence-hom-descent-data-pushout P Q f s) ( coherence-hom-descent-data-pushout Q R g s)
Homotopies between morphisms of descent data for pushouts
module _ {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} (P : descent-data-pushout 𝒮 l4) (Q : descent-data-pushout 𝒮 l5) (f g : hom-descent-data-pushout P Q) where htpy-hom-descent-data-pushout : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) htpy-hom-descent-data-pushout = Σ ( (a : domain-span-diagram 𝒮) → left-map-hom-descent-data-pushout P Q f a ~ left-map-hom-descent-data-pushout P Q g a) ( λ HA → Σ ( (b : codomain-span-diagram 𝒮) → right-map-hom-descent-data-pushout P Q f b ~ right-map-hom-descent-data-pushout P Q g b) ( λ HB → (s : spanning-type-span-diagram 𝒮) → coherence-square-homotopies ( ( HB (right-map-span-diagram 𝒮 s)) ·r ( map-family-descent-data-pushout P s)) ( coherence-hom-descent-data-pushout P Q f s) ( coherence-hom-descent-data-pushout P Q g s) ( ( map-family-descent-data-pushout Q s) ·l ( HA (left-map-span-diagram 𝒮 s)))))
The reflexive homotopy between morphisms of descent data for pushouts
module _ {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} (P : descent-data-pushout 𝒮 l4) (Q : descent-data-pushout 𝒮 l5) (f : hom-descent-data-pushout P Q) where refl-htpy-hom-descent-data-pushout : htpy-hom-descent-data-pushout P Q f f pr1 refl-htpy-hom-descent-data-pushout a = refl-htpy pr1 (pr2 refl-htpy-hom-descent-data-pushout) b = refl-htpy pr2 (pr2 refl-htpy-hom-descent-data-pushout) s = right-unit-htpy
Properties
Characterizing the identity type of morphisms of descent data for pushouts
module _ {l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3} (P : descent-data-pushout 𝒮 l4) (Q : descent-data-pushout 𝒮 l5) (f : hom-descent-data-pushout P Q) where htpy-eq-hom-descent-data-pushout : (g : hom-descent-data-pushout P Q) → (f ＝ g) → htpy-hom-descent-data-pushout P Q f g htpy-eq-hom-descent-data-pushout .f refl = refl-htpy-hom-descent-data-pushout P Q f abstract is-torsorial-htpy-hom-descent-data-pushout : is-torsorial (htpy-hom-descent-data-pushout P Q f) is-torsorial-htpy-hom-descent-data-pushout = is-torsorial-Eq-structure ( is-torsorial-Eq-Π ( λ a → is-torsorial-htpy (left-map-hom-descent-data-pushout P Q f a))) ( left-map-hom-descent-data-pushout P Q f , λ a → refl-htpy) ( is-torsorial-Eq-structure ( is-torsorial-Eq-Π ( λ b → is-torsorial-htpy (right-map-hom-descent-data-pushout P Q f b))) ( right-map-hom-descent-data-pushout P Q f , λ b → refl-htpy) ( is-torsorial-Eq-Π ( λ s → is-torsorial-htpy ( coherence-hom-descent-data-pushout P Q f s ∙h refl-htpy)))) is-equiv-htpy-eq-hom-descent-data-pushout : (g : hom-descent-data-pushout P Q) → is-equiv (htpy-eq-hom-descent-data-pushout g) is-equiv-htpy-eq-hom-descent-data-pushout = fundamental-theorem-id ( is-torsorial-htpy-hom-descent-data-pushout) ( htpy-eq-hom-descent-data-pushout) extensionality-hom-descent-data-pushout : (g : hom-descent-data-pushout P Q) → (f ＝ g) ≃ htpy-hom-descent-data-pushout P Q f g pr1 (extensionality-hom-descent-data-pushout g) = htpy-eq-hom-descent-data-pushout g pr2 (extensionality-hom-descent-data-pushout g) = is-equiv-htpy-eq-hom-descent-data-pushout g eq-htpy-hom-descent-data-pushout : (g : hom-descent-data-pushout P Q) → htpy-hom-descent-data-pushout P Q f g → f ＝ g eq-htpy-hom-descent-data-pushout g = map-inv-equiv (extensionality-hom-descent-data-pushout g)
Recent changes
- 2024-05-31. Vojtěch Štěpančík. Refactor the descent property of pushouts (#1145).