module Homotopy.Space.Sphere.Properties where

Properties of higher spheres🔗

We can put together what we know about of a suspension and about the fundamental group of the circle to show that

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 and assert that the equivalence above takes it to the number 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

Note that the Hopf fibration defined for an arbitrary H-space specialises in this case to the classical Hopf fibration over with fibre and total space 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 to the meridian passing through we get a dependent path connecting to over the automorphism of the circle given by multiplication with i.e. an identification in

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

In turn, applying this function to the loop in yields, after cancelling out an equality 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, Recall the equivalence 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 is equivalent to the join of copies of hence, that is equivalent to

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¹∗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 under and specialising to the gives us a map 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 is large enough.

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

The Freudenthal suspension theorem implies that, if the of agrees with that of with the map 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 whenever

  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 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,

πₙSⁿ≃Int :  n   πₙ₊₁ n (Sⁿ (suc n))     
πₙSⁿ≃Int 0 =
    Ω¹ (Sⁿ 1)  ∥₀      ≃⟨ ∥-∥₀-ap (Ωⁿ-ap 1 SuspS⁰≃∙S¹ .fst) 
    Ω¹ ( , base)  ∥₀ ≃⟨ Equiv.inverse (_ , ∥-∥₀-idempotent (hlevel 2)) 
   Ω¹ ( , 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 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)