pi_(n+1) of S^n is Z/2 for n at least 3

pi_succ_sphere_n_mulEquiv_zmod_two

Submitter: Kim Morrison.

Notes: A concrete stable-family homotopy-group computation.

Source: Classical theorem in unstable homotopy theory.

Informal solution: Use suspension and the stable range to show the first stable stem is Z/2.

theorem declaration uses `sorry`pi_succ_sphere_n_mulEquiv_zmod_two (n : ℕ) (hn : 3 ≤ n)
    (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :
    Nonempty
      (HomotopyGroup.Pi (n + 1) (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) x ≃*
        Multiplicative (ZMod 2)) := byn:ℕhn:3 ≤ nx:↑(Metric.sphere 0 1)⊢ Nonempty (HomotopyGroup.Pi (n + 1) (↑(Metric.sphere 0 1)) x ≃* Multiplicative (ZMod 2))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.