open import Algebra.Group.Instances.Integers
open import Algebra.Group.Cat.Base
open import Algebra.Group.Concrete
open import Algebra.Group.Homotopy
open import Algebra.Group

open import Cat.Functor.Base
open import Cat.Prelude

open import Data.Nat.Properties
open import Data.Set.Truncation
open import Data.Nat.Order
open import Data.Int.Base
open import Data.Nat.Base

open import Homotopy.Space.Suspension.Freudenthal
open import Homotopy.Space.Suspension.Properties
open import Homotopy.Space.Circle.Properties
open import Homotopy.Space.Suspension
open import Homotopy.Space.Circle
open import Homotopy.Space.Sphere
open import Homotopy.Conjugation
open import Homotopy.Truncation
open import Homotopy.Loopspace
open import Homotopy.HSpace
open import Homotopy.Base
open import Homotopy.Join

import Cat.Reasoning

import Homotopy.Space.Suspension.Pi2

module Homotopy.Space.Sphere.Properties where

Properties of higher spheres🔗

We can put together what we know about $π_{2}$ of a suspension and about the fundamental group $π_{1} (S^{1})$ of the circle to show that $π_{2} (S^{2}) ≅ Z .$

open Homotopy.Space.Suspension.Pi2 S¹-concrete HSpace-S¹

opaque
  π₂S²≅ℤ : πₙ₊₁ 1 (Sⁿ 2) Groups.≅ ℤ
  π₂S²≅ℤ = π₁S¹≅ℤ
    Groups.∘Iso π₂ΣG≅ΩG
    Groups.∘Iso πₙ₊₁-ap 1 (Susp-ap∙ SuspS⁰≃∙S¹)

The inverse to this equivalence, turning integers into 2-loops on the sphere, is constructed purely abstractly and thus too horrible to compute with. However, the forward map, giving the winding numbers of 2-loops, is more tractable. We can write down an explicit generator for $π_{2} (S^{2})$ and assert that the equivalence above takes it to the number $1$ by computation.

private opaque
  unfolding conj conj-refl π₂S²≅ℤ ΩΣG≃G n-Tr-Ω¹ Ω¹-ap

  gen : Path (Path ⌞ Sⁿ 2 ⌟ north north) refl refl
  gen i j = hcomp (∂ i ∨ ∂ j) λ where
    k (k = i0) → merid (suspend (Sⁿ 0) south (~ j)) i
    k (i = i0) → north
    k (i = i1) → merid north (~ k)
    k (j = i0) → merid north (~ k ∧ i)
    k (j = i1) → merid north (~ k ∧ i)

  π₂S²≅ℤ-computes : Groups.to π₂S²≅ℤ · inc gen ≡ 1
  π₂S²≅ℤ-computes = refl

  {-
  Checking Homotopy.Space.Sphere.Properties (…).
  Total                                            6,655ms
  Homotopy.Space.Sphere.Properties.π₂S²≅ℤ-computes 1,073ms
  -}

Note that the Hopf fibration defined for an arbitrary H-space specialises in this case to the classical Hopf fibration over $S^{2},$ with fibre $S^{1}$ and total space $S^{3} .$ We prove that the Hopf fibration does not have a section.

Hopf-nontrivial : ¬ ∀ x → Hopf x
Hopf-nontrivial s = never-refl _ loop≡refl where

First, observe what happens when we apply a section $s : (x : S^{2}) \to Hopf (x)$ to the meridian $N \equiv S$ passing through $y : S^{1} :$ we get a dependent path connecting $s (N)$ to $s (S)$ over the automorphism of the circle given by multiplication with $y,$ i.e. an identification $μ (y, s (N)) \equiv s (S)$ in $S^{1} .$

  f : (y : S¹) → mulS¹ y (s north) ≡ s south
  f y = mulS¹-comm y _ ∙ ua-pathp→path _ (ap s (merid y))

In turn, applying this function $f$ to the loop in $S^{1}$ yields, after cancelling out $f (base),$ an equality $loop_{s (N)} \equiv refl_{s (N)},$ which is impossible as these have different winding numbers.

  loop≡refl : always-loop (s north) ≡ refl
  loop≡refl = sym (square→conj (transpose (flip₂ (ap f loop))))
            ∙ conj-of-refl _

We can also characterise more precisely the total space of the Hopf fibration, $S^{1} * S^{1} .$ Recall the equivalence $S^{0} * A ≃ Σ A$ between the join with a two-element type and the suspension. Iterating this and remembering that the join of types is associative, we find that $S^{n}$ is equivalent to the join of $n + 1$ copies of $S^{0};$ hence, that $S^{n} * S^{m}$ is equivalent to $S^{n + m + 1} .$

join-of-spheres : ∀ {n m} → ⌞ Sⁿ n ⌟ ∗ ⌞ Sⁿ m ⌟ ≃ ⌞ Sⁿ (1 + n + m) ⌟
join-of-spheres {zero} {m} =
  ⌞ Sⁿ 0 ⌟ ∗ ⌞ Sⁿ m ⌟ ≃⟨ join-ap SuspS⁻¹≃S⁰ id≃ ⟩
  S⁰ ∗ ⌞ Sⁿ m ⌟       ≃⟨ 2∗≡Susp ⟩
  ⌞ Sⁿ (1 + m) ⌟      ≃∎
join-of-spheres {suc n} {m} =
  ⌞ Sⁿ (suc n) ⌟ ∗ ⌞ Sⁿ m ⌟  ≃˘⟨ join-ap 2∗≡Susp id≃ ⟩
  (S⁰ ∗ ⌞ Sⁿ n ⌟) ∗ ⌞ Sⁿ m ⌟ ≃⟨ join-associative ⟩
  S⁰ ∗ (⌞ Sⁿ n ⌟ ∗ ⌞ Sⁿ m ⌟) ≃⟨ join-ap id≃ (join-of-spheres {n} {m}) ⟩
  S⁰ ∗ ⌞ Sⁿ (1 + n + m) ⌟    ≃⟨ 2∗≡Susp ⟩
  ⌞ Sⁿ (2 + n + m) ⌟         ≃∎

We conclude that the total space of the Hopf fibration is $S^{3} .$

S¹∗S¹≃S³ : S¹ ∗ S¹ ≃ ⌞ Sⁿ 3 ⌟
S¹∗S¹≃S³ = join-ap SuspS⁰≃S¹ SuspS⁰≃S¹ e⁻¹ ∙e join-of-spheres

∫Hopf≃S³ : Σ _ Hopf ≃ ⌞ Sⁿ 3 ⌟
∫Hopf≃S³ = ∫Hopf≃join ∙e S¹∗S¹≃S³

Stability for spheres🔗

Applying the unit of the suspension–loop space adjunction $σ : A \to_{*} Ω Σ A$ under $Ω^{k}$ and specialising $A$ to the $n -sphere$ gives us a map $Ω^{k} σ : Ω^{k} S^{n} \to_{*} Ω^{k + 1} S^{n + 1} .$ In this section, we will show that this map induces an isomorphism of set truncations (hence of homotopy groups, although we do not prove this) when $n$ is large enough.

Ωⁿ-suspend : ∀ {ℓ} k (A : Type∙ ℓ) → Ωⁿ k A →∙ Ωⁿ (suc k) (Σ¹ A)
Ωⁿ-suspend k A = Equiv∙.from∙ (Ωⁿ-suc (Σ¹ A) k) ∘∙ Ωⁿ-map k (suspend∙ A)

Ωⁿ-suspend-natural
  : ∀ {ℓa ℓb} {A : Type∙ ℓa} {B : Type∙ ℓb} k (f : A →∙ B)
  → Ωⁿ-map (suc k) (Susp-map∙ f) ∘∙ Ωⁿ-suspend k A
  ≡ Ωⁿ-suspend k B ∘∙ Ωⁿ-map k f
Ωⁿ-suspend-natural {A = A} {B = B} k f = homogeneous-funext∙ λ l →
  Ωⁿ-map (suc k) (Susp-map∙ f) · (Equiv∙.from∙ (Ωⁿ-suc (Σ¹ A) k) · (Ωⁿ-map k (suspend∙ A) · l))
    ≡⟨ Equiv.adjunctl (Ωⁿ-suc _ k .fst) (Ω-suc-natural k (Susp-map∙ f) ·ₚ _) ⟩
  Equiv∙.from∙ (Ωⁿ-suc (Σ¹ B) k) · ⌜ Ωⁿ-map k (Ω¹-map (Susp-map∙ f)) · (Ωⁿ-map k (suspend∙ A) · l) ⌝
    ≡⟨ ap! (Ωⁿ-map-∘ k _ (suspend∙ A) ·ₚ l) ⟩
  Equiv∙.from∙ (Ωⁿ-suc (Σ¹ B) k) · (Ωⁿ-map k ⌜ Ω¹-map (Susp-map∙ f) ∘∙ suspend∙ A ⌝ · l)
    ≡⟨ ap! (suspend∙-natural f) ⟩
  Equiv∙.from∙ (Ωⁿ-suc (Σ¹ B) k) · ⌜ Ωⁿ-map k (suspend∙ B ∘∙ f) · l ⌝
    ≡˘⟨ ap¡ (Ωⁿ-map-∘ k (suspend∙ B) f ·ₚ l) ⟩
  Equiv∙.from∙ (Ωⁿ-suc (Σ¹ B) k) · (Ωⁿ-map k (suspend∙ B) · (Ωⁿ-map k f · l))
    ∎

The Freudenthal suspension theorem implies that, if $0 < k \leq 2 n,$ the $k -truncation$ of $Ω S^{n + 1}$ agrees with that of $S^{n},$ with the map $σ : S^{n} \to_{*} Ω S^{n + 1}$ mediating between the two up to truncation inclusion.

opaque
  Sⁿ-stability-n-Tr
    : ∀ n k (p : suc k ≤ (suc n + suc n))
    → n-Tr∙ (Sⁿ (1 + n)) (suc k) ≃∙ n-Tr∙ (Ω¹ (Sⁿ (2 + n))) (suc k)
  Sⁿ-stability-n-Tr n k p =
    n-Tr∙ (Sⁿ (1 + n)) (suc k)
      ≃∙˘⟨ n-Tr-Tr (≤-peel p) , refl ⟩
    n-Tr∙ (n-Tr∙ (Sⁿ (1 + n)) (suc n + suc n)) (suc k)
      ≃∙⟨ (let e , p = freudenthal-equivalence {A∙ = Sⁿ (suc n)} n (Sⁿ⁻¹-is-connected (2 + n)) in n-Tr-ap {n = k} e , ap n-Tr.inc p) ⟩
    n-Tr∙ (n-Tr∙ (Ω¹ (Σ¹ (Sⁿ (1 + n)))) (suc n + suc n)) (suc k)
      ≃∙⟨⟩
    n-Tr∙ (n-Tr∙ (Ω¹ (Sⁿ (2 + n))) (suc n + suc n)) (suc k)
      ≃∙⟨ n-Tr-Tr (≤-peel p) , refl ⟩
    n-Tr∙ (Ω¹ (Sⁿ (2 + n))) (suc k)
      ≃∙∎

  Sⁿ-stability-n-Tr-suspend
    : ∀ n k (p : suc k ≤ (suc n + suc n))
    → Equiv∙.to∙ (Sⁿ-stability-n-Tr n k p) ∘∙ inc∙
    ≡ inc∙ ∘∙ suspend∙ (Sⁿ (1 + n))
  Sⁿ-stability-n-Tr-suspend n k p = homogeneous-funext∙ λ _ → refl

Thus, by swapping loop spaces and truncations, we obtain an isomorphism of sets $π_{k} (S^{n}) ≃ π_{k + 1} (S^{n + 1})$ whenever $0 < k \leq 2 (n - 1) .$

module _ n k (p : suc k ≤ n + n) where
  private abstract
    p' : suc (k + 2) ≤ suc n + suc n
    p' = s≤s
       $ ≤-trans (≤-refl' (+-commutative k 2))
       $ ≤-trans (s≤s p)
       $ ≤-refl' (+-commutative (suc n) n)

  opaque
    Sⁿ-stability
      : ⌞ πₙ₊₁ (1 + k) (Sⁿ (2 + n)) ⌟ ≃ ⌞ πₙ₊₁ k (Sⁿ (1 + n)) ⌟
    Sⁿ-stability =
      ⌞ πₙ₊₁ (1 + k) (Sⁿ (2 + n)) ⌟
        ≃⟨ πₙ-def (Sⁿ (2 + n)) (1 + k) .fst ⟩
      ⌞ Ωⁿ (2 + k) (n-Tr∙ (Sⁿ (2 + n)) (2 + k + 2)) ⌟
        ≃⟨ Ωⁿ-suc (n-Tr∙ (Sⁿ (2 + n)) (2 + k + 2)) (1 + k) .fst ⟩
      ⌞ Ωⁿ (1 + k) (Ω¹ (n-Tr∙ (Sⁿ (2 + n)) (2 + k + 2))) ⌟
        ≃˘⟨ Ωⁿ-ap (1 + k) (n-Tr-Ω¹ (Sⁿ (2 + n)) (k + 2)) .fst ⟩
      ⌞ Ωⁿ (1 + k) (n-Tr∙ (Ω¹ (Sⁿ (2 + n))) (1 + k + 2)) ⌟
        ≃˘⟨ Ωⁿ-ap (1 + k) (Sⁿ-stability-n-Tr n (k + 2) p') .fst ⟩
      ⌞ Ωⁿ (1 + k) (n-Tr∙ (Sⁿ (1 + n)) (1 + k + 2)) ⌟
        ≃˘⟨ πₙ-def (Sⁿ (1 + n)) k .fst ⟩
      ⌞ πₙ₊₁ k (Sⁿ (1 + n)) ⌟
        ≃∎

We again check that the inverse map of this equivalence is the expected suspension map.

    Sⁿ-stability-suspend
      : Equiv.from Sⁿ-stability ⊙ inc
      ≡ ∥_∥₀.inc ⊙ Ωⁿ-suspend (suc k) (Sⁿ (suc n)) .fst

This boils down to chasing an element of

Ω^{k} S^{n}

through every step of the equivalence above, which we express as an annoying chain of pointed equivalences.

    Sⁿ-stability-suspend = ext λ l → trace l .snd where
      trace
        : (l : ⌞ Ωⁿ (1 + k) (Sⁿ (1 + n)) ⌟)
        →  (⌞ πₙ₊₁ k (Sⁿ (1 + n)) ⌟ , inc l)
        ≃∙ (⌞ πₙ₊₁ (1 + k) (Sⁿ (2 + n)) ⌟ , inc (Ωⁿ-suspend (suc k) (Sⁿ (suc n)) · l))
      trace l =
        ⌞ πₙ₊₁ k (Sⁿ (1 + n)) ⌟ ,
          inc l
            ≃∙⟨ πₙ-def (Sⁿ (1 + n)) k .fst , πₙ-def-inc _ k l ⟩
        ⌞ Ωⁿ (1 + k) (n-Tr∙ (Sⁿ (1 + n)) (1 + k + 2)) ⌟ ,
          Ωⁿ-map (1 + k) inc∙ · l
            ≃∙⟨ Ωⁿ-ap (1 + k) (Sⁿ-stability-n-Tr n (k + 2) p') .fst
              , (Ωⁿ-map-∘ (1 + k) (Equiv∙.to∙ (Sⁿ-stability-n-Tr n (k + 2) p')) inc∙ ·ₚ l)
              ∙ ap (λ x → Ωⁿ-map (1 + k) x · l) (Sⁿ-stability-n-Tr-suspend n (k + 2) p') ⟩
        ⌞ Ωⁿ (1 + k) (n-Tr∙ (Ω¹ (Sⁿ (2 + n))) (1 + k + 2)) ⌟ ,
          Ωⁿ-map (1 + k) (inc∙ ∘∙ suspend∙ _) · l
            ≃∙⟨ Ωⁿ-ap (1 + k) (n-Tr-Ω¹ (Sⁿ (2 + n)) (k + 2)) .fst
              , Ωⁿ-map-∘ (1 + k) (Equiv∙.to∙ (n-Tr-Ω¹ _ (k + 2))) _ ·ₚ l ⟩
        ⌞ Ωⁿ (1 + k) (Ω¹ (n-Tr∙ (Sⁿ (2 + n)) (2 + k + 2))) ⌟ ,
          Ωⁿ-map (1 + k) (Equiv∙.to∙ (n-Tr-Ω¹ _ (k + 2)) ∘∙ inc∙ ∘∙ suspend∙ _) · l
            ≃∙⟨ id≃
              , ap (λ x → Ωⁿ-map (1 + k) x · l)
                ( sym (∘∙-assoc (Equiv∙.to∙ (n-Tr-Ω¹ _ (k + 2))) inc∙ (suspend∙ _))
                ∙ ap (_∘∙ suspend∙ _) (n-Tr-Ω¹-inc _ (k + 2)))
              ∙ sym (Ωⁿ-map-∘ (1 + k) _ _ ·ₚ l) ⟩
        ⌞ Ωⁿ (1 + k) (Ω¹ (n-Tr∙ (Sⁿ (2 + n)) (2 + k + 2))) ⌟ ,
          Ωⁿ-map (1 + k) (Ω¹-map inc∙) · (Ωⁿ-map (1 + k) (suspend∙ _) · l)
            ≃∙˘⟨ Ωⁿ-suc (n-Tr∙ (Sⁿ (2 + n)) (2 + k + 2)) (1 + k) .fst
               , Ω-suc-natural (1 + k) inc∙ ·ₚ _ ⟩
        ⌞ Ωⁿ (2 + k) (n-Tr∙ (Sⁿ (2 + n)) (2 + k + 2)) ⌟ ,
          Ωⁿ-map (2 + k) inc∙ · (Ωⁿ-suspend (suc k) (Sⁿ (suc n)) · l)
            ≃∙˘⟨ πₙ-def (Sⁿ (2 + n)) (1 + k) .fst
               , πₙ-def-inc _ (suc k) _ ⟩
        ⌞ πₙ₊₁ (1 + k) (Sⁿ (2 + n)) ⌟ ,
          inc (Ωⁿ-suspend (suc k) (Sⁿ (suc n)) · l)
            ≃∙∎

As a corollary, $π_{n} (S^{n}) ≃ Z .$

πₙSⁿ≃Int : ∀ n → ⌞ πₙ₊₁ n (Sⁿ (suc n)) ⌟ ≃ ⌞ ℤ ⌟
πₙSⁿ≃Int 0 =
  ∥ ⌞ Ω¹ (Sⁿ 1) ⌟ ∥₀      ≃⟨ ∥-∥₀-ap (Ωⁿ-ap 1 SuspS⁰≃∙S¹ .fst) ⟩
  ∥ ⌞ Ω¹ (S¹ , base) ⌟ ∥₀ ≃⟨ Equiv.inverse (_ , ∥-∥₀-idempotent (hlevel 2)) ⟩
  ⌞ Ω¹ (S¹ , base) ⌟      ≃⟨ ΩS¹≃Int ⟩
  Int                     ≃∎

πₙSⁿ≃Int 1 = Iso→Equiv (i.to , iso i.from (happly i.invl) (happly i.invr)) where
  module i = Cat.Reasoning._≅_ (Sets lzero) (F-map-iso (Forget-structure _) π₂S²≅ℤ)

πₙSⁿ≃Int (suc (suc n)) =
  ⌞ πₙ₊₁ (2 + n) (Sⁿ (3 + n)) ⌟ ≃⟨ Sⁿ-stability (1 + n) (1 + n) (s≤s (+-≤r n (1 + n))) ⟩
  ⌞ πₙ₊₁ (1 + n) (Sⁿ (2 + n)) ⌟ ≃⟨ πₙSⁿ≃Int (suc n) ⟩
  ⌞ ℤ ⌟                         ≃∎

Furthermore, the isomorphisms $π_{n} (S^{n}) ≃ Z$ are compatible with the suspension maps Ωⁿ-suspend, in the sense that the following diagram of isomorphisms commutes:

opaque
  unfolding π₂S²≅ℤ

  πₙSⁿ≃Int-suspend
    : ∀ n (l : ⌞ Ωⁿ (suc n) (Sⁿ (suc n)) ⌟)
    → πₙSⁿ≃Int (suc n) · inc (Ωⁿ-suspend (suc n) (Sⁿ (suc n)) · l)
    ≡ πₙSⁿ≃Int n · inc l
  πₙSⁿ≃Int-suspend zero l =
    ΩS¹≃Int · (Ω²ΣG≃ΩG · ∥_∥₀.inc ⌜ Ωⁿ-map 2 (Susp-map∙ SuspS⁰→∙S¹) · (Ωⁿ-suspend 1 (Sⁿ 1) · l) ⌝)
      ≡⟨ ap! (Ωⁿ-suspend-natural 1 SuspS⁰→∙S¹ ·ₚ l) ⟩
    ΩS¹≃Int · (Ω²ΣG≃ΩG · ∥_∥₀.inc ⌜ Ωⁿ-suspend 1 _ · (Ω¹-map SuspS⁰→∙S¹ · l) ⌝)
      ≡⟨ ap! (transport-refl _) ⟩
    ΩS¹≃Int · ⌜ Ω²ΣG≃ΩG · ∥_∥₀.inc (Ω¹-map (suspend∙ _) · (Ω¹-map SuspS⁰→∙S¹ · l)) ⌝
      ≡⟨ ap! (Equiv.adjunctr Ω²ΣG≃ΩG (sym (Ω²ΣG≃ΩG-inv (Ω¹-map SuspS⁰→∙S¹ · l)))) ⟩
    ΩS¹≃Int · (Ω¹-map SuspS⁰→∙S¹ · l)
      ∎
  πₙSⁿ≃Int-suspend (suc n) l =
    ap (πₙSⁿ≃Int (1 + n) .fst) $
    Equiv.adjunctr (Sⁿ-stability (1 + n) (1 + n) _) $
    sym (Sⁿ-stability-suspend (1 + n) (1 + n) _ $ₚ l)