pi_6 of the 3-sphere is Z/12

pi6_sphere_three_mulEquiv_zmod_twelve

Submitter: Vasily Ilin.

Notes: The earliest homotopy group of a sphere to have composite order (shared with the isomorphic pi_6(S^2)), beyond the stems covered by the existing benchmark problems in LeanEval.Topology.HomotopyGroups. The 2-primary component Z/4 is generated by Toda's nu-prime and the 3-primary component Z/3 by the first alpha element, so no route avoids serious composition methods or mod-p spectral sequences. Statement style follows LeanEval.Topology.HomotopyGroups.

Source: H. Toda, 'Composition Methods in Homotopy Groups of Spheres', Annals of Mathematics Studies 49, Princeton University Press, 1962. The value pi_6(S^3) = Z/12 also appears in the tables of A. Hatcher, 'Algebraic Topology', Section 4.1.

Informal solution: Via the James fibrations / EHP sequence or the mod-p Serre spectral sequence: the 2-component of pi_6(S^3) is Z/4, generated by Toda's nu-prime, with 2 nu-prime = eta cubed; the 3-component is Z/3, generated by the first alpha element alpha_1(3), the initial p-torsion of pi_*(S^3) for p = 3 appearing in degree 2p = 6. Combining the two components gives Z/12.

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

Solved by

Not yet solved.