Naturality of the Hurewicz map in degree one

The Hurewicz map π₁(X, x) → H₁(X; ℤ) of TauCeti.AlgebraicTopology.Homotopy.Hurewicz.One.Basic is natural in continuous maps, with respect to the map induced on the first homology group of the singular chain complex, and it does not depend on the base point: changing the base point along a path, which conjugates loops by the path, does not change their homology classes.

Main results

• ContinuousMap.singularHomologyMap_loopClass: the map induced on first singular homology by a continuous map sends the class of a loop to the class of its image.
• TauCeti.HurewiczOne.homologyMap_H₁AddEquivHomology_hurewiczAb: naturality of the Hurewicz map on the abelianized fundamental group.
• TauCeti.HurewiczOne.homologyMap_hurewiczHomologyAddEquiv: the same for the Hurewicz isomorphism of path-connected spaces.
• TauCeti.HurewiczOne.homologyMap_hurewiczHomologyAddEquiv_mapOfEq: the same for a map carrying the base point to a prescribed base point of the target.
• TauCeti.HurewiczOne.hurewicz₁_fundamentalGroupMulEquivOfPath: the Hurewicz map is invariant under the change of base point along a path.

References

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

theorem TauCeti.HurewiczOne.map_mem_cycles₁ {X Y : TopCat} (f : X ⟶ Y) {c : ↑(((singularChains ℤ).obj X).X 1)} (hc : c ∈ cycles₁ X) : (CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).map f).f 1)) c ∈ cycles₁ Y

theorem TauCeti.HurewiczOne.homologyMap_H₁AddEquivHomology_mk {X Y : TopCat} (f : X ⟶ Y) (c : ↥(cycles₁ X)) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map f) 1)) ((H₁AddEquivHomology X) (H₁.mk c)) = (H₁AddEquivHomology Y) (H₁.mk ⟨(CategoryTheory.ConcreteCategory.hom (((singularChains ℤ).map f).f 1)) ↑c, ⋯⟩)

The map induced on the first homology group of the singular chain complex sends the class of a 1-cycle to the class of its image.

theorem TauCeti.HurewiczOne.homologyMap_H₁AddEquivHomology_loopClass {X Y : TopCat} (f : X ⟶ Y) {x : ↑X} (γ : Path x x) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map f) 1)) ((H₁AddEquivHomology X) (loopClass γ)) = (H₁AddEquivHomology Y) (loopClass (γ.map ⋯))

theorem TauCeti.HurewiczOne.homologyMap_H₁AddEquivHomology_hurewiczAb {X Y : TopCat} (f : X ⟶ Y) {x : ↑X} (a : Additive (Abelianization (FundamentalGroup (↑X) x))) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map f) 1)) ((H₁AddEquivHomology X) ((hurewiczAb x) a)) = (H₁AddEquivHomology Y) ((hurewiczAb ((CategoryTheory.ConcreteCategory.hom f) x)) (Additive.ofMul ((Abelianization.map (FundamentalGroup.map (TopCat.Hom.hom f) x)) (Additive.toMul a))))

Naturality of the Hurewicz map: for a continuous map f, the map induced on the first homology group of the singular chain complex corresponds to the map induced on fundamental groups.

theorem TauCeti.HurewiczOne.homologyMap_hurewiczHomologyAddEquiv {X Y : TopCat} (f : X ⟶ Y) [PathConnectedSpace ↑X] [PathConnectedSpace ↑Y] {x : ↑X} (a : Additive (Abelianization (FundamentalGroup (↑X) x))) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map f) 1)) ((hurewiczHomologyAddEquiv x) a) = (hurewiczHomologyAddEquiv ((CategoryTheory.ConcreteCategory.hom f) x)) (Additive.ofMul ((Abelianization.map (FundamentalGroup.map (TopCat.Hom.hom f) x)) (Additive.toMul a)))

Naturality of the Hurewicz isomorphism of path-connected spaces.

theorem TauCeti.HurewiczOne.homologyMap_hurewiczHomologyAddEquiv_mapOfEq {X Y : TopCat} (f : X ⟶ Y) [PathConnectedSpace ↑X] [PathConnectedSpace ↑Y] {x : ↑X} {y : ↑Y} (h : (CategoryTheory.ConcreteCategory.hom f) x = y) (a : Additive (Abelianization (FundamentalGroup (↑X) x))) : (ModuleCat.Hom.hom (HomologicalComplex.homologyMap ((singularChains ℤ).map f) 1)) ((hurewiczHomologyAddEquiv x) a) = (hurewiczHomologyAddEquiv y) (Additive.ofMul ((Abelianization.map (FundamentalGroup.mapOfEq (TopCat.Hom.hom f) h)) (Additive.toMul a)))

Naturality of the Hurewicz isomorphism of path-connected spaces, for a continuous map carrying the base point x to a prescribed base point y of the target.

theorem TauCeti.HurewiczOne.hurewicz₁_fundamentalGroupMulEquivOfPath {X : TopCat} {x x' : ↑X} (p : Path x x') (a : FundamentalGroup (↑X) x) : (hurewicz₁ X x') ((FundamentalGroup.fundamentalGroupMulEquivOfPath p) a) = (hurewicz₁ X x) a

Independence of the base point: the Hurewicz map is invariant under the change of base point along a path.

theorem TauCeti.HurewiczOne.hurewiczHomologyAddEquiv_fundamentalGroupMulEquivOfPath {X : TopCat} [PathConnectedSpace ↑X] {x x' : ↑X} (p : Path x x') (a : FundamentalGroup (↑X) x) : (hurewiczHomologyAddEquiv x') (Additive.ofMul (Abelianization.of ((FundamentalGroup.fundamentalGroupMulEquivOfPath p) a))) = (hurewiczHomologyAddEquiv x) (Additive.ofMul (Abelianization.of a))

Changing the base point along a path does not change the singular homology class supplied by the degree-one Hurewicz isomorphism.

theorem ContinuousMap.singularHomologyMap_loopClass {Y Z : Type} [TopologicalSpace Y] [TopologicalSpace Z] (g : C(Y, Z)) {y : Y} (γ : Path y y) : (singularHomologyMap ℤ 1 g) ((TauCeti.HurewiczOne.H₁AddEquivHomology ↧Y) (TauCeti.HurewiczOne.loopClass γ)) = (TauCeti.HurewiczOne.H₁AddEquivHomology ↧Z) (TauCeti.HurewiczOne.loopClass (γ.map ⋯))

The map induced on first singular homology by a continuous map sends the class of a loop to the class of its image.