The Hurewicz theorem in degree one

For a path-connected space X with a base point x, the Hurewicz map sends a loop at x to the homology class of the singular 1-simplex it defines, and it identifies the abelianization of the fundamental group π₁(X, x) with the first singular homology group H₁(X; ℤ) (TauCeti.HurewiczOne.hurewiczHomologyAddEquiv).

The proof is the one of Hatcher, Theorem 2A.1, carried out on the singular chains with integer coefficients through the element-level interface of TauCeti.AlgebraicTopology.Singular.ModuleChains.Basic. Paths γ : I → X are read as singular 1-simplices along the parameter of the standard 1-simplex, and three kinds of explicit singular 2-simplices give the relations:

• a constant 2-simplex shows that the chain of a constant path is a boundary;
• the composite of a concatenation γ.trans δ with the affine projection of Δ² onto [0, 1] sending the vertices to 0, 1/2 and 1 shows that γ + δ - γ.trans δ is a boundary;
• a homotopy of paths, cut along the diagonal of its square into two 2-simplices, shows that homotopic paths have homologous chains.

So the Hurewicz map is a well-defined homomorphism π₁(X, x) → H₁(X; ℤ) (TauCeti.HurewiczOne.hurewicz₁).

Conversely, a function f on path classes that is additive under concatenation induces a homomorphism out of H₁(X; ℤ) sending the class of a cycle Σ nᵢ σᵢ to Σ nᵢ f [σᵢ] (TauCeti.HurewiczOne.H₁.liftPathClass): it vanishes on boundaries because the three edges of a singular 2-simplex are images of paths in the simply connected standard simplex. The inverse of the Hurewicz map is induced in this way by sending a path class from y to z to the class of the loop that runs along a chosen path from x to y, along the class, and back from z. It inverts the Hurewicz map because conjugation is trivial in the abelianization. Conversely, the loop through a singular 1-simplex σ differs from σ by the chains of the chosen paths at its endpoints, which cancel on cycles.

The homology group is first described as the explicit homology ShortComplex.moduleCatLeftHomologyData of the short complex C₂ → C₁ → C₀, that is 1-cycles modulo boundaries (TauCeti.HurewiczOne.H₁), and then identified with the homology of the singular chain complex (TauCeti.HurewiczOne.H₁AddEquivHomology).

Main definitions and results

• TauCeti.HurewiczOne.hurewicz₁: the Hurewicz homomorphism π₁(X, x) → H₁(X; ℤ).
• TauCeti.HurewiczOne.H₁.lift, TauCeti.HurewiczOne.H₁.liftPathClass: the homomorphisms out of H₁ induced by linear maps on 1-chains vanishing on boundaries, and by functions on path classes additive under concatenation.
• TauCeti.HurewiczOne.hurewiczAddEquiv: for path-connected X, it induces an isomorphism from the abelianization of π₁(X, x) onto H₁, the 1-cycles modulo boundaries.
• TauCeti.HurewiczOne.hurewiczHomologyAddEquiv: the same isomorphism onto the first homology group of the singular chain complex of X with integer coefficients.

References

• A. Hatcher, Algebraic Topology, Theorem 2A.1.

@[reducible, inline]

noncomputable abbrev TauCeti.HurewiczOne.sc₁ (X : TopCat) : CategoryTheory.ShortComplex (ModuleCat ℤ)

The short complex C₂ → C₁ → C₀ of the singular chains of X.

@[reducible, inline]

noncomputable abbrev TauCeti.HurewiczOne.boundaries₁ (X : TopCat) : Submodule ℤ ↑(((singularChains ℤ).obj X).X 1)

The boundaries among the singular 1-chains of X.

theorem TauCeti.HurewiczOne.mem_boundaries₁ {X : TopCat} {c : ↑(((singularChains ℤ).obj X).X 1)} (y : ↑(((singularChains ℤ).obj X).X 2)) (h : (CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).obj X).d 2 1)) y = c) : c ∈ boundaries₁ X

theorem TauCeti.HurewiczOne.pathChain_const_mem_boundaries₁ {X : TopCat} (p : ↑X) : pathChain ℤ (ContinuousMap.const (↑unitInterval) p) ∈ boundaries₁ X

The chain of a constant map is a boundary.

theorem TauCeti.HurewiczOne.pathChain_add_sub_trans_mem_boundaries₁ {X : TopCat} {a b c : ↑X} (γ : Path a b) (δ : Path b c) : pathChain ℤ γ.toContinuousMap + pathChain ℤ δ.toContinuousMap - pathChain ℤ (γ.trans δ).toContinuousMap ∈ boundaries₁ X

The chain of a concatenation of paths differs from the sum of the chains of the two paths by a boundary.

theorem TauCeti.HurewiczOne.pathChain_sub_mem_boundaries₁_of_homotopy {X : TopCat} {a b : ↑X} {γ γ' : Path a b} (F : γ.Homotopy γ') : pathChain ℤ γ.toContinuousMap - pathChain ℤ γ'.toContinuousMap ∈ boundaries₁ X

The chains of homotopic paths differ by a boundary.

The Hurewicz map

@[reducible, inline]

noncomputable abbrev TauCeti.HurewiczOne.cycles₁ (X : TopCat) : Submodule ℤ ↑(((singularChains ℤ).obj X).X 1)

The singular 1-cycles of X, the kernel of the differential of sc₁ X.

@[reducible, inline]

noncomputable abbrev TauCeti.HurewiczOne.H₁ (X : TopCat) : ModuleCat ℤ

The first singular homology group of X with integer coefficients, as the explicit homology cycles₁ X ⧸ boundaries of sc₁ X in ModuleCat ℤ.

theorem TauCeti.HurewiczOne.mem_cycles₁_iff {X : TopCat} {c : ↑(((singularChains ℤ).obj X).X 1)} : c ∈ cycles₁ X ↔ (CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).obj X).d 1 0)) c = 0

A 1-chain is a cycle when its boundary vanishes.

theorem TauCeti.HurewiczOne.mem_cycles₁ {X : TopCat} {c : ↑(((singularChains ℤ).obj X).X 1)} (h : (CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).obj X).d 1 0)) c = 0) : c ∈ cycles₁ X

noncomputable def TauCeti.HurewiczOne.H₁.mk {X : TopCat} : ↥(cycles₁ X) →+ ↑(H₁ X)

The class in H₁ X of a 1-cycle, as an additive map. (It is not stated as a ℤ-linear map: instance search on the cycles would find AddCommGroup.toIntModule, which is only propositionally equal to their submodule structure.)

theorem TauCeti.HurewiczOne.H₁.mk_eq_mk_iff {X : TopCat} (c c' : ↥(cycles₁ X)) : mk c = mk c' ↔ ↑c - ↑c' ∈ boundaries₁ X

theorem TauCeti.HurewiczOne.H₁.mk_eq_zero_iff {X : TopCat} (c : ↥(cycles₁ X)) : mk c = 0 ↔ ↑c ∈ boundaries₁ X

theorem TauCeti.HurewiczOne.H₁.mk_surjective {X : TopCat} : Function.Surjective ⇑mk

theorem TauCeti.HurewiczOne.H₁.addMonoidHom_ext {X : TopCat} {A : Type u_1} [AddZeroClass A] {f g : ↑(H₁ X) →+ A} (h : ∀ (c : ↥(cycles₁ X)), f (mk c) = g (mk c)) : f = g

Two additive maps out of H₁ X agree once they agree on the classes of 1-cycles.

theorem TauCeti.HurewiczOne.H₁.addMonoidHom_ext_iff {X : TopCat} {A : Type u_1} [AddZeroClass A] {f g : ↑(H₁ X) →+ A} : f = g ↔ ∀ (c : ↥(cycles₁ X)), f (mk c) = g (mk c)

theorem TauCeti.HurewiczOne.pathChain_mem_cycles₁ {X : TopCat} {x : ↑X} (γ : Path x x) : pathChain ℤ γ.toContinuousMap ∈ cycles₁ X

noncomputable def TauCeti.HurewiczOne.loopClass {X : TopCat} {x : ↑X} (γ : Path x x) : ↑(H₁ X)

The homology class of the chain of a loop.

theorem TauCeti.HurewiczOne.loopClass_def {X : TopCat} {x : ↑X} (γ : Path x x) : loopClass γ = H₁.mk ⟨pathChain ℤ γ.toContinuousMap, ⋯⟩

theorem TauCeti.HurewiczOne.loopClass_eq_iff {X : TopCat} {x y : ↑X} (γ : Path x x) (γ' : Path y y) : loopClass γ = loopClass γ' ↔ pathChain ℤ γ.toContinuousMap - pathChain ℤ γ'.toContinuousMap ∈ boundaries₁ X

theorem TauCeti.HurewiczOne.loopClass_eq_of_apply_eq {X : TopCat} {x y : ↑X} (γ : Path x x) (γ' : Path y y) (hγ : ∀ (t : ↑unitInterval), γ t = γ' t) : loopClass γ = loopClass γ'

Loops with the same values have the same homology class, even when their base points are not syntactically equal.

@[simp]

theorem TauCeti.HurewiczOne.loopClass_refl {X : TopCat} (x : ↑X) : loopClass (Path.refl x) = 0

@[simp]

theorem TauCeti.HurewiczOne.loopClass_trans {X : TopCat} {x : ↑X} (γ δ : Path x x) : loopClass (γ.trans δ) = loopClass γ + loopClass δ

noncomputable def TauCeti.HurewiczOne.hurewicz₁ (X : TopCat) (x : ↑X) : FundamentalGroup (↑X) x →* Multiplicative ↑(H₁ X)

The Hurewicz map in degree one: a loop is sent to the homology class of its chain.

@[simp]

theorem TauCeti.HurewiczOne.hurewicz₁_mk {X : TopCat} {x : ↑X} (γ : Path x x) : (hurewicz₁ X x) (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)) = Multiplicative.ofAdd (loopClass γ)

Homomorphisms out of the first homology group

noncomputable def TauCeti.HurewiczOne.H₁.lift {X : TopCat} {A : Type} [AddCommGroup A] (f : ↑(((singularChains ℤ).obj X).X 1) →ₗ[ℤ] A) (hf : ∀ (y : ↑(((singularChains ℤ).obj X).X 2)), f ((CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).obj X).d 2 1)) y) = 0) : ↑(H₁ X) →+ A

The homomorphism out of H₁ X induced by a linear map on the singular 1-chains which vanishes on boundaries.

@[simp]

theorem TauCeti.HurewiczOne.H₁.lift_mk {X : TopCat} {A : Type} [AddCommGroup A] (f : ↑(((singularChains ℤ).obj X).X 1) →ₗ[ℤ] A) (hf : ∀ (y : ↑(((singularChains ℤ).obj X).X 2)), f ((CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).obj X).d 2 1)) y) = 0) (c : ↥(cycles₁ X)) : (lift f hf) (mk c) = f ↑c

theorem TauCeti.HurewiczOne.chainsDesc_path₁_d {X : TopCat} {A : Type} [AddCommGroup A] {f : {y z : ↑X} → Path.Homotopic.Quotient y z → A} (hf : ∀ {y z w : ↑X} (p : Path.Homotopic.Quotient y z) (q : Path.Homotopic.Quotient z w), f (p.trans q) = f p + f q) (y : ↑(((singularChains ℤ).obj X).X 2)) : (chainsDesc fun (s : (TopCat.toSSet.obj X).obj (Opposite.op { len := 1 })) => f (Path.Homotopic.Quotient.mk (TopCat.path₁ s))) ((CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).obj X).d 2 1)) y) = 0

An additive function on path classes kills the boundaries of singular 2-simplices: the three edges of a singular 2-simplex are images of paths in the simply connected standard simplex.

noncomputable def TauCeti.HurewiczOne.H₁.liftPathClass {X : TopCat} {A : Type} [AddCommGroup A] {f : {y z : ↑X} → Path.Homotopic.Quotient y z → A} (hf : ∀ {y z w : ↑X} (p : Path.Homotopic.Quotient y z) (q : Path.Homotopic.Quotient z w), f (p.trans q) = f p + f q) : ↑(H₁ X) →+ A

The homomorphism out of H₁ X induced by a function f on path classes that is additive under concatenation: the class of a cycle Σ nᵢ σᵢ is sent to Σ nᵢ f [σᵢ].

@[simp]

theorem TauCeti.HurewiczOne.H₁.liftPathClass_mk {X : TopCat} {A : Type} [AddCommGroup A] {f : {y z : ↑X} → Path.Homotopic.Quotient y z → A} (hf : ∀ {y z w : ↑X} (p : Path.Homotopic.Quotient y z) (q : Path.Homotopic.Quotient z w), f (p.trans q) = f p + f q) (c : ↥(cycles₁ X)) : (liftPathClass ⋯) (mk c) = (chainsDesc fun (s : (TopCat.toSSet.obj X).obj (Opposite.op { len := 1 })) => f (Path.Homotopic.Quotient.mk (TopCat.path₁ s))) ↑c

@[simp]

theorem TauCeti.HurewiczOne.H₁.liftPathClass_loopClass {X : TopCat} {A : Type} [AddCommGroup A] {f : {y z : ↑X} → Path.Homotopic.Quotient y z → A} (hf : ∀ {y z w : ↑X} (p : Path.Homotopic.Quotient y z) (q : Path.Homotopic.Quotient z w), f (p.trans q) = f p + f q) {x : ↑X} (γ : Path x x) : (liftPathClass ⋯) (loopClass γ) = f (Path.Homotopic.Quotient.mk γ)

The homomorphism out of H₁ X induced by an additive function f on path classes sends the class of a loop to the value of f on its class.

The inverse map

theorem TauCeti.HurewiczOne.pathChain_add_symm_mem_boundaries₁ {X : TopCat} {a b : ↑X} (γ : Path a b) : pathChain ℤ γ.toContinuousMap + pathChain ℤ γ.symm.toContinuousMap ∈ boundaries₁ X

noncomputable def TauCeti.HurewiczOne.hurewiczAb {X : TopCat} (x : ↑X) : Additive (Abelianization (FundamentalGroup (↑X) x)) →+ ↑(H₁ X)

The Hurewicz map on the abelianized fundamental group, written additively.

@[simp]

theorem TauCeti.HurewiczOne.hurewiczAb_ofMul_of {X : TopCat} (x : ↑X) (g : FundamentalGroup (↑X) x) : (hurewiczAb x) (Additive.ofMul (Abelianization.of g)) = Multiplicative.toAdd ((hurewicz₁ X x) g)

On the abelianization, the Hurewicz map is induced by TauCeti.HurewiczOne.hurewicz₁.

theorem TauCeti.HurewiczOne.hurewiczAb_ofMul_of_mk {X : TopCat} (x : ↑X) (γ : Path x x) : (hurewiczAb x) (Additive.ofMul (Abelianization.of (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)))) = loopClass γ

noncomputable def TauCeti.HurewiczOne.hurewiczAddEquiv {X : TopCat} [PathConnectedSpace ↑X] (x : ↑X) : Additive (Abelianization (FundamentalGroup (↑X) x)) ≃+ ↑(H₁ X)

The Hurewicz theorem in degree one: for a path-connected space, the Hurewicz map identifies the abelianized fundamental group with the first homology group, written as the explicit homology of the short complex C₂ → C₁ → C₀.

@[simp]

theorem TauCeti.HurewiczOne.hurewiczAddEquiv_ofMul_of_mk {X : TopCat} [PathConnectedSpace ↑X] (x : ↑X) (γ : Path x x) : (hurewiczAddEquiv x) (Additive.ofMul (Abelianization.of (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)))) = loopClass γ

theorem TauCeti.HurewiczOne.hurewiczAddEquiv_apply {X : TopCat} [PathConnectedSpace ↑X] (x : ↑X) (a : Additive (Abelianization (FundamentalGroup (↑X) x))) : (hurewiczAddEquiv x) a = (hurewiczAb x) a

@[simp]

theorem TauCeti.HurewiczOne.hurewiczAddEquiv_symm_loopClass {X : TopCat} [PathConnectedSpace ↑X] (x : ↑X) (γ : Path x x) : (hurewiczAddEquiv x).symm (loopClass γ) = Additive.ofMul (Abelianization.of (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)))

The inverse of the Hurewicz isomorphism sends the class of a loop to its class in the abelianized fundamental group.

Comparison with the homology of the singular chain complex

noncomputable def TauCeti.HurewiczOne.H₁AddEquivHomology (X : TopCat) : ↑(H₁ X) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj X) 1)

The explicit homology H₁ X of sc₁ X is the first homology group of the singular chain complex.

theorem TauCeti.HurewiczOne.H₁AddEquivHomology_mk {X : TopCat} (c : ↥(cycles₁ X)) (z : ↑(HomologicalComplex.cycles ((singularChains ℤ).obj X) 1)) (hz : (ModuleCat.Hom.hom (HomologicalComplex.iCycles ((singularChains ℤ).obj X) 1)) z = ↑c) : (H₁AddEquivHomology X) (H₁.mk c) = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ ((singularChains ℤ).obj X) 1)) z

The identification of H₁ X with the homology of the singular chain complex sends the class of a cycle c to the homology class of the cycle of the complex lying over c.

theorem TauCeti.HurewiczOne.H₁AddEquivHomology_loopClass {X : TopCat} {x : ↑X} (γ : Path x x) (z : ↑(HomologicalComplex.cycles ((singularChains ℤ).obj X) 1)) (hz : (ModuleCat.Hom.hom (HomologicalComplex.iCycles ((singularChains ℤ).obj X) 1)) z = pathChain ℤ γ.toContinuousMap) : (H₁AddEquivHomology X) (loopClass γ) = (ModuleCat.Hom.hom (HomologicalComplex.homologyπ ((singularChains ℤ).obj X) 1)) z

The identification of H₁ X with the homology of the singular chain complex sends the class of a loop to the homology class of a cycle of the complex lying over the chain of the loop.

theorem TauCeti.HurewiczOne.homology_one_addMonoidHom_ext {X : TopCat} {A : Type u_1} [AddZeroClass A] {f g : ↑(HomologicalComplex.homology ((singularChains ℤ).obj X) 1) →+ A} (h : ∀ (c : ↥(cycles₁ X)), f ((H₁AddEquivHomology X) (H₁.mk c)) = g ((H₁AddEquivHomology X) (H₁.mk c))) : f = g

Two additive maps out of the first homology group of the singular chain complex agree once they agree on the classes of 1-cycles.

The Hurewicz isomorphism

noncomputable def TauCeti.HurewiczOne.hurewiczHomologyAddEquiv {X : TopCat} [PathConnectedSpace ↑X] (x : ↑X) : Additive (Abelianization (FundamentalGroup (↑X) x)) ≃+ ↑(HomologicalComplex.homology ((singularChains ℤ).obj X) 1)

The Hurewicz theorem in degree one: for a path-connected space X with a base point x, the Hurewicz map identifies the abelianization of π₁(X, x) with H₁(X; ℤ), the first homology group of the singular chain complex of X with integer coefficients.

theorem TauCeti.HurewiczOne.hurewiczHomologyAddEquiv_apply {X : TopCat} [PathConnectedSpace ↑X] {x : ↑X} (a : Additive (Abelianization (FundamentalGroup (↑X) x))) : (hurewiczHomologyAddEquiv x) a = (H₁AddEquivHomology X) ((hurewiczAb x) a)

@[simp]

theorem TauCeti.HurewiczOne.hurewiczHomologyAddEquiv_ofMul_of_mk {X : TopCat} [PathConnectedSpace ↑X] {x : ↑X} (γ : Path x x) : (hurewiczHomologyAddEquiv x) (Additive.ofMul (Abelianization.of (FundamentalGroup.fromPath (Path.Homotopic.Quotient.mk γ)))) = (H₁AddEquivHomology X) (loopClass γ)