The absolute Hurewicz theorem

The Hurewicz homomorphism HomotopyGroup.hurewiczHom sends the class of a generalized loop p : (Iᵐ, ∂Iᵐ) → (X, x) to the image of the generator of Hₘ(Iᵐ, ∂Iᵐ) under p. This file proves the Hurewicz theorem for it: if X is (m - 1)-connected at x and m ≥ 2, then with integer coefficients it is an isomorphism πₘ(X, x) ≅ Hₘ(X; ℤ) (HomotopyGroup.hurewiczAddEquiv).

The isomorphism is deduced from the cubical Hurewicz isomorphism HomotopyGroup.cubicalHurewiczSingularHomologyAddEquiv, by comparing the two Hurewicz maps. They agree up to a sign ε = ±1 that does not depend on the space (HomotopyGroup.exists_hurewicz_eq_units_smul_cubicalHurewicz). Both maps are natural in based maps, and every generalized loop p is the image of the tautological loop TauCeti.sphereGenLoop m of the sphere Sᵐ under a based map (GenLoop.map_toSphere_sphereGenLoop), so it suffices to compare them on that loop. On πₘ(Sᵐ) the cubical Hurewicz map is an isomorphism onto Hₘ(Sᵐ; ℤ), because Sᵐ is (m - 1)-connected (TauCeti.subsingleton_homotopyGroup_sphere_of_lt), and the Hurewicz class of the tautological loop generates Hₘ(Sᵐ; ℤ) ≅ ℤ (TauCeti.isIso_hurewicz_sphereGenLoop). An additive map ℤ → ℤ whose image contains a generator is multiplication by a unit, so the two maps differ by a unit of ℤ on πₘ(Sᵐ), and hence everywhere.

Main results

• HomotopyGroup.exists_hurewicz_eq_units_smul_cubicalHurewicz: the Hurewicz map is ε times the cubical Hurewicz map, transported to simplicial singular homology, for a universal sign ε.
• HomotopyGroup.bijective_hurewicz and HomotopyGroup.hurewiczAddEquiv: the Hurewicz theorem, πₙ₊₂(X, x) ≅ Hₙ₊₂(X; ℤ) for an (n + 1)-connected space.

References

• A. Hatcher, Algebraic Topology, Section 4.2, Theorem 4.32 (the Hurewicz theorem).

theorem HomotopyGroup.exists_hurewicz_eq_units_smul_cubicalHurewicz (n : ℕ) : ∃ (ε : ℤˣ), ∀ (X : Type) [inst : TopologicalSpace X] (x : X) (a : HomotopyGroup (Fin (n + 2)) X x), (ModuleCat.Hom.hom (hurewicz (↧ℤ) (n + 1) a)) 1 = ↑ε • (CategoryTheory.ConcreteCategory.hom (TauCeti.singularCubicalHomologyIso ℤ (↧X) (n + 2)).inv) (cubicalHurewicz ℤ (n + 1) a)

The Hurewicz map is the cubical Hurewicz map up to a universal sign. There is a unit ε of ℤ such that for every space X, point x and class a ∈ πₙ₊₂(X, x), the Hurewicz class of a with integer coefficients is ε times the cubical Hurewicz class of a, read in simplicial singular homology through the inverse cubical--simplicial comparison.

theorem HomotopyGroup.bijective_hurewicz {X : Type} [TopologicalSpace X] {x : X} {n : ℕ} (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) X x)) : Function.Bijective fun (a : HomotopyGroup (Fin (n + 2)) X x) => (ModuleCat.Hom.hom (hurewicz (↧ℤ) (n + 1) a)) 1

The Hurewicz theorem. If πₖ(X, x) is trivial for every k < n + 2, then the Hurewicz map πₙ₊₂(X, x) → Hₙ₊₂(X; ℤ), [p] ↦ p_*[Iⁿ⁺²], is bijective.

noncomputable def HomotopyGroup.hurewiczAddEquiv {X : Type} [TopologicalSpace X] {x : X} {n : ℕ} (hX : ∀ k < n + 2, Subsingleton (HomotopyGroup (Fin k) X x)) : Additive (HomotopyGroup (Fin (n + 2)) X x) ≃+ ↑(((AlgebraicTopology.singularHomologyFunctor (ModuleCat ℤ) (n + 2)).obj ↧ℤ).obj ↧X)

The Hurewicz isomorphism πₙ₊₂(X, x) ≅ Hₙ₊₂(X; ℤ) for a space X with πₖ(X, x) trivial for every k < n + 2. Its forward map is the Hurewicz homomorphism HomotopyGroup.hurewiczHom with integer coefficients, evaluated at 1 : ℤ (HomotopyGroup.hurewiczAddEquiv_apply).

@[simp]

theorem HomotopyGroup.hurewiczAddEquiv_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)) : (hurewiczAddEquiv hX) a = (ModuleCat.Hom.hom ((hurewiczHom (↧ℤ) (n + 1)) a)) 1