Homotopy invariance of singular cohomology with local coefficients

Let H be a homotopy from f : X ⟶ Y to g : X ⟶ Y and let L be a local coefficient system on Y. The maps induced by f and g on twisted singular cochains land in the cochains twisted by the two pullback systems f⁎L and g⁎L, which LocalCoefficientSystem.pullbackHomotopyIso identifies by transport along the homotopy. Applying Hom(-, M) to the chain homotopy TopCat.Homotopy.twistedChainComplexHomotopy of twisted chains shows that after this identification the two cochain maps are cochain homotopic, so that they agree on twisted cohomology.

Main declarations

• TopCat.Homotopy.twistedCochainComplexHomotopy: the cochain homotopy of twisted cochain complexes.
• TopCat.Homotopy.twistedCohomologyMap_eq_comp: homotopic maps induce the same map on twisted cohomology, up to the identification of the two pullback systems.

References

• A. Hatcher, Algebraic Topology, Section 3.H.

noncomputable def TopCat.Homotopy.twistedCochainComplexHomotopy {R : Type u} [Ring R] {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (L : TauCeti.LocalCoefficientSystem R Y) : _root_.Homotopy (TauCeti.LocalCoefficientSystem.twistedCochainComplexMap k M f L) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCochainComplexMap k M g L) (TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullbackHomotopyIso H).hom.app L)))

A homotopy H from f to g induces a cochain homotopy from the map of twisted cochain complexes induced by f to the map induced by g, followed by the identification of the pullback systems along H.

theorem TopCat.Homotopy.twistedCohomologyMap_eq_comp {R : Type u} [Ring R] {X Y : TopCat} {f g : X ⟶ Y} (H : Homotopy f g) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (L : TauCeti.LocalCoefficientSystem R Y) (n : ℕ) : TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M f L n = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M g L n) (TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullbackHomotopyIso H).hom.app L) n)

Homotopy invariance of cohomology with local coefficients: homotopic maps induce the same map on twisted singular cohomology, after the identification of the two pullback systems by transport along the homotopy.