Homotopy invariance of cubical singular chains

Homotopic maps induce chain homotopic maps of normalized cubical chains (TopCat.Homotopy.normalizedCubicalChainComplexMap), so a homotopy equivalence of spaces induces a chain homotopy equivalence of normalized cubical chain complexes (ContinuousMap.HomotopyEquiv.normalizedCubicalChainComplexHomotopyEquiv), in particular a quasi-isomorphism.

As the design of the comparison prescribes, this is not proved again on cubes: it is transported from the homotopy invariance of simplicial singular chains through the natural chain homotopy equivalence TauCeti.cubicalSingularHomotopyEquiv. If f and g are homotopic, then, writing φ and ψ for the comparison maps, N(f) ≃ φ ψ N(f) = φ S(f) ψ ≃ φ S(g) ψ = φ ψ N(g) ≃ N(g).

Main definitions

• TopCat.Homotopy.normalizedCubicalChainComplexMap: the chain homotopy between the maps of normalized cubical chains induced by homotopic maps.
• ContinuousMap.HomotopyEquiv.normalizedCubicalChainComplexHomotopyEquiv: the chain homotopy equivalence induced by a homotopy equivalence.

Main results

• TopCat.Homotopy.congr_homologyMap_normalizedCubicalChainComplex: homotopic maps induce the same map on cubical homology.
• ContinuousMap.HomotopyEquiv.quasiIso_normalizedCubicalChainComplex_map: a homotopy equivalence induces a quasi-isomorphism of normalized cubical chains.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapter VII.

noncomputable def TopCat.Homotopy.normalizedCubicalChainComplexMap {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) (k : Type u) [Ring k] : _root_.Homotopy ((TauCeti.normalizedCubicalChainComplex k).map f) ((TauCeti.normalizedCubicalChainComplex k).map g)

Homotopic maps induce chain homotopic maps of normalized cubical chains.

theorem TopCat.Homotopy.congr_homologyMap_normalizedCubicalChainComplex {k : Type u} [Ring k] {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) (n : ℕ) : HomologicalComplex.homologyMap ((TauCeti.normalizedCubicalChainComplex k).map f) n = HomologicalComplex.homologyMap ((TauCeti.normalizedCubicalChainComplex k).map g) n

Homotopic maps induce the same map on cubical homology.

noncomputable def ContinuousMap.HomotopyEquiv.normalizedCubicalChainComplexHomotopyEquiv (k : Type u) [Ring k] {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : _root_.HomotopyEquiv ((TauCeti.normalizedCubicalChainComplex k).obj ↧X) ((TauCeti.normalizedCubicalChainComplex k).obj ↧Y)

A homotopy equivalence induces a chain homotopy equivalence of normalized cubical chains.

@[simp]

theorem ContinuousMap.HomotopyEquiv.normalizedCubicalChainComplexHomotopyEquiv_hom {k : Type u} [Ring k] {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : (normalizedCubicalChainComplexHomotopyEquiv k e).hom = (TauCeti.normalizedCubicalChainComplex k).map (TopCat.ofHom e.toFun)

@[simp]

theorem ContinuousMap.HomotopyEquiv.normalizedCubicalChainComplexHomotopyEquiv_inv {k : Type u} [Ring k] {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : (normalizedCubicalChainComplexHomotopyEquiv k e).inv = (TauCeti.normalizedCubicalChainComplex k).map (TopCat.ofHom e.invFun)

theorem ContinuousMap.HomotopyEquiv.quasiIso_normalizedCubicalChainComplex_map {k : Type u} [Ring k] {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] (e : HomotopyEquiv X Y) : QuasiIso ((TauCeti.normalizedCubicalChainComplex k).map (TopCat.ofHom e.toFun))

A homotopy equivalence induces a quasi-isomorphism of normalized cubical chains.