Hurewicz theorem

AbbreviationIntegral singular homology#✓fully proved

For a natural number \(n\) and a topological space \(X\), \(H_n(X; \mathbb{Z})\) denotes the \(n\)-th singular homology group of \(X\) with coefficients in \(\mathbb{Z}\), regarded as an abelian group.

noncomputable abbrev IntegralHomology (n : ℕ) (X : Type) [TopologicalSpace X] : AddCommGrpCat :=
  ((singularHomologyFunctor AddCommGrpCat.{0} n).obj (AddCommGrpCat.of ℤ)).obj (TopCat.of X)

Used by 1

Used byFirst homology is the abelianized fundamental group

TheoremFirst homology is the abelianized fundamental group#●ready to prove

Let \(X\) be a path-connected topological space and let \(x \in X\). Then the abelianization of the fundamental group \(\pi_1(X, x)\) is isomorphic, as a group, to the first integral singular homology group \(H_1(X; \mathbb{Z})\) of \(X\).

public theorem_wanted hurewicz_h1_abelianization
    (X : Type) [TopologicalSpace X] [PathConnectedSpace X] (x : X) :
    Nonempty (Additive (Abelianization (FundamentalGroup X x)) ≃+
      (IntegralHomology 1 X : Type))

Sources

• W. Hurewicz (1935); see Hatcher, Algebraic Topology, Theorem 2A.1. Knill, Some fundamental theorems in mathematics, §153. Problem hurewicz_h1_abelianization of the lean-eval benchmark.

Uses 1

Statement usesIntegral singular homology

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.