Weak homotopy equivalences induce isomorphisms on singular homology

A weak homotopy equivalence f : X → Y induces a quasi-isomorphism of normalized cubical singular chains, and isomorphisms H_n(X; M) ≅ H_n(Y; M) on singular homology with coefficients in any module M over any ring R, in particular in any abelian group (R = ℤ) (Hatcher, Algebraic Topology, Proposition 4.21). No CW structure on X or Y is needed. The carrier of M lies in the universe of X and Y, as in the local-coefficient statement below; R may lie in any universe.

The proof of the cubical statement factors f through its mapping cylinder M_f as

X ≃ₜ (bottom face of M_f) ↪ M_f → Y.

• The first map is a homeomorphism (TauCeti.MappingCylinder.inclHomeomorph).
• The last map, the projection, is a homotopy equivalence (TauCeti.MappingCylinder.homotopyEquiv), so it induces a chain homotopy equivalence of cubical chains.
• For the inclusion of the bottom face, every point of M_f is joined by a path to the bottom face, and the relative homotopy sets of the pair vanish because f is a weak homotopy equivalence (ContinuousMap.IsWeakHomotopyEquivalence.subsingleton_relHomotopyGroup_mappingCylinder). So the singular cubes of M_f deform into the bottom face, and the inclusion induces a chain homotopy equivalence of cubical chains (TauCeti.isIso_singularHomologyMap_subtypeVal_of_relHomotopyGroup and the cubical statement behind it).

The same factorization proves the statement with local coefficients: for a local coefficient system L on Y, the map H_n(X; f⁎L) ⟶ H_n(Y; L) is an isomorphism. The bottom face of the mapping cylinder is handled by the compression of cubical chains with local coefficients (TauCeti.quasiIso_normalizedTwistedCubicalChainComplexMap_subtypeVal_of_relHomotopyGroup), transported to simplicial chains through the comparison TauCeti.LocalCoefficientSystem.twistedCubicalToSingularMap, which is natural in the space. The other two factors are homotopy equivalences, which induce isomorphisms on homology with local coefficients by homotopy invariance (ContinuousMap.HomotopyEquiv.isIso_twistedHomologyMap).

Singular homology with coefficients in a module M is homology with local coefficients in the constant system at M (TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso), compatibly with maps of spaces (TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso_hom_space_naturality), so the statement for singular homology is the case of a constant system.

Main results

• ContinuousMap.IsWeakHomotopyEquivalence.quasiIso_normalizedCubicalChainComplex_map: a weak homotopy equivalence induces a quasi-isomorphism of normalized cubical chains.
• ContinuousMap.IsWeakHomotopyEquivalence.quasiIso_twistedChainComplexMap, ContinuousMap.IsWeakHomotopyEquivalence.isIso_twistedHomologyMap: the same with local coefficients.
• ContinuousMap.IsWeakHomotopyEquivalence.quasiIso_normalizedTwistedCubicalChainComplexMap: the cubical form with local coefficients.
• ContinuousMap.IsWeakHomotopyEquivalence.isIso_singularHomologyMap: a weak homotopy equivalence induces isomorphisms on singular homology with coefficients in any module.

References

• A. Hatcher, Algebraic Topology, Section 4.1, Proposition 4.21, and Section 3.H for homology with local coefficients.

theorem ContinuousMap.IsWeakHomotopyEquivalence.quasiIso_normalizedCubicalChainComplex_map {X Y : Type u} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} (k : Type u) [Ring k] (hf : f.IsWeakHomotopyEquivalence) : QuasiIso ((TauCeti.normalizedCubicalChainComplex k).map (TopCat.ofHom f))

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

Local coefficients

theorem ContinuousMap.IsWeakHomotopyEquivalence.quasiIso_twistedChainComplexMap {X Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {R : Type u} [Ring R] (hf : f.IsWeakHomotopyEquivalence) (L : TauCeti.LocalCoefficientSystem R ↧Y) : QuasiIso (TauCeti.LocalCoefficientSystem.twistedChainComplexMap (TopCat.ofHom f) L)

A weak homotopy equivalence induces a quasi-isomorphism of singular chains with local coefficients: for every local coefficient system L on Y, the map of singular chain complexes from X with coefficients in f⁎L to Y with coefficients in L is a quasi-isomorphism.

theorem ContinuousMap.IsWeakHomotopyEquivalence.isIso_twistedHomologyMap {X Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {R : Type u} [Ring R] (hf : f.IsWeakHomotopyEquivalence) (L : TauCeti.LocalCoefficientSystem R ↧Y) (n : ℕ) : CategoryTheory.IsIso (TauCeti.LocalCoefficientSystem.twistedHomologyMap (TopCat.ofHom f) L n)

A weak homotopy equivalence induces isomorphisms on singular homology with local coefficients, the local-coefficient form of Hatcher, Proposition 4.21: for every local coefficient system L on Y, the map H_n(X; f⁎L) ⟶ H_n(Y; L) is an isomorphism.

theorem ContinuousMap.IsWeakHomotopyEquivalence.quasiIso_normalizedTwistedCubicalChainComplexMap {X Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {R : Type u} [Ring R] (hf : f.IsWeakHomotopyEquivalence) (L : TauCeti.LocalCoefficientSystem R ↧Y) : QuasiIso (TauCeti.LocalCoefficientSystem.normalizedTwistedCubicalChainComplexMap f L)

A weak homotopy equivalence induces a quasi-isomorphism of normalized cubical chains with local coefficients.

Singular homology with coefficients in a module

theorem ContinuousMap.IsWeakHomotopyEquivalence.isIso_singularHomologyMap {X Y : Type v} [TopologicalSpace X] [TopologicalSpace Y] {f : C(X, Y)} {R : Type u} [Ring R] (hf : f.IsWeakHomotopyEquivalence) (M : ModuleCat R) (n : ℕ) : CategoryTheory.IsIso (((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) n).obj M).map (TopCat.ofHom f))

A weak homotopy equivalence induces isomorphisms on singular homology with coefficients in any module M over any ring R, in particular in any abelian group (R = ℤ) (Hatcher, Proposition 4.21). The carrier of M lies in the universe of X and Y; R may lie in any universe. This is the case of the constant coefficient system at M in isIso_twistedHomologyMap.