From fdc36fc5a4319908eb0a47188ea79a19e0bbae5b Mon Sep 17 00:00:00 2001 From: Fredrik Bakke Date: Sat, 9 Mar 2024 21:48:29 +0100 Subject: [PATCH] Associativity of pullbacks (#1054) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Proves $(A ×_X B) ×_Y C ≃ A ×_X (B ×_Y C)$ for standard and non-standard pullbacks. --- src/foundation-core/pullbacks.lagda.md | 103 ++++++++- src/foundation/pullbacks.lagda.md | 4 +- src/foundation/standard-pullbacks.lagda.md | 198 ++++++++++++++++++ .../universal-property-pullbacks.lagda.md | 4 +- .../orthogonal-maps.lagda.md | 4 +- .../universal-property-pushouts.lagda.md | 4 +- 6 files changed, 305 insertions(+), 12 deletions(-) diff --git a/src/foundation-core/pullbacks.lagda.md b/src/foundation-core/pullbacks.lagda.md index 8c2d7fae4d..94d5fe5e54 100644 --- a/src/foundation-core/pullbacks.lagda.md +++ b/src/foundation-core/pullbacks.lagda.md @@ -384,12 +384,12 @@ module _ where abstract - is-pullback-top-is-pullback-rectangle : + is-pullback-top-square-is-pullback-rectangle : (c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) → is-pullback f g c → is-pullback f (g ∘ h) (pasting-vertical-cone f g h c d) → is-pullback (horizontal-map-cone f g c) h d - is-pullback-top-is-pullback-rectangle c d is-pb-c is-pb-dc = + is-pullback-top-square-is-pullback-rectangle c d is-pb-c is-pb-dc = is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone ( horizontal-map-cone f g c) ( h) @@ -442,12 +442,12 @@ module _ ( x , refl)) abstract - is-pullback-rectangle-is-pullback-top : + is-pullback-rectangle-is-pullback-top-square : (c : cone f g B) (d : cone (horizontal-map-cone f g c) h A) → is-pullback f g c → is-pullback (horizontal-map-cone f g c) h d → is-pullback f (g ∘ h) (pasting-vertical-cone f g h c d) - is-pullback-rectangle-is-pullback-top c d is-pb-c is-pb-d = + is-pullback-rectangle-is-pullback-top-square c d is-pb-c is-pb-d = is-pullback-is-fiberwise-equiv-map-fiber-vertical-map-cone ( f) ( g ∘ h) @@ -502,6 +502,101 @@ module _ ( pr1 t)))) ``` +### Pullbacks are associative + +Consider two cospans with a shared vertex `B`: + +```text + f g h i + A ----> X <---- B ----> Y <---- C, +``` + +and with pullback cones `α` and `β` respectively. Moreover, consider a cone `γ` +over the pullbacks as in the following diagram + +```text + ∙ ------------> ∙ ------------> C + | | ⌟ | + | γ | β | i + ∨ ∨ ∨ + ∙ ------------> B ------------> Y + | ⌟ | h + | α | g + ∨ ∨ + A ------------> X. + f +``` + +Then the pasting `γ □ α` is a pullback if and only if `γ` is if and only if the +pasting `γ □ β` is. And, in particular, we have the equivalence + +\[ (A ×_X B) ×_Y C ≃ A ×_X (B ×_Y C). \] + +```agda +module _ + {l1 l2 l3 l4 l5 l6 l7 l8 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + {S : UU l6} {T : UU l7} {U : UU l8} + (α : cone f g S) (β : cone h i T) + (γ : cone (horizontal-map-cone f g α) (vertical-map-cone h i β) U) + (is-pullback-α : is-pullback f g α) + (is-pullback-β : is-pullback h i β) + where + + is-pullback-associative : + is-pullback + ( f) + ( g ∘ vertical-map-cone h i β) + ( pasting-vertical-cone f g (vertical-map-cone h i β) α γ) → + is-pullback + ( h ∘ horizontal-map-cone f g α) + ( i) + ( pasting-horizontal-cone (horizontal-map-cone f g α) h i β γ) + is-pullback-associative H = + is-pullback-rectangle-is-pullback-left-square + ( horizontal-map-cone f g α) + ( h) + ( i) + ( β) + ( γ) + ( is-pullback-β) + ( is-pullback-top-square-is-pullback-rectangle + ( f) + ( g) + ( vertical-map-cone h i β) + ( α) + ( γ) + ( is-pullback-α) + ( H)) + + is-pullback-inv-associative : + is-pullback + ( h ∘ horizontal-map-cone f g α) + ( i) + ( pasting-horizontal-cone (horizontal-map-cone f g α) h i β γ) → + is-pullback + ( f) + ( g ∘ vertical-map-cone h i β) + ( pasting-vertical-cone f g (vertical-map-cone h i β) α γ) + is-pullback-inv-associative H = + is-pullback-rectangle-is-pullback-top-square + ( f) + ( g) + ( vertical-map-cone h i β) + ( α) + ( γ) + ( is-pullback-α) + ( is-pullback-left-square-is-pullback-rectangle + ( horizontal-map-cone f g α) + ( h) + ( i) + ( β) + ( γ) + ( is-pullback-β) + ( H)) +``` + ### Pullbacks can be "folded" Given a pullback square diff --git a/src/foundation/pullbacks.lagda.md b/src/foundation/pullbacks.lagda.md index a874b3ec49..0221070c13 100644 --- a/src/foundation/pullbacks.lagda.md +++ b/src/foundation/pullbacks.lagda.md @@ -240,7 +240,7 @@ module _ is-pullback h' k' (f' , g' , top) is-pullback-top-is-pullback-bottom-cube-is-equiv is-equiv-hA is-equiv-hB is-equiv-hC is-equiv-hD is-pb-bottom = - is-pullback-top-is-pullback-rectangle h hD k' + is-pullback-top-square-is-pullback-rectangle h hD k' ( hB , h' , front-left) ( f' , g' , top) ( is-pullback-is-equiv-vertical-maps h hD @@ -262,7 +262,7 @@ module _ ( ap-concat-htpy' ( (front-left ·r f') ∙h (hD ·l top)) ( inv-htpy-right-unit-htpy {H = h ·l back-left})))) - ( is-pullback-rectangle-is-pullback-top h k hC + ( is-pullback-rectangle-is-pullback-top-square h k hC ( f , g , bottom) ( hA , g' , back-right) ( is-pb-bottom) diff --git a/src/foundation/standard-pullbacks.lagda.md b/src/foundation/standard-pullbacks.lagda.md index 51cd62a11f..f66c83afb2 100644 --- a/src/foundation/standard-pullbacks.lagda.md +++ b/src/foundation/standard-pullbacks.lagda.md @@ -129,6 +129,36 @@ module _ pr2 (pr2 (gap c z)) = coherence-square-cone f g c z ``` +#### The standard ternary pullback + +Given two cospans with a shared vertex `B`: + +```text + f g h i + A ----> X <---- B ----> Y <---- C, +``` + +we call the standard limit of the diagram the +{{#concept "standard ternary pullback" Disambiguation="of types" Agda=standard-ternary-pullback}}. +It is defined as the sum + +```text + standard-ternary-pullback f g h i := + Σ (a : A) (b : B) (c : C), ((f a ＝ g b) × (h b ＝ i c)). +``` + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + standard-ternary-pullback : UU (l1 ⊔ l2 ⊔ l3 ⊔ l4 ⊔ l5) + standard-ternary-pullback = + Σ A (λ a → Σ B (λ b → Σ C (λ c → (f a ＝ g b) × (h b ＝ i c)))) +``` + ## Properties ### Characterization of the identity type of the standard pullback @@ -271,6 +301,174 @@ triangle-map-commutative-standard-pullback : triangle-map-commutative-standard-pullback f g c = refl-htpy ``` +### Standard pullbacks are associative + +Consider two cospans with a shared vertex `B`: + +```text + f g h i + A ----> X <---- B ----> Y <---- C, +``` + +then we can construct their limit using standard pullbacks in two equivalent +ways. We can construct it by first forming the standard pullback of `f` and `g`, +and then forming the standard pullback of the resulting `h ∘ f'` and `i` + +```text + (A ×_X B) ×_Y C ---------------------> C + | ⌟ | + | | i + ∨ ∨ + A ×_X B ---------> B ------------> Y + | ⌟ f' | h + | | g + ∨ ∨ + A ------------> X, + f +``` + +or we can first form the pullback of `h` and `i`, and then form the pullback of +`f` and the resulting `g ∘ i'`: + +```text + A ×_X (B ×_Y C) --> B ×_Y C ---------> C + | ⌟ | ⌟ | + | | i' | i + | ∨ ∨ + | B ------------> Y + | | h + | | g + ∨ ∨ + A ------------> X. + f +``` + +We show that both of these constructions are equivalent by showing they are +equivalent to the standard ternary pullback. + +**Note:** Associativity with respect to ternary cospans + +```text + B + | + | g + ∨ + A ------> X <------ C + f h +``` + +is a special case of what we consider here that is recovered by using + +```text + f g g h + A ----> X <---- B ----> X <---- C. +``` + +- See also the following relevant stack exchange question: + [Associativity of pullbacks](https://math.stackexchange.com/questions/2046276/associativity-of-pullbacks). + +#### Computing the left associated iterated standard pullback + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + map-left-associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i → + standard-ternary-pullback f g h i + map-left-associative-standard-pullback ((a , b , p) , c , q) = + ( a , b , c , p , q) + + map-inv-left-associative-standard-pullback : + standard-ternary-pullback f g h i → + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i + map-inv-left-associative-standard-pullback (a , b , c , p , q) = + ( ( a , b , p) , c , q) + + is-equiv-map-left-associative-standard-pullback : + is-equiv map-left-associative-standard-pullback + is-equiv-map-left-associative-standard-pullback = + is-equiv-is-invertible + ( map-inv-left-associative-standard-pullback) + ( refl-htpy) + ( refl-htpy) + + compute-left-associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃ + standard-ternary-pullback f g h i + compute-left-associative-standard-pullback = + ( map-left-associative-standard-pullback , + is-equiv-map-left-associative-standard-pullback) +``` + +#### Computing the right associated iterated dependent pullback + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + map-right-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) → + standard-ternary-pullback f g h i + map-right-associative-standard-pullback (a , (b , c , p) , q) = + ( a , b , c , q , p) + + map-inv-right-associative-standard-pullback : + standard-ternary-pullback f g h i → + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) + map-inv-right-associative-standard-pullback (a , b , c , p , q) = + ( a , (b , c , q) , p) + + is-equiv-map-right-associative-standard-pullback : + is-equiv map-right-associative-standard-pullback + is-equiv-map-right-associative-standard-pullback = + is-equiv-is-invertible + ( map-inv-right-associative-standard-pullback) + ( refl-htpy) + ( refl-htpy) + + compute-right-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) ≃ + standard-ternary-pullback f g h i + compute-right-associative-standard-pullback = + ( map-right-associative-standard-pullback , + is-equiv-map-right-associative-standard-pullback) +``` + +#### Standard pullbacks are associative + +```agda +module _ + {l1 l2 l3 l4 l5 : Level} + {X : UU l1} {Y : UU l2} {A : UU l3} {B : UU l4} {C : UU l5} + (f : A → X) (g : B → X) (h : B → Y) (i : C → Y) + where + + associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i ≃ + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) + associative-standard-pullback = + ( inv-equiv (compute-right-associative-standard-pullback f g h i)) ∘e + ( compute-left-associative-standard-pullback f g h i) + + map-associative-standard-pullback : + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i → + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) + map-associative-standard-pullback = map-equiv associative-standard-pullback + + map-inv-associative-standard-pullback : + standard-pullback f (g ∘ vertical-map-standard-pullback {f = h} {g = i}) → + standard-pullback (h ∘ horizontal-map-standard-pullback {f = f} {g = g}) i + map-inv-associative-standard-pullback = + map-inv-equiv associative-standard-pullback +``` + ### Pullbacks can be "folded" Given a standard pullback square diff --git a/src/foundation/universal-property-pullbacks.lagda.md b/src/foundation/universal-property-pullbacks.lagda.md index 91a7926d36..cd707c49f7 100644 --- a/src/foundation/universal-property-pullbacks.lagda.md +++ b/src/foundation/universal-property-pullbacks.lagda.md @@ -189,7 +189,7 @@ module _ ( horizontal-map-cone f g c) ( h) ( d) - ( is-pullback-top-is-pullback-rectangle f g h c d + ( is-pullback-top-square-is-pullback-rectangle f g h c d ( is-pullback-universal-property-pullback f g c up-pb-c) ( is-pullback-universal-property-pullback f (g ∘ h) ( pasting-vertical-cone f g h c d) @@ -207,7 +207,7 @@ module _ ( f) ( g ∘ h) ( pasting-vertical-cone f g h c d) - ( is-pullback-rectangle-is-pullback-top f g h c d + ( is-pullback-rectangle-is-pullback-top-square f g h c d ( is-pullback-universal-property-pullback f g c up-pb-c) ( is-pullback-universal-property-pullback ( horizontal-map-cone f g c) diff --git a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md index f36a8be710..971e36e5dd 100644 --- a/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md +++ b/src/orthogonal-factorization-systems/orthogonal-maps.lagda.md @@ -420,7 +420,7 @@ module _ is-orthogonal-pullback-condition f g → is-orthogonal-pullback-condition f (h ∘ g) is-orthogonal-pullback-condition-right-comp = - is-pullback-rectangle-is-pullback-top + is-pullback-rectangle-is-pullback-top-square ( precomp f Z) ( postcomp A h) ( postcomp A g) @@ -452,7 +452,7 @@ module _ is-orthogonal-pullback-condition f (h ∘ g) → is-orthogonal-pullback-condition f g is-orthogonal-pullback-condition-right-right-factor = - is-pullback-top-is-pullback-rectangle + is-pullback-top-square-is-pullback-rectangle ( precomp f Z) ( postcomp A h) ( postcomp A g) diff --git a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md index 80c3d20dc8..e0e8419f3d 100644 --- a/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-pushouts.lagda.md @@ -462,7 +462,7 @@ module _ ( horizontal-map-cocone (vertical-map-cocone f g c) k d) ( coherence-square-cocone f g c) ( coherence-square-cocone (vertical-map-cocone f g c) k d))))) - ( is-pullback-rectangle-is-pullback-top + ( is-pullback-rectangle-is-pullback-top-square ( precomp f W) ( precomp g W) ( precomp k W) @@ -495,7 +495,7 @@ module _ ( k) ( d) ( λ W → - is-pullback-top-is-pullback-rectangle + is-pullback-top-square-is-pullback-rectangle ( precomp f W) ( precomp g W) ( precomp k W)