Coproducts of pullbacks

Content created by Fredrik Bakke.

Created on 2024-03-02.
Last modified 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'))

Table of files about pullbacks

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

Recent changes