open import 1Lab.Prelude

open import Homotopy.Space.Circle.Base
open import Homotopy.Space.Suspension

module Homotopy.Space.Sphere where

The -1 and 0 spheres🔗

In classical topology, the topological space $S^n$ is typically defined as the subspace of ${\mathbb{R}}^{n+1}$ consisting of all points at unit distance from the origin. We see from this definition that the $0\text{-sphere}$ is the discrete two point space $\{-1,1\}\subset \mathbb{R}\text{,}$ and that the $-1$ sphere is the empty subspace $\varnothing \subset \{0\}\text{.}$ We will recycle existing types and define:

S⁻¹ : Type
S⁻¹ = ⊥

S⁰ : Type
S⁰ = Bool

We note that S⁰ may be identified with Susp S⁻¹. Since the pattern matching checker can prove that merid x i is impossible when x : ⊥, the case for this constructor does not need to be written, this makes the proof look rather tautologous.

open is-iso

SuspS⁻¹≃S⁰ : Susp S⁻¹ ≃ S⁰
SuspS⁻¹≃S⁰ = SuspS⁻¹→S⁰ , is-iso→is-equiv iso-pf where
  SuspS⁻¹→S⁰ : Susp S⁻¹ → S⁰
  SuspS⁻¹→S⁰ north = true
  SuspS⁻¹→S⁰ south = false

  S⁰→SuspS⁻¹ : S⁰ → Susp S⁻¹
  S⁰→SuspS⁻¹ true = north
  S⁰→SuspS⁻¹ false = south

  iso-pf : is-iso SuspS⁻¹→S⁰
  iso-pf .from = S⁰→SuspS⁻¹
  iso-pf .rinv false = refl
  iso-pf .rinv true = refl
  iso-pf .linv north = refl
  iso-pf .linv south = refl

n-Spheres🔗

The spheres of higher dimension can be defined inductively: $S^{n+1}=\Sigma S^n\text{,}$ that is, suspending the $n\text{-sphere}$ constructs the $n+1\text{-sphere.}$

The spheres are essentially indexed by the natural numbers, except that we want to start at $-1$ instead of $0\text{.}$ To remind ourselves of this, we name our spheres with a superscript ${}^{n-1}\text{:}$

Sⁿ⁻¹ : Nat → Type
Sⁿ⁻¹ zero = S⁻¹
Sⁿ⁻¹ (suc n) = Susp (Sⁿ⁻¹ n)

By convention, the $n\text{-sphere}$ (for $n\ge 0\text{)}$ is considered as a pointed type with base point the north pole $N\text{.}$

Sⁿ : Nat → Type∙ lzero
Sⁿ n = Sⁿ⁻¹ (suc n) , north

A slightly less trivial example of definitions lining up is the verification that Sⁿ⁻¹ 2 is equivalent to our previous definition of S¹:

SuspS⁰≃S¹ : Sⁿ⁻¹  ≃ S¹
SuspS⁰≃S¹ = SuspS⁰→S¹ , is-iso→is-equiv iso-pf where

In Sⁿ⁻¹ 2, we have two point constructors joined by two paths, while in S¹ we have a single point constructor and a loop. Geometrically, we can picture morphing Sⁿ⁻¹ 2 into S¹ by squashing one of the meridians down to a point, thus bringing N and S together. This intuition leads to a definition:

  SuspS⁰→S¹ : Sⁿ⁻¹  → S¹
  SuspS⁰→S¹ north = base
  SuspS⁰→S¹ south = base
  SuspS⁰→S¹ (merid north i) = base
  SuspS⁰→S¹ (merid south i) = loop i

In the other direction, we send base to N, and then need to send loop to some path N ≡ N. Since this map should define an equivalence, we make it such that loop wraps around the space Sⁿ 2 by way of traversing both meridians.

  S¹→SuspS⁰ : S¹ → Sⁿ⁻¹ 
  S¹→SuspS⁰ base = north
  S¹→SuspS⁰ (loop i) = (merid south ∙ sym (merid north)) i

  iso-pf : is-iso SuspS⁰→S¹
  iso-pf .from = S¹→SuspS⁰
  iso-pf .rinv base = refl
  iso-pf .rinv (loop i) =
    ap (λ p → p i)
      (ap SuspS⁰→S¹ (merid south ∙ sym (merid north)) ≡⟨ ap-∙ SuspS⁰→S¹ (merid south) (sym (merid north))⟩≡
      loop ∙ refl                                     ≡⟨ ∙-idr _ ⟩≡
      loop                                            ∎)
  iso-pf .linv north = refl
  iso-pf .linv south = merid north
  iso-pf .linv (merid north i) j = merid north (i ∧ j)
  iso-pf .linv (merid south i) j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → merid south i
    k (i = i0) → north
    k (i = i1) → merid north (j ∨ ~ k)
    k (j = i0) → ∙-filler (merid south) (sym (merid north)) k i
    k (j = i1) → merid south i

SuspS⁰→∙S¹ : Sⁿ  →∙ S¹∙
SuspS⁰→∙S¹ = SuspS⁰≃S¹ .fst , refl

SuspS⁰≃∙S¹ : Sⁿ  ≃∙ S¹∙
SuspS⁰≃∙S¹ = SuspS⁰≃S¹ , refl