The universal property of fiber products
Content created by Fredrik Bakke, Egbert Rijke and Jonathan Prieto-Cubides.
Created on 2022-02-10.
Last modified on 2023-09-11.
module foundation.universal-property-fiber-products where
Imports
open import foundation.cones-over-cospans open import foundation.dependent-pair-types open import foundation.equality-cartesian-product-types open import foundation.universe-levels open import foundation-core.cartesian-product-types open import foundation-core.equality-dependent-pair-types open import foundation-core.equivalences open import foundation-core.fibers-of-maps 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.pullbacks open import foundation-core.universal-property-pullbacks
Idea
The fiberwise product of two families P
and Q
over a type X
is the family
of types (P x) × (Q x)
over X
. Similarly, the fiber product of two maps
f :A → X
and g : B → X
is the type Σ X (λ x → fiber f x × fiber g x)
,
which fits in a pullback diagram on f
and g
.
module _ {l1 l2 l3 : Level} {X : UU l1} (P : X → UU l2) (Q : X → UU l3) where cone-fiberwise-prod : cone (pr1 {B = P}) (pr1 {B = Q}) (Σ X (λ x → (P x) × (Q x))) pr1 cone-fiberwise-prod = tot (λ x → pr1) pr1 (pr2 cone-fiberwise-prod) = tot (λ x → pr2) pr2 (pr2 cone-fiberwise-prod) = refl-htpy
We will show that the fiberwise product is a pullback by showing that the gap map is an equivalence. We do this by directly construct an inverse to the gap map.
gap-fiberwise-prod : Σ X (λ x → (P x) × (Q x)) → canonical-pullback (pr1 {B = P}) (pr1 {B = Q}) gap-fiberwise-prod = gap pr1 pr1 cone-fiberwise-prod inv-gap-fiberwise-prod : canonical-pullback (pr1 {B = P}) (pr1 {B = Q}) → Σ X (λ x → (P x) × (Q x)) pr1 (inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl))) = x pr1 (pr2 (inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl)))) = p pr2 (pr2 (inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl)))) = q abstract is-section-inv-gap-fiberwise-prod : (gap-fiberwise-prod ∘ inv-gap-fiberwise-prod) ~ id is-section-inv-gap-fiberwise-prod ((x , p) , ((.x , q) , refl)) = eq-pair-Σ refl (eq-pair-Σ refl refl) abstract is-retraction-inv-gap-fiberwise-prod : (inv-gap-fiberwise-prod ∘ gap-fiberwise-prod) ~ id is-retraction-inv-gap-fiberwise-prod (x , p , q) = refl abstract is-pullback-fiberwise-prod : is-pullback (pr1 {B = P}) (pr1 {B = Q}) cone-fiberwise-prod is-pullback-fiberwise-prod = is-equiv-is-invertible inv-gap-fiberwise-prod is-section-inv-gap-fiberwise-prod is-retraction-inv-gap-fiberwise-prod abstract universal-property-pullback-fiberwise-prod : {l : Level} → universal-property-pullback l ( pr1 {B = P}) ( pr1 {B = Q}) ( cone-fiberwise-prod) universal-property-pullback-fiberwise-prod = universal-property-pullback-is-pullback pr1 pr1 cone-fiberwise-prod is-pullback-fiberwise-prod module _ {l1 l2 l3 : Level} {A : UU l1} {B : UU l2} {X : UU l3} (f : A → X) (g : B → X) where cone-total-prod-fibers : cone f g (Σ X (λ x → (fiber f x) × (fiber g x))) pr1 cone-total-prod-fibers (x , (a , p) , (b , q)) = a pr1 (pr2 cone-total-prod-fibers) (x , (a , p) , (b , q)) = b pr2 (pr2 cone-total-prod-fibers) (x , (a , p) , (b , q)) = p ∙ inv q gap-total-prod-fibers : Σ X (λ x → (fiber f x) × (fiber g x)) → canonical-pullback f g gap-total-prod-fibers = gap f g cone-total-prod-fibers inv-gap-total-prod-fibers : canonical-pullback f g → Σ X (λ x → (fiber f x) × (fiber g x)) pr1 (inv-gap-total-prod-fibers (a , b , p)) = g b pr1 (pr1 (pr2 (inv-gap-total-prod-fibers (a , b , p)))) = a pr2 (pr1 (pr2 (inv-gap-total-prod-fibers (a , b , p)))) = p pr1 (pr2 (pr2 (inv-gap-total-prod-fibers (a , b , p)))) = b pr2 (pr2 (pr2 (inv-gap-total-prod-fibers (a , b , p)))) = refl abstract is-section-inv-gap-total-prod-fibers : (gap-total-prod-fibers ∘ inv-gap-total-prod-fibers) ~ id is-section-inv-gap-total-prod-fibers (a , b , p) = map-extensionality-canonical-pullback f g refl refl ( inv right-unit ∙ inv right-unit) abstract is-retraction-inv-gap-total-prod-fibers : (inv-gap-total-prod-fibers ∘ gap-total-prod-fibers) ~ id is-retraction-inv-gap-total-prod-fibers (.(g b) , (a , p) , (b , refl)) = eq-pair-Σ refl (eq-pair (eq-pair-Σ refl right-unit) refl) abstract is-pullback-total-prod-fibers : is-pullback f g cone-total-prod-fibers is-pullback-total-prod-fibers = is-equiv-is-invertible inv-gap-total-prod-fibers is-section-inv-gap-total-prod-fibers is-retraction-inv-gap-total-prod-fibers
Recent changes
- 2023-09-11. Fredrik Bakke and Egbert Rijke. Some computations for different notions of equivalence (#711).
- 2023-09-06. Egbert Rijke. Rename fib to fiber (#722).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644).