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