module Homotopy.Space.Suspension where
Suspension🔗
Given a type its (reduced) suspension is the higher-inductive type generated by the following constructors:
data Susp {ℓ} (A : Type ℓ) : Type ℓ where north : Susp A south : Susp A merid : A → north ≡ south
The names north
and south
are meant to evoke the
north and south poles of a sphere, respectively, and
the name merid
should evoke the
meridians. Indeed, we can picture a suspension like a sphere1:
We have the north and south poles and above and below a copy of the space which is diagrammatically represented by the shaded region. In the type theory, we can’t really “see” this copy of we only see its ghost, as something keeping all the meridians from collapsing.
By convention, we see the suspension as a pointed type with the north pole as the base point.
Σ∙ : ∀ {ℓ} (A : Type ℓ) → Type∙ ℓ Σ∙ A = Susp A , north Σ¹ : ∀ {ℓ} → Type∙ ℓ → Type∙ ℓ Σ¹ (A , _) = Σ∙ A
Susp-elim : ∀ {ℓ ℓ'} {A : Type ℓ} (P : Susp A → Type ℓ') → (pN : P north) (pS : P south) → (∀ x → PathP (λ i → P (merid x i)) pN pS) → ∀ x → P x Susp-elim P pN pS pmerid north = pN Susp-elim P pN pS pmerid south = pS Susp-elim P pN pS pmerid (merid x i) = pmerid x i unquoteDecl Susp-elim-prop = make-elim-n 1 Susp-elim-prop (quote Susp)
Every suspension admits a surjection from the booleans:
2→Σ : ∀ {ℓ} {A : Type ℓ} → Bool → Susp A 2→Σ true = north 2→Σ false = south 2→Σ-surjective : is-surjective (2→Σ {A = A}) 2→Σ-surjective = Susp-elim-prop (λ _ → hlevel 1) (inc (true , refl)) (inc (false , refl))
Suspension extends to a functor in the evident way.
Susp-map : (A → B) → Susp A → Susp B Susp-map f north = north Susp-map f south = south Susp-map f (merid x i) = merid (f x) i Susp-map∙ : (A∙ →∙ B∙) → Σ¹ A∙ →∙ Σ¹ B∙ Susp-map∙ (f , pt) = Susp-map f , refl Susp-map∙-id : Susp-map∙ {A∙ = A∙} id∙ ≡ id∙ Susp-map∙-id = funext∙ (Susp-elim _ refl refl λ x i j → merid x i) refl Susp-map∙-∘ : (f : B∙ →∙ C∙) (g : A∙ →∙ B∙) → Susp-map∙ (f ∘∙ g) ≡ Susp-map∙ f ∘∙ Susp-map∙ g Susp-map∙-∘ (f , _) (g , _) = funext∙ (Susp-elim _ refl refl (λ x i j → merid (f (g x)) i)) (sym (∙-idl _)) Susp-map∙-zero : Susp-map∙ (zero∙ {A = A∙} {B = B∙}) ≡ zero∙ Susp-map∙-zero {B∙ = B , b₀} = funext∙ (Susp-elim _ refl (sym (merid b₀)) λ a i j → merid b₀ (i ∧ ~ j)) refl
Susp-Maps∙ : Maps∙ A∙ B∙ →∙ Maps∙ (Σ¹ A∙) (Σ¹ B∙) Susp-Maps∙ .fst = Susp-map∙ Susp-Maps∙ {A∙ = A∙} {B∙ = B∙} .snd = Susp-map∙-zero {A∙ = A∙} {B∙ = B∙} Susp-ap : A ≃ B → Susp A ≃ Susp B Susp-ap e .fst = Susp-map (e .fst) Susp-ap e .snd = is-iso→is-equiv λ where .is-iso.from → Susp-elim _ north south (λ x → merid (Equiv.from e x)) .is-iso.rinv → Susp-elim _ refl refl (λ x i j → merid (Equiv.ε e x j) i) .is-iso.linv → Susp-elim _ refl refl (λ x i j → merid (Equiv.η e x j) i) Susp-ap∙ : A∙ ≃∙ B∙ → Σ¹ A∙ ≃∙ Σ¹ B∙ Susp-ap∙ (e , pt) .fst = Susp-ap e Susp-ap∙ (e , pt) .snd = refl
Diagrams are hard, okay?!↩︎