Naturality of the constant-coefficient comparison for singular cohomology

The comparison between cohomology with a constant local system and ordinary singular cohomology commutes with continuous maps. The pullback of the constant system is identified with the constant system on the source. This gives the map-level comparison needed when cohomology with local coefficients is specialized to ordinary cohomology.

References

• A. Hatcher, Algebraic Topology, Section 3.1.

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexConstantIso_hom_space_naturality {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} (f : X ⟶ Y) (N : ModuleCat R) : CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f ((constantFunctor Y).obj N)) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M (pullbackConstantIso (TopCat.Hom.hom f) N).inv) (twistedCochainComplexConstantIso k M X N).hom) = CategoryTheory.CategoryStruct.comp (twistedCochainComplexConstantIso k M Y N).hom (TopCat.singularCochainComplexMap f)

The constant-system comparison of cochain complexes commutes with a continuous map, after identifying the pullback of a constant system with the constant system on the source.

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexConstantIso_hom_space_naturality_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} (f : X ⟶ Y) (N : ModuleCat R) {Z : CochainComplex (ModuleCat k) ℕ} (h : TopCat.singularCochainComplex N k M X ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f ((constantFunctor Y).obj N)) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M (pullbackConstantIso (TopCat.Hom.hom f) N).inv) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexConstantIso k M X N).hom h)) = CategoryTheory.CategoryStruct.comp (twistedCochainComplexConstantIso k M Y N).hom (CategoryTheory.CategoryStruct.comp (TopCat.singularCochainComplexMap f) h)

The constant-system comparison of cochain complexes commutes with a continuous map, after identifying the pullback of a constant system with the constant system on the source.

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyConstantIso_hom_space_naturality {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} (f : X ⟶ Y) (N : ModuleCat R) (n : ℕ) : CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f ((constantFunctor Y).obj N) n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M (pullbackConstantIso (TopCat.Hom.hom f) N).inv n) (twistedCohomologyConstantIso k M X N n).hom) = CategoryTheory.CategoryStruct.comp (twistedCohomologyConstantIso k M Y N n).hom (TopCat.singularCohomologyMap f n)

The constant-system comparison on cohomology is natural in the space.

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyConstantIso_hom_space_naturality_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} (f : X ⟶ Y) (N : ModuleCat R) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology N k M X n ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f ((constantFunctor Y).obj N) n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M (pullbackConstantIso (TopCat.Hom.hom f) N).inv n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyConstantIso k M X N n).hom h)) = CategoryTheory.CategoryStruct.comp (twistedCohomologyConstantIso k M Y N n).hom (CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap f n) h)

The constant-system comparison on cohomology is natural in the space.