The cubical Hurewicz equivalence in singular homology

For an (n + 1)-connected pointed space, the cubical Hurewicz homomorphism in degree n + 2 is an additive equivalence. The natural chain-homotopy equivalence between simplicial and normalized cubical singular chains transports this to an equivalence with ordinary singular homology (HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv).

The resulting equivalence is natural in based maps; so is the transported cubical Hurewicz map itself, with no connectivity hypothesis (HomotopyGroup.singularCubicalHomologyIso_inv_cubicalHurewiczHom_naturality). It supplies the degree-n + 2 singular homology isomorphism, while TauCeti.isZero_singularHomologyFunctor_of_subsingleton_homotopyGroup supplies the positive lower-degree vanishing. The comparison here retains the cubical Hurewicz map as its forward description. The independently defined relative-fundamental-class map HomotopyGroup.hurewiczHom agrees with it up to a universal sign (HomotopyGroup.exists_hurewicz_eq_units_smul_cubicalHurewicz), which gives the Hurewicz theorem for hurewiczHom (HomotopyGroup.hurewiczAddEquiv).

The inductive Hurewicz criterion TauCeti.subsingleton_homotopyGroup_of_isZero_homology_singularChains shows that a simply connected space with vanishing integral singular 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, Chapters II and VII.
• A. Hatcher, Algebraic Topology, Cambridge University Press, 2002, Theorem 4.32.

noncomputable def HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv {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.singularChains ℤ).obj ↧X) (n + 2))

The cubical Hurewicz equivalence with ordinary singular homology. If πₖ(X, x) is trivial for every k < n + 2, then πₙ₊₂(X, x) is additively equivalent to degree-n + 2 singular homology with integer coefficients. Its forward map is the cubical Hurewicz homomorphism followed by the inverse cubical--simplicial homology comparison.

@[simp]

theorem HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv_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)) : (cubicalHurewiczSingularHomologyAddEquiv hX) a = (CategoryTheory.ConcreteCategory.hom (TauCeti.singularCubicalHomologyIso ℤ (↧X) (n + 2)).inv) ((cubicalHurewiczHom ℤ (n + 1)) a)

The cubical Hurewicz equivalence with singular homology sends a homotopy class to its cubical Hurewicz class, transported through the inverse cubical--simplicial comparison.

theorem HomotopyGroup.singularCubicalHomologyIso_inv_cubicalHurewiczHom_naturality {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {n : ℕ} (k : Type) [Ring k] (f : C(X, Y)) (hf : f x = y) (a : Additive (HomotopyGroup (Fin (n + 1)) X x)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((TauCeti.singularChains k).map (TopCat.ofHom f)) (n + 1))) ((CategoryTheory.ConcreteCategory.hom (TauCeti.singularCubicalHomologyIso k (↧X) (n + 1)).inv) ((cubicalHurewiczHom k n) a)) = (CategoryTheory.ConcreteCategory.hom (TauCeti.singularCubicalHomologyIso k (↧Y) (n + 1)).inv) ((cubicalHurewiczHom k n) (Additive.ofMul (map f hf (Additive.toMul a))))

The cubical Hurewicz class, transported to singular homology through the inverse cubical--simplicial comparison, is natural in based maps, for coefficients in any ring k. No connectivity hypothesis is needed.

theorem HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv_naturality {X Y : Type} [TopologicalSpace X] [TopologicalSpace Y] {x : X} {y : Y} {n : ℕ} (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) X x)) (hY : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) Y y)) (f : C(X, Y)) (hf : f x = y) (a : Additive (HomotopyGroup (Fin (n + 2)) X x)) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap ((TauCeti.singularChains ℤ).map (TopCat.ofHom f)) (n + 2))) ((cubicalHurewiczSingularHomologyAddEquiv hX) a) = (cubicalHurewiczSingularHomologyAddEquiv hY) (Additive.ofMul (map f hf (Additive.toMul a)))

The cubical Hurewicz equivalence with singular homology is natural in based maps between spaces satisfying the connectivity hypothesis.

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

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