The cubical Hurewicz isomorphism

Let X be (m - 1)-connected at x, in the sense that πₖ(X, x) is trivial for every k < m. Eilenberg's coherent deformation retracts the normalized cubical chains of X onto the chains spanned by m-based cubes. In degree m, these cubes are precisely generalized loops. The face relation identifies the resulting quotient by boundaries with πₘ(X, x).

This file carries out that last step when m ≥ 2. Retraction onto based cubes proves surjectivity, while applying the based-cube class map to a bounding chain proves injectivity. The resulting bijection is packaged as an additive equivalence.

The inductive Hurewicz criterion TauCeti.subsingleton_homotopyGroup_of_isZero_homology_normalizedCubicalChainComplex shows that a simply connected space with vanishing integral normalized cubical homology in degrees at least two has trivial homotopy groups in every degree.

References

• S. Eilenberg, Singular homology theory, Ann. of Math. (2) 45 (1944), 407--447.
• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter II.
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 4.32.

noncomputable def HomotopyGroup.cubicalHurewiczAddEquiv {X : Type} [TopologicalSpace X] {x : X} {n : ℕ} (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) X x)) : Additive (HomotopyGroup (Fin (n + 2)) X x) ≃+ ↑(HomologicalComplex.homology ((TauCeti.normalizedCubicalChainComplex ℤ).obj ↧X) (n + 2))

The cubical Hurewicz isomorphism. If πₖ(X, x) is trivial for every k < n + 2, then the degree-n + 2 cubical Hurewicz homomorphism is an additive equivalence from π_{n+2}(X, x) to normalized cubical homology.

@[simp]

theorem HomotopyGroup.cubicalHurewiczAddEquiv_apply {X : Type} [TopologicalSpace X] {x : X} {n : ℕ} (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) X x)) (a : Additive (HomotopyGroup (Fin (n + 2)) X x)) : (cubicalHurewiczAddEquiv hX) a = (cubicalHurewiczHom ℤ (n + 1)) a

The cubical Hurewicz equivalence has the cubical Hurewicz homomorphism as its forward map.

theorem TauCeti.subsingleton_homotopyGroup_of_isZero_homology_normalizedCubicalChainComplex {X : Type} [TopologicalSpace X] (x : X) [PathConnectedSpace X] [Subsingleton (HomotopyGroup.Pi 1 X x)] (hH : ∀ (n : ℕ), CategoryTheory.Limits.IsZero (HomologicalComplex.homology ((normalizedCubicalChainComplex ℤ).obj ↧X) (n + 2))) (k : ℕ) : Subsingleton (HomotopyGroup.Pi k X x)

Inductive Hurewicz vanishing criterion (normalized cubical homology). If X is path connected with trivial π_ 1 X x and its integral normalized cubical homology vanishes in every degree n + 2, then all homotopy groups π_ k X x are trivial.