Homotopy groups of spheres up to their dimension #
The unit sphere Sⁿ of an (n + 1)-dimensional real normed space is (n - 1)-connected:
πₖ(Sⁿ, x) is trivial for every k < n, in every degree including π₀
(TauCeti.subsingleton_homotopyGroup_sphere_of_lt). Consequently, by the Hurewicz theorem and
the homology of spheres, πₙ(Sⁿ, x) ≅ ℤ for n ≥ 2 (TauCeti.homotopyGroupSphereAddEquiv),
the double Moore loop space of S³ has first integral homology ℤ
(TauCeti.MooreLoopSpace.doubleFirstHomologySphereAddEquiv), and for m ≥ 4 the double Moore loop
space of Sᵐ has integral homology ℤ in degree m - 2
(TauCeti.MooreLoopSpace.doubleHomologySphereAddEquiv). In particular πₙ(Sⁿ, x) is nontrivial
for n ≥ 2 (TauCeti.nontrivial_homotopyGroup_sphere). In degree zero, as π₂(S²) ≅ ℤ,
the double Moore loop space of S²
has one path component for each integer, and its reduced zeroth homology is the coproduct of copies
of the coefficients indexed by the nonzero integers
(TauCeti.MooreLoopSpace.doubleReducedHomology₀SphereIso); with coefficients in a ring R it
contains a copy of R, so an infinite cyclic subgroup for R = ℤ
(TauCeti.MooreLoopSpace.exists_injective_doubleReducedHomology₀_sphere).
The vanishing follows from cellular compression, as in Hatcher's Corollary 4.12. The sphere
Sⁿ has a CW structure with one 0-cell and one n-cell (TauCeti.sphereCWComplex), so its
(n - 1)-skeleton is a single point. The inclusion of that skeleton is surjective on πₖ for
k ≤ n - 1 (TauCeti.surjective_homotopyGroupMap_skeletonLT), so πₖ(Sⁿ) is trivial at the
0-cell, and hence at every base point since Sⁿ is path connected. Spheres of normed spaces are
reduced to Euclidean ones through TauCeti.sphereHomeomorphOfFinrankEq.
The isomorphism πₙ(Sⁿ, x) ≅ ℤ is the cubical Hurewicz isomorphism
HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv followed by the identification
TauCeti.reducedSingularHomologySphereIso of Hₙ(Sⁿ; ℤ) with ℤ determined by an orthonormal
basis, so its sign depends on the orientation of that basis.
Main declarations #
TauCeti.subsingleton_homotopyGroup_sphere_of_lt:πₖ(Sⁿ, x)is trivial fork < n.TauCeti.homotopyGroupSphereAddEquiv:πₙ(Sⁿ, x) ≅ ℤforn ≥ 2, given an orthonormal basis.TauCeti.MooreLoopSpace.doubleFirstHomologySphereAddEquiv:H₁(ΩᴹΩᴹS³; ℤ) ≅ ℤ.TauCeti.MooreLoopSpace.doubleHomologySphereAddEquiv:Hₘ₋₂(ΩᴹΩᴹSᵐ; ℤ) ≅ ℤform ≥ 4.TauCeti.MooreLoopSpace.doubleReducedHomology₀SphereIso:H~₀(ΩᴹΩᴹS²; R) ≅ ∐_{k ≠ 0} R, with generator[γ] - [1]at the integer class ofγ(TauCeti.MooreLoopSpace.ι_doubleReducedHomology₀SphereIso_inv_ι).
References #
- A. Hatcher, Algebraic Topology, Section 4.1, Corollaries 4.9 and 4.12, and Section 4.2, Corollary 4.25.
- J.-F. Barraud, M. Damian, V. Humilière, A. Oancea, Floer homology with DG coefficients. Applications to cotangent bundles, arXiv:2404.07953, Propositions 5.11 and 6.21.
Spheres are (n - 1)-connected (Hatcher, Corollary 4.9). For the unit sphere Sⁿ of an
(n + 1)-dimensional real normed space, the homotopy set πₖ(Sⁿ, x) is trivial for every
k = Nat.card N < n. In degree zero this says that Sⁿ is path connected for n ≥ 1.
The n-th homotopy group of Sⁿ is ℤ for n ≥ 2 (Hatcher, Corollary 4.25). For the
unit sphere of a real inner product space with an orthonormal basis b indexed by Fin (n + 3),
this is the cubical Hurewicz isomorphism π_{n+2}(S^{n+2}, x) ≅ H_{n+2}(S^{n+2}; ℤ) followed by
the identification of H_{n+2}(S^{n+2}; ℤ) with ℤ determined by b.
Instances For
TauCeti.homotopyGroupSphereAddEquiv is the cubical Hurewicz isomorphism followed by the
identification of the top homology of the sphere with ℤ.
The first homology of the double loop space of S³ is ℤ. For the unit sphere S³ of
a real inner product space with an orthonormal basis b indexed by Fin 4, the first integral
homology of the double Moore loop space ΩᴹΩᴹS³ is π₃(S³) ≅ ℤ, through degree-one Hurewicz
(TauCeti.MooreLoopSpace.doubleFirstHomologyAddEquiv) and
TauCeti.homotopyGroupSphereAddEquiv.
Instances For
TauCeti.MooreLoopSpace.doubleFirstHomologySphereAddEquiv is the inverse of degree-one
Hurewicz for the double Moore loop space followed by TauCeti.homotopyGroupSphereAddEquiv.
The double loop space of Sⁿ⁺⁴ has homology ℤ in degree n + 2. For the unit sphere
Sⁿ⁺⁴ of a real inner product space with an orthonormal basis b indexed by Fin (n + 5), the
integral homology of the double Moore loop space ΩᴹΩᴹSⁿ⁺⁴ in degree n + 2 is
πₙ₊₄(Sⁿ⁺⁴) ≅ ℤ, through the Hurewicz identification
TauCeti.MooreLoopSpace.doubleHomologyAddEquiv and TauCeti.homotopyGroupSphereAddEquiv.
Instances For
TauCeti.MooreLoopSpace.doubleHomologySphereAddEquiv is the inverse of the Hurewicz
identification for the double Moore loop space followed by
TauCeti.homotopyGroupSphereAddEquiv.
πₙ(Sⁿ) is nontrivial for n ≥ 2: for the unit sphere Sⁿ⁺² of an
(n + 3)-dimensional real normed space, πₙ₊₂(Sⁿ⁺², x) is nontrivial.
Reduced zeroth homology of the double loop space of S². For the unit sphere S² of a
real inner product space with an orthonormal basis b indexed by Fin 3, the reduced zeroth
homology H~₀(ΩᴹΩᴹS²; R) is the coproduct of copies of R indexed by the nonzero integers: the
path components of ΩᴹΩᴹS² are the elements of π₂(S²) ≅ ℤ
(TauCeti.homotopyGroupSphereAddEquiv).
Instances For
The generator of TauCeti.MooreLoopSpace.doubleReducedHomology₀SphereIso at the integer
π₂(S²) ≅ ℤ assigns to the class of a double Moore loop γ is [γ] - [1].
The generator of TauCeti.MooreLoopSpace.doubleReducedHomology₀SphereIso at the integer
π₂(S²) ≅ ℤ assigns to the class of a double Moore loop γ is [γ] - [1].
The reduced zeroth homology of ΩᴹΩᴹS² contains the coefficients. For the unit sphere
S² of a real normed space of dimension three and a ring R, the kernel of the augmentation
H₀(ΩᴹΩᴹS²; R) → H₀(pt; R) contains a copy of R; for R = ℤ this is an infinite cyclic
subgroup.