From a51d2eb590c2c9bddb01efd15536665d84c6dd49 Mon Sep 17 00:00:00 2001 From: VojtechStep Date: Wed, 17 Apr 2024 23:33:07 +0200 Subject: [PATCH] is-equiv diagram -> is-equiv inclusion into colimit --- ...cocones-under-sequential-diagrams.lagda.md | 3 + ...rsal-property-sequential-colimits.lagda.md | 333 ++++++++++++++++++ 2 files changed, 336 insertions(+) diff --git a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md index 3863a8f311..5f4d6c625b 100644 --- a/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md +++ b/src/synthetic-homotopy-theory/cocones-under-sequential-diagrams.lagda.md @@ -91,6 +91,9 @@ module _ ( map-cocone-sequential-diagram (succ-ℕ n)) ( map-sequential-diagram A n) coherence-cocone-sequential-diagram = pr2 c + + first-map-cocone-sequential-diagram : family-sequential-diagram A 0 → X + first-map-cocone-sequential-diagram = map-cocone-sequential-diagram 0 ``` ### Homotopies of cocones under a sequential diagram diff --git a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md index 54ca756368..714f25f962 100644 --- a/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md +++ b/src/synthetic-homotopy-theory/universal-property-sequential-colimits.lagda.md @@ -7,20 +7,28 @@ module synthetic-homotopy-theory.universal-property-sequential-colimits where
Imports ```agda +open import elementary-number-theory.natural-numbers + open import foundation.action-on-identifications-functions +open import foundation.commuting-squares-of-homotopies open import foundation.commuting-triangles-of-maps open import foundation.contractible-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.fibers-of-maps +open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-types open import foundation.precomposition-functions +open import foundation.retractions +open import foundation.sections open import foundation.subtype-identity-principle open import foundation.universal-property-equivalences open import foundation.universe-levels +open import foundation.whiskering-higher-homotopies-composition +open import foundation.whiskering-homotopies-composition open import synthetic-homotopy-theory.cocones-under-sequential-diagrams open import synthetic-homotopy-theory.coforks @@ -360,3 +368,328 @@ module _ ( up-c) ( up-c')) ``` + +### Inclusion maps of a sequential colimit under a sequential diagram of equivalences are equivalences + +If a sequential diagram `(A, a)` with a colimit `X` and inclusion maps +`iₙ : Aₙ → X` has the property that all `aₙ : Aₙ → Aₙ₊₁` are equivalences, then +all the inclusion maps are also equivalences. + +It suffices to show that `i₀ : A₀ → X` is an equivalence, since then the +statement follows by induction on `n` and the 3-for-2 property of equivalences: +we have [commuting triangles](foundation-core.commuting-triangles-of-maps.md) + +```text + aₙ + Aₙ ------> Aₙ₊₁ + \ ≃ / + ≃ \ / + iₙ \ / iₙ₊₁ + ∨ ∨ + X , +``` + +where `aₙ` is an equivalence by assumption, and `iₙ` is an equivalence by the +induction hypothesis, making `iₙ₊₁` an equivalence. + +To show that `i₀` is an equivalence, we use the map + +```text + first-map-cocone-sequential-colimit : {Y : 𝒰} → cocone A Y → (A₀ → Y) +``` + +selecting the first map of a cocone `j₀ : A₀ → Y`, which makes the following +triangle commute: + +```text + cocone-map + X → Y ----------> cocone A Y + \ / + \ / + - ∘ i₀ \ / first-map-cocone-sequential-colimit + \ / + ∨ ∨ + A₀ → Y . +``` + +By `X` being a colimit we have that `cocone-map` is an equivalence. Then it +suffices to show that `first-map-cocone-sequential-colimit` is an equivalence, +because it would follow that `- ∘ i₀` is an equivalence, which by the +[universal property of equivalences](foundation.universal-property-equivalences.md) +implies that `iₒ` is an equivalence. + +To show that `first-map-cocone-sequential-colimit` is an equivalence, we +construct an inverse map + +```text + cocone-first-map-is-equiv-sequential-diagram : {Y : 𝒰} → (A₀ → Y) → cocone A Y , +``` + +which to every `f : A₀ → Y` assigns the cocone + +```text + a₀ a₁ + A₀ ----> A₁ ----> A₂ ----> ⋯ + \ | / + \ | / + \ f∘a₀⁻¹ / + f \ | / f ∘ a₁⁻¹ ∘ a₀⁻¹ + \ | / + ∨ ∨ ∨ + Y , +``` + +where the coherences are witnesses that `aₙ⁻¹` are retractions of `aₙ`. + +Since the first inclusion map in this cocone is `f`, it is immediate that +`cocone-first-map-is-equiv-sequential-diagram` is a section of +`first-map-cocone-sequential-colimit`. To show that it is a retraction we need a +homotopy for any cocone `c` between itself and the cocone induced by its first +map `j₀ : A₀ → Y`. We refer to the cocone induced by `j₀` as `(j₀')`. + +The homotopy of cocones consists of homotopies + +```text + Kₙ : (j₀')ₙ ~ jₙ , +``` + +which we construct by induction as + +```text + K₀ : (j₀')₀ ≐ j₀ ~ j₀ by reflexivity + Kₙ₊₁ : (j₀')ₙ₊₁ ≐ (j₀')ₙ ∘ aₙ⁻¹ + ~ jₙ ∘ aₙ⁻¹ by Kₙ + ~ jₙ₊₁ ∘ aₙ ∘ aₙ⁻¹ by coherence Hₙ of c + ~ jₙ₊₁ by aₙ⁻¹ being a section of aₙ , +``` + +and a coherence datum which upon some pondering boils down to the following +[commuting square of homotopies](foundation-core.commuting-squares-of-homotopies.md): + +```text + Kₙ ·r (aₙ⁻¹ ∘ aₙ) Hₙ ·r (aₙ⁻¹ ∘ aₙ) + (j₀')ₙ ∘ aₙ⁻¹ ∘ aₙ ------------------> jₙ ∘ aₙ⁻¹ ∘ aₙ -------------------> jₙ₊₁ ∘ aₙ ∘ aₙ⁻¹ ∘ aₙ + | | | + | | | + | (j₀')ₙ ·l is-retraction aₙ⁻¹ | jₙ ·l is-retraction aₙ⁻¹ | jₙ₊₁ ·l is-section aₙ⁻¹ ·r aₙ + | | | + ∨ ∨ ∨ + (j₀')ₙ ------------------------------> jₙ -----------------------------> jₙ₊₁ ∘ aₙ . + Kₙ Hₙ +``` + +This rectangle is almost a pasting of the squares of naturality of `Kₙ` and `Hₙ` +with respect to `is-retraction` --- it remains to pass from +`(jₙ₊₁ ∘ aₙ) ·l is-retraction aₙ⁻¹` to `jₙ₊₁ ·l is-section aₙ⁻¹ ·r aₙ`, which we +can do by applying the coherence of +[coherently invertible maps](foundation-core.coherently-invertible-maps.md). + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} {Y : UU l2} + (equivs : (n : ℕ) → is-equiv (map-sequential-diagram A n)) + where + + map-cocone-first-map-is-equiv-sequential-diagram : + (family-sequential-diagram A 0 → Y) → + (n : ℕ) → + family-sequential-diagram A n → Y + map-cocone-first-map-is-equiv-sequential-diagram f zero-ℕ = + f + map-cocone-first-map-is-equiv-sequential-diagram f (succ-ℕ n) = + ( map-cocone-first-map-is-equiv-sequential-diagram f n) ∘ + ( map-inv-is-equiv (equivs n)) + + inv-htpy-cocone-first-map-is-equiv-sequential-diagram : + (f : family-sequential-diagram A 0 → Y) → + (n : ℕ) → + coherence-triangle-maps' + ( map-cocone-first-map-is-equiv-sequential-diagram f n) + ( ( map-cocone-first-map-is-equiv-sequential-diagram f n) ∘ + ( map-inv-is-equiv (equivs n))) + ( map-sequential-diagram A n) + inv-htpy-cocone-first-map-is-equiv-sequential-diagram f n = + ( map-cocone-first-map-is-equiv-sequential-diagram f n) ·l + ( is-retraction-map-inv-is-equiv (equivs n)) + + htpy-cocone-first-map-is-equiv-sequential-diagram : + (f : family-sequential-diagram A 0 → Y) → + (n : ℕ) → + coherence-triangle-maps + ( map-cocone-first-map-is-equiv-sequential-diagram f n) + ( ( map-cocone-first-map-is-equiv-sequential-diagram f n) ∘ + ( map-inv-is-equiv (equivs n))) + ( map-sequential-diagram A n) + htpy-cocone-first-map-is-equiv-sequential-diagram f n = + inv-htpy (inv-htpy-cocone-first-map-is-equiv-sequential-diagram f n) + + cocone-first-map-is-equiv-sequential-diagram : + (family-sequential-diagram A 0 → Y) → cocone-sequential-diagram A Y + pr1 (cocone-first-map-is-equiv-sequential-diagram f) = + map-cocone-first-map-is-equiv-sequential-diagram f + pr2 (cocone-first-map-is-equiv-sequential-diagram f) = + htpy-cocone-first-map-is-equiv-sequential-diagram f + + is-section-cocone-first-map-is-equiv-sequential-diagram : + is-section + ( first-map-cocone-sequential-diagram) + ( cocone-first-map-is-equiv-sequential-diagram) + is-section-cocone-first-map-is-equiv-sequential-diagram = refl-htpy + + htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram : + (c : cocone-sequential-diagram A Y) → + (n : ℕ) → + map-cocone-first-map-is-equiv-sequential-diagram + ( first-map-cocone-sequential-diagram c) + ( n) ~ + map-cocone-sequential-diagram c n + htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram + c zero-ℕ = refl-htpy + htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram + c (succ-ℕ n) = + ( ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram c + ( n)) ·r + ( map-inv-is-equiv (equivs n))) ∙h + ( ( coherence-cocone-sequential-diagram c n) ·r + ( map-inv-is-equiv (equivs n))) ∙h + ( ( map-cocone-sequential-diagram c (succ-ℕ n)) ·l + ( is-section-map-inv-is-equiv (equivs n))) + + coh-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram : + (c : cocone-sequential-diagram A Y) → + coherence-htpy-cocone-sequential-diagram + ( cocone-first-map-is-equiv-sequential-diagram + ( first-map-cocone-sequential-diagram c)) + ( c) + ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram c) + coh-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram c n = + inv-htpy-left-transpose-htpy-concat + ( inv-htpy-cocone-first-map-is-equiv-sequential-diagram + ( first-map-cocone-sequential-diagram c) + ( n)) + ( ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram c + ( n)) ∙h + ( coherence-cocone-sequential-diagram c n)) + ( ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram c + ( succ-ℕ n)) ·r + ( map-sequential-diagram A n)) + ( concat-right-homotopy-coherence-square-homotopies + ( ( ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram + ( c) + ( n)) ∙h + ( coherence-cocone-sequential-diagram c n)) ·r + ( map-inv-is-equiv (equivs n) ∘ map-sequential-diagram A n)) + ( ( map-cocone-first-map-is-equiv-sequential-diagram + ( first-map-cocone-sequential-diagram c) + ( n)) ·l + ( is-retraction-map-inv-is-equiv (equivs n))) + ( ( ( map-cocone-sequential-diagram c (succ-ℕ n)) ∘ + ( map-sequential-diagram A n)) ·l + ( is-retraction-map-inv-is-equiv (equivs n))) + ( ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram + ( c) + ( n)) ∙h + ( coherence-cocone-sequential-diagram c n)) + ( ( inv-preserves-comp-left-whisker-comp + ( map-cocone-sequential-diagram c (succ-ℕ n)) + ( map-sequential-diagram A n) + ( is-retraction-map-inv-is-equiv (equivs n))) ∙h + ( left-whisker-comp² + ( map-cocone-sequential-diagram c (succ-ℕ n)) + ( inv-htpy (coherence-map-inv-is-equiv (equivs n))))) + ( λ a → + inv-nat-htpy + ( ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram + ( c) + ( n)) ∙h + ( coherence-cocone-sequential-diagram c n)) + ( is-retraction-map-inv-is-equiv (equivs n) a))) + + is-retraction-cocone-first-map-is-equiv-sequential-diagram : + is-retraction + ( first-map-cocone-sequential-diagram) + ( cocone-first-map-is-equiv-sequential-diagram) + is-retraction-cocone-first-map-is-equiv-sequential-diagram c = + eq-htpy-cocone-sequential-diagram A _ _ + ( htpy-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram c , + coh-htpy-is-retraction-cocone-first-map-is-equiv-sequential-diagram c) + + is-equiv-first-map-cocone-is-equiv-sequential-diagram : + is-equiv first-map-cocone-sequential-diagram + is-equiv-first-map-cocone-is-equiv-sequential-diagram = + is-equiv-is-invertible + ( cocone-first-map-is-equiv-sequential-diagram) + ( is-section-cocone-first-map-is-equiv-sequential-diagram) + ( is-retraction-cocone-first-map-is-equiv-sequential-diagram) + +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + {X : UU l2} {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + (equivs : (n : ℕ) → is-equiv (map-sequential-diagram A n)) + where + + triangle-first-map-cocone-sequential-colimit-is-equiv : + {l3 : Level} {Y : UU l3} → + coherence-triangle-maps + ( precomp (first-map-cocone-sequential-diagram c) Y) + ( first-map-cocone-sequential-diagram) + ( cocone-map-sequential-diagram c) + triangle-first-map-cocone-sequential-colimit-is-equiv = refl-htpy + + is-equiv-first-map-cocone-sequential-colimit-is-equiv : + is-equiv (first-map-cocone-sequential-diagram c) + is-equiv-first-map-cocone-sequential-colimit-is-equiv = + is-equiv-is-equiv-precomp + ( first-map-cocone-sequential-diagram c) + ( λ Y → + is-equiv-left-map-triangle + ( precomp (first-map-cocone-sequential-diagram c) Y) + ( first-map-cocone-sequential-diagram) + ( cocone-map-sequential-diagram c) + ( triangle-first-map-cocone-sequential-colimit-is-equiv) + ( up-c Y) + ( is-equiv-first-map-cocone-is-equiv-sequential-diagram equivs)) + + is-equiv-map-cocone-sequential-colimit-is-equiv : + (n : ℕ) → is-equiv (map-cocone-sequential-diagram c n) + is-equiv-map-cocone-sequential-colimit-is-equiv zero-ℕ = + is-equiv-first-map-cocone-sequential-colimit-is-equiv + is-equiv-map-cocone-sequential-colimit-is-equiv (succ-ℕ n) = + is-equiv-right-map-triangle + ( map-cocone-sequential-diagram c n) + ( map-cocone-sequential-diagram c (succ-ℕ n)) + ( map-sequential-diagram A n) + ( coherence-cocone-sequential-diagram c n) + ( is-equiv-map-cocone-sequential-colimit-is-equiv n) + ( equivs n) +``` + +### A sequential colimit of contractible types is contractible + +A sequential diagram of contractible types consists of equivalences, as shown in +[`sequential-diagrams`](synthetic-homotopy-theory.sequential-diagrams.md), so +the inclusion maps into a colimit are equivalences as well, as shown above. In +particular, there is an equivalence `i₀ : A₀ ≃ X`, and since `A₀` is +contractible, it follows that `X` is contractible. + +```agda +module _ + {l1 l2 : Level} {A : sequential-diagram l1} + {X : UU l2} {c : cocone-sequential-diagram A X} + (up-c : universal-property-sequential-colimit c) + where + + is-contr-sequential-colimit-is-contr-sequential-diagram : + ((n : ℕ) → is-contr (family-sequential-diagram A n)) → + is-contr X + is-contr-sequential-colimit-is-contr-sequential-diagram contrs = + is-contr-is-equiv' + ( family-sequential-diagram A 0) + ( map-cocone-sequential-diagram c 0) + ( is-equiv-map-cocone-sequential-colimit-is-equiv + ( up-c) + ( is-equiv-sequential-diagram-is-contr contrs) + ( 0)) + ( contrs 0) +```