Products of pullbacks
Content created by Fredrik Bakke.
Created on 2024-03-02.
Last modified on 2024-03-20.
module foundation.products-pullbacks where
Imports
open import foundation.cones-over-cospan-diagrams open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.functoriality-cartesian-product-types open import foundation.inhabited-types open import foundation.propositional-truncations open import foundation.pullbacks open import foundation.standard-pullbacks open import foundation.type-arithmetic-dependent-pair-types open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.equivalences open import foundation-core.function-types open import foundation-core.functoriality-dependent-pair-types open import foundation-core.homotopies open import foundation-core.identity-types 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 product
C × C' ----> B × B'
| |
| | g × g'
∨ ∨
A × A' ----> X × X'
f × f'
is a pullback if each factor is. Conversely, if the product is a pullback and the standard pullback of each factor is inhabited, then each factor is also a pullback.
Definitions
Product 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 product-cone : cone f g C → cone f' g' C' → cone (map-product f f') (map-product g g') (C × C') pr1 (product-cone (p , q , H) (p' , q' , H')) = map-product p p' pr1 (pr2 (product-cone (p , q , H) (p' , q' , H'))) = map-product q q' pr2 (pr2 (product-cone (p , q , H) (p' , q' , H'))) = htpy-map-product H H'
Properties
Computing the standard pullback of a product
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 map-product-cone-standard-pullback : (standard-pullback f g) × (standard-pullback f' g') → standard-pullback (map-product f f') (map-product g g') map-product-cone-standard-pullback = ( tot ( λ t → ( tot (λ s → eq-pair')) ∘ ( map-interchange-Σ-Σ (λ y p y' → f' (pr2 t) ＝ g' y')))) ∘ ( map-interchange-Σ-Σ (λ x t x' → Σ B' (λ y' → f' x' ＝ g' y'))) abstract is-equiv-map-product-cone-standard-pullback : is-equiv map-product-cone-standard-pullback is-equiv-map-product-cone-standard-pullback = is-equiv-comp ( tot (λ t → tot (λ s → eq-pair') ∘ map-interchange-Σ-Σ _)) ( map-interchange-Σ-Σ _) ( is-equiv-map-interchange-Σ-Σ _) ( is-equiv-tot-is-fiberwise-equiv ( λ t → is-equiv-comp ( tot (λ s → eq-pair')) ( map-interchange-Σ-Σ (λ y p y' → f' (pr2 t) ＝ g' y')) ( is-equiv-map-interchange-Σ-Σ _) ( is-equiv-tot-is-fiberwise-equiv ( λ s → is-equiv-eq-pair (map-product f f' t) (map-product g g' s))))) compute-product-standard-pullback : (standard-pullback f g) × (standard-pullback f' g') ≃ standard-pullback (map-product f f') (map-product g g') compute-product-standard-pullback = ( map-product-cone-standard-pullback , is-equiv-map-product-cone-standard-pullback)
The gap map of the standard pullback of a product computes as a product of gap maps
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 triangle-map-product-cone-standard-pullback : (c : cone f g C) (c' : cone f' g' C') → ( gap (map-product f f') (map-product g g') (product-cone f g f' g' c c')) ~ ( ( map-product-cone-standard-pullback f g f' g') ∘ ( map-product (gap f g c) (gap f' g' c'))) triangle-map-product-cone-standard-pullback c c' = refl-htpy
Products 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-product-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-product f f') ( map-product g g') ( product-cone f g f' g' c c') is-pullback-product-is-pullback c c' is-pb-c is-pb-c' = is-equiv-left-map-triangle ( gap ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c')) ( map-product-cone-standard-pullback f g f' g') ( map-product (gap f g c) (gap f' g' c')) ( triangle-map-product-cone-standard-pullback f g f' g' c c') ( is-equiv-map-product (gap f g c) (gap f' g' c') is-pb-c is-pb-c') ( is-equiv-map-product-cone-standard-pullback f g f' g')
Products of cones satisfying 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) (c : cone f g C) (f' : A' → X') (g' : B' → X') (c' : cone f' g' C') where universal-property-pullback-product-universal-property-pullback : universal-property-pullback f g c → universal-property-pullback f' g' c' → universal-property-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') universal-property-pullback-product-universal-property-pullback H H' = universal-property-pullback-is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') ( is-pullback-product-is-pullback f g f' g' c c' ( is-pullback-universal-property-pullback f g c H) ( is-pullback-universal-property-pullback f' g' c' H'))
If the product is a pullback and the standard pullback of each factor is inhabited then both factors 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') (c : cone f g C) (c' : cone f' g' C') where abstract is-pullback-left-factor-is-inhabited-standard-pullback-right-factor-is-pullback-product' : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → standard-pullback f' g' → is-pullback f g c is-pullback-left-factor-is-inhabited-standard-pullback-right-factor-is-pullback-product' H t = is-equiv-left-factor-is-equiv-map-product' ( gap f g c) ( gap f' g' c') ( t) ( is-equiv-top-map-triangle ( gap ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c')) ( map-product-cone-standard-pullback f g f' g') ( map-product (gap f g c) (gap f' g' c')) ( triangle-map-product-cone-standard-pullback f g f' g' c c') ( is-equiv-map-product-cone-standard-pullback f g f' g') ( H)) abstract is-pullback-left-factor-is-inhabited-standard-pullback-right-factor-is-pullback-product : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → is-inhabited (standard-pullback f' g') → is-pullback f g c is-pullback-left-factor-is-inhabited-standard-pullback-right-factor-is-pullback-product H = rec-trunc-Prop ( is-pullback-Prop f g c) ( is-pullback-left-factor-is-inhabited-standard-pullback-right-factor-is-pullback-product' ( H)) is-pullback-left-factor-is-inhabited-right-factor-is-pullback-product' : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → C' → is-pullback f g c is-pullback-left-factor-is-inhabited-right-factor-is-pullback-product' H t = is-pullback-left-factor-is-inhabited-standard-pullback-right-factor-is-pullback-product' ( H) ( gap f' g' c' t) is-pullback-left-factor-is-inhabited-right-factor-is-pullback-product : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → is-inhabited C' → is-pullback f g c is-pullback-left-factor-is-inhabited-right-factor-is-pullback-product H = rec-trunc-Prop ( is-pullback-Prop f g c) ( is-pullback-left-factor-is-inhabited-right-factor-is-pullback-product' ( H)) abstract is-pullback-right-factor-is-inhabited-standard-pullback-left-factor-is-pullback-product' : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → standard-pullback f g → is-pullback f' g' c' is-pullback-right-factor-is-inhabited-standard-pullback-left-factor-is-pullback-product' H t = is-equiv-right-factor-is-equiv-map-product' ( gap f g c) ( gap f' g' c') ( t) ( is-equiv-top-map-triangle ( gap ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c')) ( map-product-cone-standard-pullback f g f' g') ( map-product (gap f g c) (gap f' g' c')) ( triangle-map-product-cone-standard-pullback f g f' g' c c') ( is-equiv-map-product-cone-standard-pullback f g f' g') ( H)) abstract is-pullback-right-factor-is-inhabited-standard-pullback-left-factor-is-pullback-product : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → is-inhabited (standard-pullback f g) → is-pullback f' g' c' is-pullback-right-factor-is-inhabited-standard-pullback-left-factor-is-pullback-product H = rec-trunc-Prop ( is-pullback-Prop f' g' c') ( is-pullback-right-factor-is-inhabited-standard-pullback-left-factor-is-pullback-product' ( H)) is-pullback-right-factor-is-inhabited-left-factor-is-pullback-product' : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → C → is-pullback f' g' c' is-pullback-right-factor-is-inhabited-left-factor-is-pullback-product' H t = is-pullback-right-factor-is-inhabited-standard-pullback-left-factor-is-pullback-product' ( H) ( gap f g c t) is-pullback-right-factor-is-inhabited-left-factor-is-pullback-product : is-pullback ( map-product f f') ( map-product g g') ( product-cone f g f' g' c c') → is-inhabited C → is-pullback f' g' c' is-pullback-right-factor-is-inhabited-left-factor-is-pullback-product H = rec-trunc-Prop ( is-pullback-Prop f' g' c') ( is-pullback-right-factor-is-inhabited-left-factor-is-pullback-product' ( H))
Table of files about pullbacks
The following table lists files that are about pullbacks as a general concept.
Recent changes
- 2024-03-20. Fredrik Bakke. Janitorial work on equivalences and embeddings (#1085).
- 2024-03-02. Fredrik Bakke. Factor out standard pullbacks (#1042).