Coproducts of pullbacks

Content created by Fredrik Bakke.

Created on 2024-03-02.

module foundation.coproducts-pullbacks where

Imports
open import foundation.action-on-identifications-functions
open import foundation.cones-over-cospan-diagrams
open import foundation.coproduct-types
open import foundation.dependent-pair-types
open import foundation.equality-coproduct-types
open import foundation.functoriality-coproduct-types
open import foundation.identity-types
open import foundation.standard-pullbacks
open import foundation.universe-levels

open import foundation-core.commuting-triangles-of-maps
open import foundation-core.equality-dependent-pair-types
open import foundation-core.equivalences
open import foundation-core.function-types
open import foundation-core.homotopies
open import foundation-core.pullbacks
open import foundation-core.retractions
open import foundation-core.sections
open import foundation-core.universal-property-pullbacks


Idea

Given two commuting squares of maps,

    C ------> B                  C' -----> B'
|         |                  |         |
|         |  g     and       |         | g'
∨         ∨                  ∨         ∨
A ------> X                  A' -----> X',
f                            f'


then their coproduct

  C + C' ----> B + B'
|            |
|            | g + g'
∨            ∨
A + A' ----> X + X'
f + f'


is a pullback if each summand is.

Definitions

Coproduct cones

module _
{l1 l2 l3 l4 l1' l2' l3' l4' : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
{A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {C' : UU l4'}
(f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
where

coproduct-cone :
cone f g C → cone f' g' C' →
cone (map-coproduct f f') (map-coproduct g g') (C + C')
pr1 (coproduct-cone (p , q , H) (p' , q' , H')) = map-coproduct p p'
pr1 (pr2 (coproduct-cone (p , q , H) (p' , q' , H'))) = map-coproduct q q'
pr2 (pr2 (coproduct-cone (p , q , H) (p' , q' , H'))) =
( inv-htpy (preserves-comp-map-coproduct p f p' f')) ∙h
( htpy-map-coproduct H H') ∙h
( preserves-comp-map-coproduct q g q' g')


Properties

Computing the standard pullback of a coproduct

module _
{l1 l2 l3 l1' l2' l3' : Level}
{A : UU l1} {B : UU l2} {X : UU l3}
{A' : UU l1'} {B' : UU l2'} {X' : UU l3'}
(f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
where

inl-map-standard-pullback-coproduct :
standard-pullback f g →
standard-pullback (map-coproduct f f') (map-coproduct g g')
pr1 (inl-map-standard-pullback-coproduct (x , y , p)) = inl x
pr1 (pr2 (inl-map-standard-pullback-coproduct (x , y , p))) = inl y
pr2 (pr2 (inl-map-standard-pullback-coproduct (x , y , p))) = ap inl p

inr-map-standard-pullback-coproduct :
standard-pullback f' g' →
standard-pullback (map-coproduct f f') (map-coproduct g g')
pr1 (inr-map-standard-pullback-coproduct (x , y , p)) = inr x
pr1 (pr2 (inr-map-standard-pullback-coproduct (x , y , p))) = inr y
pr2 (pr2 (inr-map-standard-pullback-coproduct (x , y , p))) = ap inr p

map-standard-pullback-coproduct :
standard-pullback f g + standard-pullback f' g' →
standard-pullback (map-coproduct f f') (map-coproduct g g')
map-standard-pullback-coproduct (inl v) =
inl-map-standard-pullback-coproduct v
map-standard-pullback-coproduct (inr u) =
inr-map-standard-pullback-coproduct u

map-inv-standard-pullback-coproduct :
standard-pullback (map-coproduct f f') (map-coproduct g g') →
standard-pullback f g + standard-pullback f' g'
map-inv-standard-pullback-coproduct (inl x , inl y , p) =
inl (x , y , is-injective-inl p)
map-inv-standard-pullback-coproduct (inr x , inr y , p) =
inr (x , y , is-injective-inr p)

is-section-map-inv-standard-pullback-coproduct :
is-section
( map-standard-pullback-coproduct)
( map-inv-standard-pullback-coproduct)
is-section-map-inv-standard-pullback-coproduct (inl x , inl y , p) =
eq-pair-eq-fiber (eq-pair-eq-fiber (is-section-is-injective-inl p))
is-section-map-inv-standard-pullback-coproduct (inr x , inr y , p) =
eq-pair-eq-fiber (eq-pair-eq-fiber (is-section-is-injective-inr p))

is-retraction-map-inv-standard-pullback-coproduct :
is-retraction
( map-standard-pullback-coproduct)
( map-inv-standard-pullback-coproduct)
is-retraction-map-inv-standard-pullback-coproduct (inl (x , y , p)) =
ap
( inl)
( eq-pair-eq-fiber (eq-pair-eq-fiber (is-retraction-is-injective-inl p)))
is-retraction-map-inv-standard-pullback-coproduct (inr (x , y , p)) =
ap
( inr)
( eq-pair-eq-fiber (eq-pair-eq-fiber (is-retraction-is-injective-inr p)))

abstract
is-equiv-map-standard-pullback-coproduct :
is-equiv map-standard-pullback-coproduct
is-equiv-map-standard-pullback-coproduct =
is-equiv-is-invertible
map-inv-standard-pullback-coproduct
is-section-map-inv-standard-pullback-coproduct
is-retraction-map-inv-standard-pullback-coproduct

compute-standard-pullback-coproduct :
standard-pullback f g + standard-pullback f' g' ≃
standard-pullback (map-coproduct f f') (map-coproduct g g')
compute-standard-pullback-coproduct =
map-standard-pullback-coproduct , is-equiv-map-standard-pullback-coproduct


The gap map of a coproduct computes as a coproduct of gap maps

module _
{l1 l2 l3 l1' l2' l3' : Level}
{A : UU l1} {B : UU l2} {X : UU l3}
{A' : UU l1'} {B' : UU l2'} {X' : UU l3'}
(f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
where

triangle-map-standard-pullback-coproduct :
{l4 l4' : Level} {C : UU l4} {C' : UU l4'}
(c : cone f g C) (c' : cone f' g' C') →
coherence-triangle-maps
( gap
( map-coproduct f f')
( map-coproduct g g')
( coproduct-cone f g f' g' c c'))
( map-standard-pullback-coproduct f g f' g')
( map-coproduct (gap f g c) (gap f' g' c'))
triangle-map-standard-pullback-coproduct c c' (inl _) =
eq-pair-eq-fiber (eq-pair-eq-fiber right-unit)
triangle-map-standard-pullback-coproduct c c' (inr _) =
eq-pair-eq-fiber (eq-pair-eq-fiber right-unit)


Coproducts of pullbacks are pullbacks

module _
{l1 l2 l3 l4 l1' l2' l3' l4' : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
{A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {C' : UU l4'}
(f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
where

abstract
is-pullback-coproduct-is-pullback :
(c : cone f g C) (c' : cone f' g' C') →
is-pullback f g c →
is-pullback f' g' c' →
is-pullback
( map-coproduct f f')
( map-coproduct g g')
( coproduct-cone f g f' g' c c')
is-pullback-coproduct-is-pullback c c' is-pb-c is-pb-c' =
is-equiv-left-map-triangle
( gap
( map-coproduct f f')
( map-coproduct g g')
( coproduct-cone f g f' g' c c'))
( map-standard-pullback-coproduct f g f' g')
( map-coproduct (gap f g c) (gap f' g' c'))
( triangle-map-standard-pullback-coproduct f g f' g' c c')
( is-equiv-map-coproduct is-pb-c is-pb-c')
( is-equiv-map-standard-pullback-coproduct f g f' g')


Coproducts of cones that satisfy the universal property of pullbacks satisfy the universal property of pullbacks

module _
{l1 l2 l3 l4 l1' l2' l3' l4' : Level}
{A : UU l1} {B : UU l2} {X : UU l3} {C : UU l4}
{A' : UU l1'} {B' : UU l2'} {X' : UU l3'} {C' : UU l4'}
(f : A → X) (g : B → X) (f' : A' → X') (g' : B' → X')
where

abstract
universal-property-pullback-coproduct-universal-property-pullback :
(c : cone f g C) (c' : cone f' g' C') →
universal-property-pullback f g c →
universal-property-pullback f' g' c' →
universal-property-pullback
( map-coproduct f f')
( map-coproduct g g')
( coproduct-cone f g f' g' c c')
universal-property-pullback-coproduct-universal-property-pullback
c c' up-pb-c up-pb-c' =
universal-property-pullback-is-pullback
( map-coproduct f f')
( map-coproduct g g')
( coproduct-cone f g f' g' c c')
( is-pullback-coproduct-is-pullback f g f' g' c c'
( is-pullback-universal-property-pullback f g c up-pb-c)
( is-pullback-universal-property-pullback f' g' c' up-pb-c'))


The following table lists files that are about pullbacks as a general concept.

ConceptFile
Cospan diagramsfoundation.cospans
Morphisms of cospan diagramsfoundation.morphisms-cospans
Cones over cospan diagramsfoundation.cones-over-cospan-diagrams
The universal property of pullbacks (foundation-core)foundation-core.universal-property-pullbacks
The universal property of pullbacks (foundation)foundation.universal-property-pullbacks
The universal property of fiber productsfoundation.universal-property-fiber-products
Standard pullbacksfoundation.standard-pullbacks
Pullbacks (foundation-core)foundation-core.pullbacks
Pullbacks (foundation)foundation.pullbacks
Functoriality of pullbacksfoundation.functoriality-pullbacks
Cartesian morphisms of arrowsfoundation.cartesian-morphisms-arrows
Dependent products of pullbacksfoundation.dependent-products-pullbacks
Dependent sums of pullbacksfoundation.dependent-sums-pullbacks
Products of pullbacksfoundation.products-pullbacks
Coroducts of pullbacksfoundation.coproducts-pullbacks
Postcomposition of pullbacksfoundation.postcomposition-pullbacks
Pullbacks of subtypesfoundation.pullbacks-subtypes
The pullback-homorthogonal-factorization-systems.pullback-hom
Functoriality of the pullback-homorthogonal-factorization-systems.functoriality-pullback-hom
Pullbacks in precategoriescategory-theory.pullbacks-in-precategories