hurewicz_h1_abelianization.toml

id = "hurewicz_h1_abelianization"
title = "Hurewicz theorem in degree 1 (H₁ = abelianization of π₁)"
test = false
module = "LeanEval.Topology.Hurewicz"
holes = ["hurewicz_h1_abelianization"]
submitter = "Kim Morrison"
notes = "For a path-connected space X, the first integral singular homology group is the abelianization of the fundamental group. Trusted helper IntegralHomology (non-hole). Path-connectedness is essential. Mathlib has singular homology and the fundamental group but not the degree-1 Hurewicz isomorphism. Candidate from §153 of the Knill survey."
source = "W. Hurewicz (1935); see Hatcher, *Algebraic Topology*, Theorem 2A.1. Knill, *Some fundamental theorems in mathematics*, §153."
informal_solution = "Construct the natural map h : π₁(X,x) → H₁(X;ℤ) sending a loop to its singular 1-cycle. It kills commutators (H₁ is abelian), giving Φ : π₁^{ab} → H₁. Surjectivity: for path-connected X every 1-cycle is homologous to a sum of loops based at x (connect with paths). Injectivity: a loop bounding a 2-chain can be filled by a homotopy, using the path-connectedness to base everything at x. Hence Φ is an isomorphism. Requires comparing the simplicial/singular chain model with π₁, not in Mathlib."