pi_3 of the 2-sphere is Z

pi3_sphere_two_mulEquiv_int

Submitter: Kim Morrison.

Notes: The classical computation pi_3(S^2) = Z, with an explicit basepoint.

Source: Classical theorem in algebraic topology.

Informal solution: Use the Hopf fibration to identify the third homotopy group of the 2-sphere with the integers.

theorem declaration uses `sorry`pi3_sphere_two_mulEquiv_int (x : Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) :
    Nonempty
      (HomotopyGroup.Pi 3 (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) x ≃*
        Multiplicative ℤ) := byx:↑(Metric.sphere 0 1)⊢ Nonempty (HomotopyGroup.Pi 3 (↑(Metric.sphere 0 1)) x ≃* Multiplicative ℤ)
  sorryAll goals completed! 🐙

Solved by

Not yet solved.