The flattening lemma for pushouts

Content created by Egbert Rijke, Vojtěch Štěpančík and Fredrik Bakke.

Created on 2023-09-05.

module synthetic-homotopy-theory.flattening-lemma-pushouts where

Imports
open import foundation.action-on-identifications-functions
open import foundation.commuting-cubes-of-maps
open import foundation.commuting-squares-of-maps
open import foundation.commuting-triangles-of-maps
open import foundation.dependent-pair-types
open import foundation.equality-dependent-pair-types
open import foundation.equivalences
open import foundation.function-extensionality
open import foundation.function-types
open import foundation.functoriality-dependent-function-types
open import foundation.functoriality-dependent-pair-types
open import foundation.homotopies
open import foundation.identity-types
open import foundation.span-diagrams
open import foundation.transport-along-identifications
open import foundation.universal-property-dependent-pair-types
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.dependent-cocones-under-spans
open import synthetic-homotopy-theory.dependent-universal-property-pushouts
open import synthetic-homotopy-theory.descent-data-pushouts
open import synthetic-homotopy-theory.equivalences-descent-data-pushouts
open import synthetic-homotopy-theory.universal-property-pushouts


Idea

The flattening lemma for pushouts states that pushouts commute with dependent pair types. More precisely, given a pushout square

      g
S -----> B
|        |
f|        | j
∨      ⌜ ∨
A -----> X
i


with homotopy H : i ∘ f ~ j ∘ g, and for any type family P over X, the commuting square

  Σ (s : S), P(if(s)) ---> Σ (s : S), P(jg(s)) ---> Σ (b : B), P(j(b))
|                                                 |
|                                                 |
∨                                               ⌜ ∨
Σ (a : A), P(i(a)) -----------------------------> Σ (x : X), P(x)


is again a pushout square.

Definitions

The statement of the flattening lemma for pushouts

module _
{ l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
{ X : UU l4} (P : X → UU l5)
( f : S → A) (g : S → B) (c : cocone f g X)
where

vertical-map-span-flattening-pushout :
Σ S (P ∘ horizontal-map-cocone f g c ∘ f) →
Σ A (P ∘ horizontal-map-cocone f g c)
vertical-map-span-flattening-pushout =
map-Σ-map-base f (P ∘ horizontal-map-cocone f g c)

horizontal-map-span-flattening-pushout :
Σ S (P ∘ horizontal-map-cocone f g c ∘ f) →
Σ B (P ∘ vertical-map-cocone f g c)
horizontal-map-span-flattening-pushout =
map-Σ
( P ∘ vertical-map-cocone f g c)
( g)
( λ s → tr P (coherence-square-cocone f g c s))

horizontal-map-cocone-flattening-pushout :
Σ A (P ∘ horizontal-map-cocone f g c) → Σ X P
horizontal-map-cocone-flattening-pushout =
map-Σ-map-base (horizontal-map-cocone f g c) P

vertical-map-cocone-flattening-pushout :
Σ B (P ∘ vertical-map-cocone f g c) → Σ X P
vertical-map-cocone-flattening-pushout =
map-Σ-map-base (vertical-map-cocone f g c) P

coherence-square-cocone-flattening-pushout :
coherence-square-maps
( horizontal-map-span-flattening-pushout)
( vertical-map-span-flattening-pushout)
( vertical-map-cocone-flattening-pushout)
( horizontal-map-cocone-flattening-pushout)
coherence-square-cocone-flattening-pushout =
coherence-square-maps-map-Σ-map-base P g f
( vertical-map-cocone f g c)
( horizontal-map-cocone f g c)
( coherence-square-cocone f g c)

cocone-flattening-pushout :
cocone
( vertical-map-span-flattening-pushout)
( horizontal-map-span-flattening-pushout)
( Σ X P)
pr1 cocone-flattening-pushout =
horizontal-map-cocone-flattening-pushout
pr1 (pr2 cocone-flattening-pushout) =
vertical-map-cocone-flattening-pushout
pr2 (pr2 cocone-flattening-pushout) =
coherence-square-cocone-flattening-pushout

flattening-lemma-pushout-statement : UUω
flattening-lemma-pushout-statement =
universal-property-pushout f g c →
universal-property-pushout
( vertical-map-span-flattening-pushout)
( horizontal-map-span-flattening-pushout)
( cocone-flattening-pushout)

module _
{l1 l2 l3 l4 l5 : Level} {𝒮 : span-diagram l1 l2 l3}
{X : UU l4} (c : cocone-span-diagram 𝒮 X)
(P : X → UU l5)
where

span-diagram-flattening-pushout : span-diagram (l1 ⊔ l5) (l2 ⊔ l5) (l3 ⊔ l5)
span-diagram-flattening-pushout =
make-span-diagram
( vertical-map-span-flattening-pushout P _ _ c)
( horizontal-map-span-flattening-pushout P _ _ c)


The statement of the flattening lemma for pushouts, phrased using descent data

The above statement of the flattening lemma works with a provided type family over the pushout. We can instead accept a definition of this family via descent data for the pushout.

module _
{l1 l2 l3 l4 : Level} {𝒮 : span-diagram l1 l2 l3}
(P : descent-data-pushout 𝒮 l4)
where

vertical-map-span-flattening-descent-data-pushout :
Σ ( spanning-type-span-diagram 𝒮)
( λ s → pr1 P (left-map-span-diagram 𝒮 s)) →
Σ ( domain-span-diagram 𝒮) (pr1 P)
vertical-map-span-flattening-descent-data-pushout =
map-Σ-map-base
( left-map-span-diagram 𝒮)
( pr1 P)

horizontal-map-span-flattening-descent-data-pushout :
Σ ( spanning-type-span-diagram 𝒮)
( λ s → pr1 P (left-map-span-diagram 𝒮 s)) →
Σ ( codomain-span-diagram 𝒮) (pr1 (pr2 P))
horizontal-map-span-flattening-descent-data-pushout =
map-Σ
( pr1 (pr2 P))
( right-map-span-diagram 𝒮)
( λ s → map-equiv (pr2 (pr2 P) s))

span-diagram-flattening-descent-data-pushout :
span-diagram (l1 ⊔ l4) (l2 ⊔ l4) (l3 ⊔ l4)
span-diagram-flattening-descent-data-pushout =
make-span-diagram
( vertical-map-span-flattening-descent-data-pushout)
( horizontal-map-span-flattening-descent-data-pushout)

module _
{ l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
( f : S → A) (g : S → B) (c : cocone f g X)
( P : descent-data-pushout (make-span-diagram f g) l5)
( Q : X → UU l5)
( e :
equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q))
where

horizontal-map-cocone-flattening-descent-data-pushout :
Σ A (pr1 P) → Σ X Q
horizontal-map-cocone-flattening-descent-data-pushout =
map-Σ Q
( horizontal-map-cocone f g c)
( λ a → map-equiv (pr1 e a))

vertical-map-cocone-flattening-descent-data-pushout :
Σ B (pr1 (pr2 P)) → Σ X Q
vertical-map-cocone-flattening-descent-data-pushout =
map-Σ Q
( vertical-map-cocone f g c)
( λ b → map-equiv (pr1 (pr2 e) b))

coherence-square-cocone-flattening-descent-data-pushout :
coherence-square-maps
( horizontal-map-span-flattening-descent-data-pushout P)
( vertical-map-span-flattening-descent-data-pushout P)
( vertical-map-cocone-flattening-descent-data-pushout)
( horizontal-map-cocone-flattening-descent-data-pushout)
coherence-square-cocone-flattening-descent-data-pushout =
htpy-map-Σ Q
( coherence-square-cocone f g c)
( λ s → map-equiv (pr1 e (f s)))
( λ s → inv-htpy (pr2 (pr2 e) s))

cocone-flattening-descent-data-pushout :
cocone
( vertical-map-span-flattening-descent-data-pushout P)
( horizontal-map-span-flattening-descent-data-pushout P)
( Σ X Q)
pr1 cocone-flattening-descent-data-pushout =
horizontal-map-cocone-flattening-descent-data-pushout
pr1 (pr2 cocone-flattening-descent-data-pushout) =
vertical-map-cocone-flattening-descent-data-pushout
pr2 (pr2 cocone-flattening-descent-data-pushout) =
coherence-square-cocone-flattening-descent-data-pushout

flattening-lemma-descent-data-pushout-statement : UUω
flattening-lemma-descent-data-pushout-statement =
universal-property-pushout f g c →
universal-property-pushout
( vertical-map-span-flattening-descent-data-pushout P)
( horizontal-map-span-flattening-descent-data-pushout P)
( cocone-flattening-descent-data-pushout)


Properties

Proof of the flattening lemma for pushouts

The proof uses the theorem that maps from sigma types are equivalent to dependent maps over the index type, for which we can invoke the dependent universal property of the indexing pushout.

module _
{ l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3}
{ X : UU l4} (P : X → UU l5)
( f : S → A) (g : S → B) (c : cocone f g X)
where

cocone-map-flattening-pushout :
{ l : Level} (Y : UU l) →
( Σ X P → Y) →
cocone
( vertical-map-span-flattening-pushout P f g c)
( horizontal-map-span-flattening-pushout P f g c)
( Y)
cocone-map-flattening-pushout Y =
cocone-map
( vertical-map-span-flattening-pushout P f g c)
( horizontal-map-span-flattening-pushout P f g c)
( cocone-flattening-pushout P f g c)

comparison-dependent-cocone-ind-Σ-cocone :
{ l : Level} (Y : UU l) →
Σ ( (a : A) → P (horizontal-map-cocone f g c a) → Y)
( λ k →
Σ ( (b : B) → P (vertical-map-cocone f g c b) → Y)
( λ l →
( s : S) (t : P (horizontal-map-cocone f g c (f s))) →
( k (f s) t) ＝
( l (g s) (tr P (coherence-square-cocone f g c s) t)))) ≃
dependent-cocone f g c (λ x → P x → Y)
comparison-dependent-cocone-ind-Σ-cocone Y =
equiv-tot
( λ k →
equiv-tot
( λ l →
equiv-Π-equiv-family
( equiv-htpy-dependent-function-dependent-identification-function-type
( Y)
( coherence-square-cocone f g c)
( k ∘ f)
( l ∘ g))))

triangle-comparison-dependent-cocone-ind-Σ-cocone :
{ l : Level} (Y : UU l) →
coherence-triangle-maps
( dependent-cocone-map f g c (λ x → P x → Y))
( map-equiv (comparison-dependent-cocone-ind-Σ-cocone Y))
( map-equiv equiv-ev-pair³ ∘ cocone-map-flattening-pushout Y ∘ ind-Σ)
triangle-comparison-dependent-cocone-ind-Σ-cocone Y h =
eq-pair-eq-fiber
( eq-pair-eq-fiber
( eq-htpy
( inv-htpy
( compute-equiv-htpy-dependent-function-dependent-identification-function-type
( Y)
( coherence-square-cocone f g c)
( h)))))
abstract
flattening-lemma-pushout :
flattening-lemma-pushout-statement P f g c
flattening-lemma-pushout up-c Y =
is-equiv-left-factor
( cocone-map-flattening-pushout Y)
( ind-Σ)
( is-equiv-right-factor
( map-equiv equiv-ev-pair³)
( cocone-map-flattening-pushout Y ∘ ind-Σ)
( is-equiv-map-equiv equiv-ev-pair³)
( is-equiv-top-map-triangle
( dependent-cocone-map f g c (λ x → P x → Y))
( map-equiv (comparison-dependent-cocone-ind-Σ-cocone Y))
( ( map-equiv equiv-ev-pair³) ∘
( cocone-map-flattening-pushout Y) ∘
( ind-Σ))
( triangle-comparison-dependent-cocone-ind-Σ-cocone Y)
( is-equiv-map-equiv (comparison-dependent-cocone-ind-Σ-cocone Y))
( dependent-universal-property-universal-property-pushout _ _ _ up-c
( λ x → P x → Y))))
( is-equiv-ind-Σ)


Proof of the descent data statement of the flattening lemma

The proof is carried out by constructing a commuting cube, which has equivalences for vertical maps, the cocone-flattening-pushout square for the bottom, and the cocone-flattening-descent-data-pushout square for the top.

The bottom is a pushout by the above flattening lemma, which implies that the top is also a pushout.

The other parts of the cube are defined naturally, and come from the following map of spans:

  Σ (a : A) (PA a) <------- Σ (s : S) (PA (f s)) -----> Σ (b : B) (PB b)
|                           |                         |
|                           |                         |
∨                           ∨                         ∨
Σ (a : A) (P (i a)) <---- Σ (s : S) (P (i (f s))) ---> Σ (b : B) (P (j b))


where the vertical maps are equivalences given fiberwise by the equivalence of descent data.

module _
{ l1 l2 l3 l4 l5 : Level} {S : UU l1} {A : UU l2} {B : UU l3} {X : UU l4}
( f : S → A) (g : S → B) (c : cocone f g X)
( P : descent-data-pushout (make-span-diagram f g) l5)
( Q : X → UU l5)
( e :
equiv-descent-data-pushout P (descent-data-family-cocone-span-diagram c Q))
where

coherence-cube-flattening-lemma-descent-data-pushout :
coherence-cube-maps
( vertical-map-span-flattening-pushout Q f g c)
( horizontal-map-span-flattening-pushout Q f g c)
( horizontal-map-cocone-flattening-pushout Q f g c)
( vertical-map-cocone-flattening-pushout Q f g c)
( vertical-map-span-flattening-descent-data-pushout P)
( horizontal-map-span-flattening-descent-data-pushout P)
( horizontal-map-cocone-flattening-descent-data-pushout f g c P Q e)
( vertical-map-cocone-flattening-descent-data-pushout f g c P Q e)
( tot (λ s → map-equiv (pr1 e (f s))))
( tot (λ a → map-equiv (pr1 e a)))
( tot (λ b → map-equiv (pr1 (pr2 e) b)))
( id)
( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e)
( refl-htpy)
( htpy-map-Σ
( Q ∘ vertical-map-cocone f g c)
( refl-htpy)
( λ s →
tr Q (coherence-square-cocone f g c s) ∘ (map-equiv (pr1 e (f s))))
( λ s → inv-htpy (pr2 (pr2 e) s)))
( refl-htpy)
( refl-htpy)
( coherence-square-cocone-flattening-pushout Q f g c)
coherence-cube-flattening-lemma-descent-data-pushout (s , t) =
( ap-id
( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e
( s , t))) ∙
( triangle-eq-pair-Σ Q
( coherence-square-cocone f g c s)
( inv (pr2 (pr2 e) s t))) ∙
( ap
( eq-pair-Σ (coherence-square-cocone f g c s) refl ∙_)
( inv
( ( right-unit) ∙
( compute-ap-map-Σ-map-base-eq-pair-Σ
( vertical-map-cocone f g c)
( Q)
( refl)
( inv (pr2 (pr2 e) s t))))))

abstract
flattening-lemma-descent-data-pushout :
flattening-lemma-descent-data-pushout-statement f g c P Q e
flattening-lemma-descent-data-pushout up-c =
universal-property-pushout-top-universal-property-pushout-bottom-cube-is-equiv
( vertical-map-span-flattening-pushout Q f g c)
( horizontal-map-span-flattening-pushout Q f g c)
( horizontal-map-cocone-flattening-pushout Q f g c)
( vertical-map-cocone-flattening-pushout Q f g c)
( vertical-map-span-flattening-descent-data-pushout P)
( horizontal-map-span-flattening-descent-data-pushout P)
( horizontal-map-cocone-flattening-descent-data-pushout f g c P Q e)
( vertical-map-cocone-flattening-descent-data-pushout f g c P Q e)
( tot (λ s → map-equiv (pr1 e (f s))))
( tot (λ a → map-equiv (pr1 e a)))
( tot (λ b → map-equiv (pr1 (pr2 e) b)))
( id)
( coherence-square-cocone-flattening-descent-data-pushout f g c P Q e)
( refl-htpy)
( htpy-map-Σ
( Q ∘ vertical-map-cocone f g c)
( refl-htpy)
( λ s →
tr Q (coherence-square-cocone f g c s) ∘ (map-equiv (pr1 e (f s))))
( λ s → inv-htpy (pr2 (pr2 e) s)))
( refl-htpy)
( refl-htpy)
( coherence-square-cocone-flattening-pushout Q f g c)
( coherence-cube-flattening-lemma-descent-data-pushout)
( is-equiv-tot-is-fiberwise-equiv
( λ s → is-equiv-map-equiv (pr1 e (f s))))
( is-equiv-tot-is-fiberwise-equiv
( λ a → is-equiv-map-equiv (pr1 e a)))
( is-equiv-tot-is-fiberwise-equiv
( λ b → is-equiv-map-equiv (pr1 (pr2 e) b)))
( is-equiv-id)
( flattening-lemma-pushout Q f g c up-c)