From 3c03fcff3cf64d266172afa7e558c2f32c1eb471 Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 17 Aug 2024 20:24:07 +0200 Subject: [PATCH] Horizontal fiber condition for pullbacks (#1142) This is a simple PR dualizing the vertical fiber condition for pullbacks. --- src/foundation-core/pullbacks.lagda.md | 86 ++++++++++++++++++- .../cartesian-morphisms-arrows.lagda.md | 2 +- .../dependent-sums-pullbacks.lagda.md | 2 +- .../functoriality-fibers-of-maps.lagda.md | 18 ++++ 4 files changed, 105 insertions(+), 3 deletions(-) diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index ca48ba96ed..070e4667c4 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -13,6 +13,7 @@ open import foundation.dependent-pair-types open import foundation.functoriality-cartesian-product-types open import foundation.functoriality-fibers-of-maps open import foundation.identity-types +open import foundation.morphisms-arrows open import foundation.standard-pullbacks open import foundation.universe-levels @@ -283,6 +284,22 @@ abstract ### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the vertical maps +A cone is a pullback if and only if the induced family of maps on fibers between +the vertical maps is a family of equivalences + +```text + fiber i a --> fiber g (f a) + | | + | | + ∨ ∨ + C ------------> B + | | + i | | g + ∨ ∨ + a ∈ A ------------> X. + f +``` + ```agda module _ {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} @@ -290,7 +307,7 @@ module _ where square-tot-map-fiber-vertical-map-cone : - gap f g c ∘ map-equiv-total-fiber (pr1 c) ~ + gap f g c ∘ map-equiv-total-fiber (vertical-map-cone f g c) ~ tot (λ _ → tot (λ _ → inv)) ∘ tot (map-fiber-vertical-map-cone f g c) square-tot-map-fiber-vertical-map-cone (.(vertical-map-cone f g c x) , x , refl) = @@ -332,6 +349,73 @@ module _ ( is-equiv-tot-is-fiberwise-equiv is-equiv-fsq) ``` +### A cone is a pullback if and only if it induces a family of equivalences between the fibers of the horizontal maps + +A cone is a pullback if and only if the induced family of maps on fibers between +the horizontal maps is a family of equivalences + +```text + j + fiber j b ----> C --------> B ∋ b + | | | + | | | g + ∨ ∨ ∨ + fiber f (g b) --> A --------> X. + f +``` + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} + (f : A → X) (g : B → X) (c : cone f g C) + where + + square-tot-map-fiber-horizontal-map-cone : + ( gap g f (swap-cone f g c) ∘ + map-equiv-total-fiber (horizontal-map-cone f g c)) ~ + ( tot (λ _ → tot (λ _ → inv)) ∘ + tot (map-fiber-horizontal-map-cone f g c)) + square-tot-map-fiber-horizontal-map-cone + (.(horizontal-map-cone f g c x) , x , refl) = + eq-pair-eq-fiber + ( eq-pair-eq-fiber + ( ap + ( inv) + ( inv (right-unit ∙ inv-inv (coherence-square-cone f g c x))))) + + square-tot-map-fiber-horizontal-map-cone' : + ( ( λ x → + ( horizontal-map-cone f g c x , + vertical-map-cone f g c x , + coherence-square-cone f g c x)) ∘ + map-equiv-total-fiber (horizontal-map-cone f g c)) ~ + tot (map-fiber-horizontal-map-cone f g c) + square-tot-map-fiber-horizontal-map-cone' + (.(horizontal-map-cone f g c x) , x , refl) = + eq-pair-eq-fiber + ( eq-pair-eq-fiber + ( inv (right-unit ∙ inv-inv (coherence-square-cone f g c x)))) + + abstract + is-fiberwise-equiv-map-fiber-horizontal-map-cone-is-pullback : + is-pullback f g c → + is-fiberwise-equiv (map-fiber-horizontal-map-cone f g c) + is-fiberwise-equiv-map-fiber-horizontal-map-cone-is-pullback pb = + is-fiberwise-equiv-map-fiber-vertical-map-cone-is-pullback g f + ( swap-cone f g c) + ( is-pullback-swap-cone f g c pb) + + abstract + is-pullback-is-fiberwise-equiv-map-fiber-horizontal-map-cone : + is-fiberwise-equiv (map-fiber-horizontal-map-cone f g c) → + is-pullback f g c + is-pullback-is-fiberwise-equiv-map-fiber-horizontal-map-cone is-equiv-fsq = + is-pullback-swap-cone' f g c + ( is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone g f + ( swap-cone f g c) + ( is-equiv-fsq)) +``` + ### The horizontal pullback pasting property Given a diagram as follows where the right-hand square is a pullback diff --git a/src/foundation/cartesian-morphisms-arrows.lagda.md b/src/foundation/cartesian-morphisms-arrows.lagda.md index 8750d63496..1812b64c33 100644 --- a/src/foundation/cartesian-morphisms-arrows.lagda.md +++ b/src/foundation/cartesian-morphisms-arrows.lagda.md @@ -831,7 +831,7 @@ module _ ### Lifting cartesian morphisms along lifts of the codomain -Suppose given a cospan of morphisms of arrows +Suppose given a cospan diagram of arrows ```text A ------> C <------ B diff --git a/src/foundation/dependent-sums-pullbacks.lagda.md b/src/foundation/dependent-sums-pullbacks.lagda.md index 406b3de694..08b0f1e12d 100644 --- a/src/foundation/dependent-sums-pullbacks.lagda.md +++ b/src/foundation/dependent-sums-pullbacks.lagda.md @@ -102,7 +102,7 @@ Given a map `f : A → B` with a family of maps over it ```text map-Σ f g - Σ A P ----------> Σ B Q + Σ A P ---------> Σ B Q | | | | ∨ ∨ diff --git a/src/foundation/functoriality-fibers-of-maps.lagda.md b/src/foundation/functoriality-fibers-of-maps.lagda.md index 8566e6620f..5beb6de9e9 100644 --- a/src/foundation/functoriality-fibers-of-maps.lagda.md +++ b/src/foundation/functoriality-fibers-of-maps.lagda.md @@ -123,6 +123,24 @@ module _ ( a) ``` +### Any cone induces a family of maps between the fibers of the vertical maps + +```agda +module _ + {l1 l2 l3 l4 : Level} {A : UU l1} {B : UU l2} {C : UU l3} {X : UU l4} + (f : A → X) (g : B → X) (c : cone f g C) (b : B) + where + + map-fiber-horizontal-map-cone : + fiber (horizontal-map-cone f g c) b → fiber f (g b) + map-fiber-horizontal-map-cone = + map-domain-hom-arrow-fiber + ( horizontal-map-cone f g c) + ( f) + ( hom-arrow-cone' f g c) + ( b) +``` + ### For any `f : A → B` and any identification `p : b ＝ b'` in `B`, we obtain a morphism of arrows between the fiber inclusion at `b` to the fiber inclusion at `b'` ```agda