The cubical Hurewicz class in relative cubical homology #
A generalized loop p : Ω^ (Fin (m + 1)) X x sends the boundary of the cube to x, so it is also
a relative cycle of the normalized cubical chains of the pair (X, {x})
(TopPair.cubicalCycleOfCube). This file shows that the image of the cubical Hurewicz class
GenLoop.cubicalHurewicz k p under the map from absolute to relative cubical homology is the class
of this relative cycle (GenLoop.homologyMap_π_cubicalHurewicz).
Main results #
GenLoop.homologyMap_π_cubicalHurewicz: the cubical Hurewicz class ofp, read in the relative cubical homology of(X, {x}), is the class ofpas a relative cycle.
theorem
GenLoop.homologyMap_π_cubicalHurewicz
(k : Type u)
[Ring k]
{X : Type u}
[TopologicalSpace X]
{x : X}
{m : ℕ}
(p : ↑(GenLoop (Fin (m + 1)) X x))
:
(CategoryTheory.ConcreteCategory.hom
(HomologicalComplex.homologyMap
(CategoryTheory.Limits.cokernel.π ((TauCeti.normalizedCubicalChainComplex k).map TopPair.map)) (m + 1)))
(cubicalHurewicz k p) = (CategoryTheory.ConcreteCategory.hom
(HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (TopPair.ofSubset {x})) (m + 1)))
(TopPair.cubicalCycleOfCube k ↑p ⋯)
The cubical Hurewicz class of a generalized loop p at x, read in the relative cubical
homology of (X, {x}), is the class of p as a relative cycle.