Serre finiteness for homotopy groups of spheres
pi_sphere_infinite_iff
Submitter: Vasily Ilin.
Notes: A two-way characterization of infinitude: pi_k(S^n) is infinite exactly at k = n and, for even n, at k = 2n-1 (phrased as k + 1 = 2*n to avoid truncated subtraction). The forward direction packages all of Serre's finiteness statements; the backward direction requires exhibiting infinitely many homotopy classes, i.e. degree theory for k = n and a Hopf-invariant or Whitehead-product argument for k = 2n-1 with n even. Quantifying over all k means no finiteness case can be dodged. The hypothesis 1 <= n is necessary: at n = k = 0 the right-hand side holds but pi_0(S^0) is a two-element set. Explicit basepoints follow LeanEval.Topology.HomotopyGroups.
Source: J.-P. Serre, 'Homologie singuliere des espaces fibres. Applications', Ann. of Math. 54 (1951), 425-505; J.-P. Serre, 'Groupes d'homotopie et classes de groupes abeliens', Ann. of Math. 58 (1953), 258-294. See also A. Hatcher, 'Spectral Sequences in Algebraic Topology', Theorem 1.21.
Informal solution: Serre class theory applied to the spectral sequences of the path-loop fibrations and Eilenberg-MacLane spaces shows that pi_k(S^n) is finitely generated, and that rationally pi_k(S^n) tensor Q is Q for k = n, and additionally Q for k = 2n-1 when n is even, and 0 otherwise; this gives every finiteness claim. For the infinitude: the degree homomorphism shows pi_n(S^n) surjects onto Z, and for even n the Hopf invariant (equivalently the Whitehead product [iota, iota]) provides an element of infinite order in pi_{2n-1}(S^n).
theorem declaration uses `sorry`pi_sphere_infinite_iff (k n : ℕ) (hn : 1 ≤ n)
(x : Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) :
Infinite (HomotopyGroup.Pi k (Metric.sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) x) ↔
k = n ∨ (Even n ∧ k + 1 = 2 * n) := k:ℕn:ℕhn:1 ≤ nx:↑(Metric.sphere 0 1)⊢ Infinite (HomotopyGroup.Pi k (↑(Metric.sphere 0 1)) x) ↔ k = n ∨ Even n ∧ k + 1 = 2 * n
All goals completed! 🐙Solved by
Not yet solved.