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.descent-data-pushouts where
Imports
open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.span-diagrams open import foundation.transport-along-identifications open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans
Idea
Descent data¶
for the pushout of a
span diagram 𝒮
f g
A <-- S --> B
is a triple (PA, PB, PS)
, where PA : A → 𝒰
is a type family over A
,
PB : B → 𝒰
is a type family over B
, and PS
is a family of
equivalences
PS : (s : S) → PA (f a) ≃ PB (g a).
In
descent-property-pushouts
,
we show that this is exactly the data one needs to "glue together" a type family
P : X → 𝒰
over the pushout X
of 𝒮
.
The identity type of descent data is
characterized in
equivalences-descent-data-pushouts
.
It may not be immediately clear why "descent data" is an appropriate name for
this concept, because there is no apparent downward motion. Traditionally,
descent is studied in the context of a collection of objects Xᵢ
covering a
single object X
, and local structure on the individual Xᵢ
's descending onto
X
, collecting into a global structure, given that the pieces are appropriately
compatible on any "overlaps". A pushout of 𝒮
is covered by A
and B
, and
the overlaps are encoded in f
and g
. Then structure on A
and B
,
expressed as type families PA
and PB
, "descends" to a structure on X
(a
type family over X
). Two elements "overlap" in X
if there is an
identification between them coming from S
, and the gluing/compatibility
condition exactly requires the local structure of PA
and PB
to agree on such
elements, i.e. asks for an equivalence PA(fs) ≃ PB(gs)
.
Definitions
Descent data for pushouts
module _ {l1 l2 l3 : Level} (𝒮 : span-diagram l1 l2 l3) where descent-data-pushout : (l4 : Level) → UU (l1 ⊔ l2 ⊔ l3 ⊔ lsuc l4) descent-data-pushout l = Σ ( domain-span-diagram 𝒮 → UU l) ( λ PA → Σ ( codomain-span-diagram 𝒮 → UU l) ( λ PB → (s : spanning-type-span-diagram 𝒮) → PA (left-map-span-diagram 𝒮 s) ≃ PB (right-map-span-diagram 𝒮 s)))
Components of descent data for pushouts
module _ {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} (P : descent-data-pushout 𝒮 l4) where left-family-descent-data-pushout : domain-span-diagram 𝒮 → UU l4 left-family-descent-data-pushout = pr1 P right-family-descent-data-pushout : codomain-span-diagram 𝒮 → UU l4 right-family-descent-data-pushout = pr1 (pr2 P) equiv-family-descent-data-pushout : (s : spanning-type-span-diagram 𝒮) → left-family-descent-data-pushout (left-map-span-diagram 𝒮 s) ≃ right-family-descent-data-pushout (right-map-span-diagram 𝒮 s) equiv-family-descent-data-pushout = pr2 (pr2 P) map-family-descent-data-pushout : (s : spanning-type-span-diagram 𝒮) → left-family-descent-data-pushout (left-map-span-diagram 𝒮 s) → right-family-descent-data-pushout (right-map-span-diagram 𝒮 s) map-family-descent-data-pushout s = map-equiv (equiv-family-descent-data-pushout s) is-equiv-map-family-descent-data-pushout : (s : spanning-type-span-diagram 𝒮) → is-equiv (map-family-descent-data-pushout s) is-equiv-map-family-descent-data-pushout s = is-equiv-map-equiv (equiv-family-descent-data-pushout s)
Descent data induced by families over cocones
Given a cocone
g
S -----> B
| |
f | | j
∨ ∨
A -----> X
i
and a family P : X → 𝒰
, we can obtain PA
and PB
by precomposing with i
and j
, respectively. Then to produce an equivalence
PS s : P (ifs) ≃ P (jgs)
, we
transport along the
coherence H s : ifs = jgs
, which is an equivalence.
module _ {l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3} {X : UU l4} (c : cocone-span-diagram 𝒮 X) where descent-data-family-cocone-span-diagram : {l5 : Level} → (X → UU l5) → descent-data-pushout 𝒮 l5 pr1 (descent-data-family-cocone-span-diagram P) = P ∘ horizontal-map-cocone _ _ c pr1 (pr2 (descent-data-family-cocone-span-diagram P)) = P ∘ vertical-map-cocone _ _ c pr2 (pr2 (descent-data-family-cocone-span-diagram P)) s = equiv-tr P (coherence-square-cocone _ _ c s)
Recent changes
- 2024-05-31. Vojtěch Štěpančík. Refactor the descent property of pushouts (#1145).