Suspension Structures
Content created by Egbert Rijke, Fredrik Bakke, Raymond Baker and maybemabeline.
Created on 2023-08-28.
Last modified on 2023-11-23.
module synthetic-homotopy-theory.suspension-structures where
Imports
open import foundation.action-on-identifications-functions open import foundation.commuting-squares-of-identifications open import foundation.constant-maps open import foundation.contractible-types open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-extensionality open import foundation.function-types open import foundation.functoriality-dependent-pair-types open import foundation.homotopies open import foundation.identity-systems open import foundation.identity-types open import foundation.injective-maps open import foundation.path-algebra open import foundation.structure-identity-principle open import foundation.unit-type open import foundation.universal-property-unit-type open import foundation.universe-levels open import synthetic-homotopy-theory.cocones-under-spans
Idea
The suspension of X
is the pushout of
the span unit <-- X --> unit
. A
cocone under such a span
is called a suspension-cocone
. Explicitly, a suspension cocone with nadir Y
consists of functions
f : unit → Y
g : unit → Y
and a homotopy
h : (x : X) → (f ∘ (const X unit star)) x = (g ∘ (const X unit star)) x
Using the
universal property of unit
, we
can characterize suspension cocones as equivalent to a selection of "north" and
"south" poles
north , south : Y
and a meridian function
meridian : X → north = south
We call this type of structure suspension-structure
.
Definition
Suspension cocones on a type
suspension-cocone : {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (l1 ⊔ l2) suspension-cocone X Y = cocone (const X unit star) (const X unit star) Y
Suspension structures on a type
module _ {l1 l2 : Level} (X : UU l1) (Y : UU l2) where suspension-structure : UU (l1 ⊔ l2) suspension-structure = Σ Y (λ N → Σ Y (λ S → (x : X) → N = S)) module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} where north-suspension-structure : suspension-structure X Y → Y north-suspension-structure c = pr1 c south-suspension-structure : suspension-structure X Y → Y south-suspension-structure c = (pr1 ∘ pr2) c meridian-suspension-structure : (c : suspension-structure X Y) → X → north-suspension-structure c = south-suspension-structure c meridian-suspension-structure c = (pr2 ∘ pr2) c
Properties
Equivalence between suspension structures and suspension cocones
cocone-suspension-structure : {l1 l2 : Level} (X : UU l1) (Y : UU l2) → suspension-structure X Y → suspension-cocone X Y pr1 (cocone-suspension-structure X Y (N , S , merid)) = point N pr1 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = point S pr2 (pr2 (cocone-suspension-structure X Y (N , S , merid))) = merid equiv-suspension-structure-suspension-cocone : {l1 l2 : Level} (X : UU l1) (Z : UU l2) → suspension-cocone X Z ≃ suspension-structure X Z equiv-suspension-structure-suspension-cocone X Z = equiv-Σ ( λ z1 → Σ Z (λ z2 → (x : X) → Id z1 z2)) ( equiv-universal-property-unit Z) ( λ z1 → equiv-Σ ( λ z2 → (x : X) → Id (z1 star) z2) ( equiv-universal-property-unit Z) ( λ z2 → id-equiv)) map-equiv-suspension-structure-suspension-cocone : {l1 l2 : Level} (X : UU l1) (Z : UU l2) → suspension-cocone X Z → suspension-structure X Z map-equiv-suspension-structure-suspension-cocone X Z = map-equiv (equiv-suspension-structure-suspension-cocone X Z) is-equiv-map-equiv-suspension-structure-suspension-cocone : {l1 l2 : Level} (X : UU l1) (Z : UU l2) → is-equiv (map-equiv-suspension-structure-suspension-cocone X Z) is-equiv-map-equiv-suspension-structure-suspension-cocone X Z = is-equiv-map-equiv (equiv-suspension-structure-suspension-cocone X Z) map-inv-equiv-suspension-structure-suspension-cocone : {l1 l2 : Level} (X : UU l1) (Z : UU l2) → suspension-structure X Z → suspension-cocone X Z map-inv-equiv-suspension-structure-suspension-cocone X Z = map-inv-equiv (equiv-suspension-structure-suspension-cocone X Z) is-equiv-map-inv-equiv-suspension-structure-suspension-cocone : {l1 l2 : Level} (X : UU l1) (Z : UU l2) → is-equiv (map-inv-equiv-suspension-structure-suspension-cocone X Z) is-equiv-map-inv-equiv-suspension-structure-suspension-cocone X Z = is-equiv-map-inv-equiv (equiv-suspension-structure-suspension-cocone X Z) htpy-comparison-suspension-cocone-suspension-structure : {l1 l2 : Level} (X : UU l1) (Z : UU l2) → ( map-inv-equiv-suspension-structure-suspension-cocone X Z) ~ ( cocone-suspension-structure X Z) htpy-comparison-suspension-cocone-suspension-structure ( X) ( Z) ( s) = is-injective-map-equiv ( equiv-suspension-structure-suspension-cocone X Z) ( is-section-map-inv-equiv ( equiv-suspension-structure-suspension-cocone X Z) ( s))
Characterization of equalities in suspension-structure
module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} where htpy-suspension-structure : (c c' : suspension-structure X Z) → UU (l1 ⊔ l2) htpy-suspension-structure c c' = Σ ( (north-suspension-structure c) = (north-suspension-structure c')) ( λ p → Σ ( ( south-suspension-structure c) = ( south-suspension-structure c')) ( λ q → ( x : X) → ( meridian-suspension-structure c x ∙ q) = ( p ∙ meridian-suspension-structure c' x))) north-htpy-suspension-structure : {c c' : suspension-structure X Z} → htpy-suspension-structure c c' → north-suspension-structure c = north-suspension-structure c' north-htpy-suspension-structure = pr1 south-htpy-suspension-structure : {c c' : suspension-structure X Z} → htpy-suspension-structure c c' → south-suspension-structure c = south-suspension-structure c' south-htpy-suspension-structure = pr1 ∘ pr2 meridian-htpy-suspension-structure : {c c' : suspension-structure X Z} → (h : htpy-suspension-structure c c') → ( x : X) → coherence-square-identifications ( north-htpy-suspension-structure h) ( meridian-suspension-structure c x) ( meridian-suspension-structure c' x) ( south-htpy-suspension-structure h) meridian-htpy-suspension-structure = pr2 ∘ pr2 extensionality-suspension-structure : (c c' : suspension-structure X Z) → (c = c') ≃ (htpy-suspension-structure c c') extensionality-suspension-structure (N , S , merid) = extensionality-Σ ( λ y p → Σ (S = pr1 y) (λ q → (x : X) → (merid x ∙ q) = (p ∙ pr2 y x))) ( refl) ( refl , right-unit-htpy) ( λ z → id-equiv) ( extensionality-Σ ( λ H q → (x : X) → (merid x ∙ q) = H x) ( refl) ( right-unit-htpy) ( λ z → id-equiv) ( λ H → equiv-concat-htpy right-unit-htpy H ∘e equiv-funext)) module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c c' : suspension-structure X Z} where htpy-eq-suspension-structure : (c = c') → htpy-suspension-structure c c' htpy-eq-suspension-structure = map-equiv (extensionality-suspension-structure c c') eq-htpy-suspension-structure : htpy-suspension-structure c c' → (c = c') eq-htpy-suspension-structure = map-inv-equiv (extensionality-suspension-structure c c') module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c : suspension-structure X Z} where refl-htpy-suspension-structure : htpy-suspension-structure c c pr1 refl-htpy-suspension-structure = refl pr1 (pr2 refl-htpy-suspension-structure) = refl pr2 (pr2 refl-htpy-suspension-structure) = right-unit-htpy is-refl-refl-htpy-suspension-structure : refl-htpy-suspension-structure = htpy-eq-suspension-structure refl is-refl-refl-htpy-suspension-structure = refl extensionality-suspension-structure-refl-htpy-suspension-structure : eq-htpy-suspension-structure refl-htpy-suspension-structure = refl extensionality-suspension-structure-refl-htpy-suspension-structure = is-injective-map-equiv ( extensionality-suspension-structure c c) ( is-section-map-inv-equiv ( extensionality-suspension-structure c c) ( refl-htpy-suspension-structure)) module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c : suspension-structure X Z} where ind-htpy-suspension-structure : { l : Level} ( P : ( c' : suspension-structure X Z) → ( htpy-suspension-structure c c') → UU l) → ( P c refl-htpy-suspension-structure) → ( c' : suspension-structure X Z) ( H : htpy-suspension-structure c c') → P c' H ind-htpy-suspension-structure P = pr1 ( is-identity-system-is-torsorial ( c) ( refl-htpy-suspension-structure) ( is-contr-equiv ( Σ (suspension-structure X Z) (λ c' → c = c')) ( inv-equiv ( equiv-tot (extensionality-suspension-structure c))) ( is-torsorial-path c)) ( P))
The action of paths of the projections have the expected effect
module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} (c : suspension-structure X Z) where ap-pr1-eq-htpy-suspension-structure : (c' : suspension-structure X Z) (H : htpy-suspension-structure c c') → (ap (pr1) (eq-htpy-suspension-structure H)) = (pr1 H) ap-pr1-eq-htpy-suspension-structure = ind-htpy-suspension-structure ( λ c' H → (ap (pr1) (eq-htpy-suspension-structure H)) = (pr1 H)) ( (ap ( ap pr1) ( is-retraction-map-inv-equiv ( extensionality-suspension-structure c c) ( refl)))) ap-pr1∘pr2-eq-htpy-suspension-structure : (c' : suspension-structure X Z) (H : htpy-suspension-structure c c') → (ap (pr1 ∘ pr2) (eq-htpy-suspension-structure H)) = ((pr1 ∘ pr2) H) ap-pr1∘pr2-eq-htpy-suspension-structure = ind-htpy-suspension-structure ( λ c' H → ap (pr1 ∘ pr2) (eq-htpy-suspension-structure H) = (pr1 ∘ pr2) H) ( ap ( ap (pr1 ∘ pr2)) ( is-retraction-map-inv-equiv ( extensionality-suspension-structure c c) ( refl)))
Characterization of equalities in htpy-suspension-structure
module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c c' : suspension-structure X Z} where htpy-in-htpy-suspension-structure : htpy-suspension-structure c c' → htpy-suspension-structure c c' → UU (l1 ⊔ l2) htpy-in-htpy-suspension-structure (n , s , h) (n' , s' , h') = Σ ( n = n') ( λ p → Σ ( s = s') ( λ q → (x : X) → coherence-square-identifications ( h x) ( identification-left-whisk ( meridian-suspension-structure c x) ( q)) ( identification-right-whisk ( p) ( meridian-suspension-structure c' x)) ( h' x))) extensionality-htpy-suspension-structure : (h h' : htpy-suspension-structure c c') → (h = h') ≃ htpy-in-htpy-suspension-structure h h' extensionality-htpy-suspension-structure (n , s , h) = extensionality-Σ ( λ y p → Σ ( s = pr1 y) ( λ q → (x : X) → coherence-square-identifications ( h x) ( identification-left-whisk ( meridian-suspension-structure c x) ( q)) ( identification-right-whisk ( p) ( meridian-suspension-structure c' x)) ( pr2 y x))) ( refl) ( refl , inv-htpy right-unit-htpy) ( λ n' → id-equiv) ( extensionality-Σ ( λ h' q → (x : X) → coherence-square-identifications ( h x) ( identification-left-whisk (meridian-suspension-structure c x) q) ( identification-right-whisk ( refl) ( meridian-suspension-structure c' x)) ( h' x)) ( refl) ( inv-htpy right-unit-htpy) ( λ q → id-equiv) ( λ h' → ( inv-equiv (equiv-concat-htpy' h' (right-unit-htpy))) ∘e ( equiv-inv-htpy h h') ∘e ( equiv-funext {f = h} {g = h'}))) north-htpy-in-htpy-suspension-structure : {h h' : htpy-suspension-structure c c'} → htpy-in-htpy-suspension-structure h h' → ( north-htpy-suspension-structure h) = ( north-htpy-suspension-structure h') north-htpy-in-htpy-suspension-structure = pr1 south-htpy-in-htpy-suspension-structure : {h h' : htpy-suspension-structure c c'} → htpy-in-htpy-suspension-structure h h' → ( south-htpy-suspension-structure h) = ( south-htpy-suspension-structure h') south-htpy-in-htpy-suspension-structure = pr1 ∘ pr2 meridian-htpy-in-htpy-suspension-structure : {h h' : htpy-suspension-structure c c'} → (H : htpy-in-htpy-suspension-structure h h') → (x : X) → coherence-square-identifications ( meridian-htpy-suspension-structure h x) ( identification-left-whisk ( meridian-suspension-structure c x) ( south-htpy-in-htpy-suspension-structure H)) ( identification-right-whisk ( north-htpy-in-htpy-suspension-structure H) ( meridian-suspension-structure c' x)) ( meridian-htpy-suspension-structure h' x) meridian-htpy-in-htpy-suspension-structure = pr2 ∘ pr2 module _ {l1 l2 : Level} {X : UU l1} {Z : UU l2} {c c' : suspension-structure X Z} {h h' : htpy-suspension-structure c c'} where htpy-eq-htpy-suspension-structure : h = h' → htpy-in-htpy-suspension-structure h h' htpy-eq-htpy-suspension-structure = map-equiv (extensionality-htpy-suspension-structure h h') eq-htpy-in-htpy-suspension-structure : htpy-in-htpy-suspension-structure h h' → h = h' eq-htpy-in-htpy-suspension-structure = map-inv-equiv (extensionality-htpy-suspension-structure h h')
Recent changes
- 2023-11-23. Raymond Baker. Infrastructure for homotopies between maps out of a suspension (#924).
- 2023-10-21. Egbert Rijke. Rename
is-contr-total
tois-torsorial
(#871). - 2023-10-12. Fredrik Bakke. Define suspension prespectra and maps of prespectra (#833).
- 2023-09-16. maybemabeline and Egbert Rijke. Equivalence between the first sphere and the circle (#776).
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).