Singular cohomology with local coefficients

Let L be a local coefficient system of R-modules on a space X and let M be an R-module. Applying Hom(-, M) to the singular chains of X twisted by L gives the twisted singular cochain complex: in degree n it is the module of morphisms from the twisted n-chains to M, and its differential is precomposition with the twisted singular boundary. Its cohomology is the singular cohomology of X with coefficients in L and values in M. As for untwisted singular cohomology, the cochain groups are modules over any ring k acting linearly on R-modules: ℤ always, and R itself when R is commutative.

Since the twisted n-chains are the coproduct over the singular n-simplices σ of the fibre of L at the initial vertex of σ, a twisted n-cochain is a family of morphisms L(σ(0)) ⟶ M, one for each singular n-simplex. So this is cohomology with coefficients in the dual of L, which is the form in which cap products pair cohomology against homology twisted by the orientation system of a manifold.

Everything is functorial: a morphism of local coefficient systems L ⟶ K induces a cochain map from the cochains twisted by K to those twisted by L, a continuous map f : X ⟶ Y induces a cochain map from the cochains of Y twisted by L to those of X twisted by the pullback system, and for a constant system the construction returns ordinary singular cohomology. Pulling a system back along homotopic maps produces canonically isomorphic twisted cochain complexes and cohomology groups.

Main declarations

• TauCeti.LocalCoefficientSystem.twistedCochainComplex and TauCeti.LocalCoefficientSystem.twistedCohomology: the twisted singular cochain complex and its cohomology.
• TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap and TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap: change of local coefficient system.
• TauCeti.LocalCoefficientSystem.twistedCochainComplexMap and TauCeti.LocalCoefficientSystem.twistedCohomologyMap: the maps induced by a continuous map.
• TauCeti.LocalCoefficientSystem.twistedCohomologyPullbackHomotopyIso: the canonical comparison for pullbacks along homotopic maps.
• TauCeti.LocalCoefficientSystem.twistedCohomologyConstantIso: for a constant system, twisted cohomology is ordinary singular cohomology.

References

• A. Hatcher, Algebraic Topology, Sections 3.1 and 3.H.
• A. Dold, Lectures on Algebraic Topology, Springer, 1972, Chapters VII--VIII.

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedCochainComplex {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} (L : LocalCoefficientSystem R X) : CochainComplex (ModuleCat k) ℕ

The singular cochain complex of X with coefficients in the local coefficient system L and values in M: in degree n, the k-module of morphisms from the twisted singular n-chains of X to M.

Equations

• TauCeti.LocalCoefficientSystem.twistedCochainComplex k M L = L.twistedChainComplex.linearYonedaObj k M

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedCohomology {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : ModuleCat k

The singular cohomology of X in degree n with coefficients in the local coefficient system L and values in M.

Equations

• TauCeti.LocalCoefficientSystem.twistedCohomology k M L n = HomologicalComplex.homology (TauCeti.LocalCoefficientSystem.twistedCochainComplex k M L) n

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) : twistedCochainComplex k M K ⟶ twistedCochainComplex k M L

The cochain map induced by a morphism of local coefficient systems: precomposition with the induced morphism of twisted chains.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap_f_apply {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : ℕ) (g : ↑((twistedCochainComplex k M K).X n)) : (CategoryTheory.ConcreteCategory.hom ((twistedCochainComplexCoefficientMap k M η).f n)) g = CategoryTheory.CategoryStruct.comp ((twistedChainComplexCoefficientMap η).f n) g

The degree-n component of the cochain map induced by a morphism of local coefficient systems acts by precomposition.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap_id {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} (L : LocalCoefficientSystem R X) : twistedCochainComplexCoefficientMap k M (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id (twistedCochainComplex k M L)

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap_comp {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) : twistedCochainComplexCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M θ) (twistedCochainComplexCoefficientMap k M η)

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap_comp_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) {Z : CochainComplex (ModuleCat k) ℕ} (h : twistedCochainComplex k M L ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M θ) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M η) h)

noncomputable def TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientIso {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) : twistedCochainComplex k M K ≅ twistedCochainComplex k M L

An isomorphism of local coefficient systems induces an isomorphism of twisted cochain complexes, contravariantly in the coefficient system.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientIso_hom {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) : (twistedCochainComplexCoefficientIso k M e).hom = twistedCochainComplexCoefficientMap k M e.hom

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientIso_inv {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) : (twistedCochainComplexCoefficientIso k M e).inv = twistedCochainComplexCoefficientMap k M e.inv

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (η : L ⟶ K) (n : ℕ) : twistedCohomology k M K n ⟶ twistedCohomology k M L n

The map on twisted cohomology induced by a morphism of local coefficient systems.

Equations

• TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap k M η n = HomologicalComplex.homologyMap (TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap k M η) n

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap_id {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : twistedCohomologyCoefficientMap k M (CategoryTheory.CategoryStruct.id L) n = CategoryTheory.CategoryStruct.id (twistedCohomology k M L n)

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap_comp {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) (n : ℕ) : twistedCohomologyCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ) n = CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M θ n) (twistedCohomologyCoefficientMap k M η n)

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap_comp_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K J : LocalCoefficientSystem R X} (η : L ⟶ K) (θ : K ⟶ J) (n : ℕ) {Z : ModuleCat k} (h : twistedCohomology k M L n ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ) n) h = CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M θ n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M η n) h)

noncomputable def TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientIso {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) (n : ℕ) : twistedCohomology k M K n ≅ twistedCohomology k M L n

An isomorphism of local coefficient systems induces an isomorphism on twisted cohomology, contravariantly in the coefficient system.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientIso_hom {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) (n : ℕ) : (twistedCohomologyCoefficientIso k M e n).hom = twistedCohomologyCoefficientMap k M e.hom n

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientIso_inv {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} {L K : LocalCoefficientSystem R X} (e : L ≅ K) (n : ℕ) : (twistedCohomologyCoefficientIso k M e n).inv = twistedCohomologyCoefficientMap k M e.inv n

noncomputable def TauCeti.LocalCoefficientSystem.twistedCochainComplexPullbackHomotopyIso {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (L : LocalCoefficientSystem R Y) : twistedCochainComplex k M ((pullback (TopCat.Hom.hom g)).obj L) ≅ twistedCochainComplex k M ((pullback (TopCat.Hom.hom f)).obj L)

The canonical comparison of twisted cochain complexes whose coefficient systems are pulled back along homotopic maps. It is induced by transport along the pointwise paths of the homotopy.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexPullbackHomotopyIso_hom {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (L : LocalCoefficientSystem R Y) : (twistedCochainComplexPullbackHomotopyIso k M H L).hom = twistedCochainComplexCoefficientMap k M ((pullbackHomotopyIso H).hom.app L)

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexPullbackHomotopyIso_inv {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (L : LocalCoefficientSystem R Y) : (twistedCochainComplexPullbackHomotopyIso k M H L).inv = twistedCochainComplexCoefficientMap k M ((pullbackHomotopyIso H).inv.app L)

noncomputable def TauCeti.LocalCoefficientSystem.twistedCohomologyPullbackHomotopyIso {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y : TopCat} {f g : X ⟶ Y} (H : (TopCat.Hom.hom f).Homotopy (TopCat.Hom.hom g)) (L : LocalCoefficientSystem R Y) (n : ℕ) : twistedCohomology k M ((pullback (TopCat.Hom.hom g)).obj L) n ≅ twistedCohomology k M ((pullback (TopCat.Hom.hom f)).obj L) n

Homotopic pullbacks of a local coefficient system have canonically isomorphic twisted cohomology groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedCochainComplexMap {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) (L : LocalCoefficientSystem R Y) : twistedCochainComplex k M L ⟶ twistedCochainComplex k M ((pullback (TopCat.Hom.hom f)).obj L)

The cochain map induced by a continuous map f : X ⟶ Y, from the cochains of Y twisted by L to the cochains of X twisted by the pullback of L along f.

Equations

• TauCeti.LocalCoefficientSystem.twistedCochainComplexMap k M f L = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (TauCeti.LocalCoefficientSystem.twistedChainComplexMap f L).op

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexMap_f_apply {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) (L : LocalCoefficientSystem R Y) (n : ℕ) (g : ↑((twistedCochainComplex k M L).X n)) : (CategoryTheory.ConcreteCategory.hom ((twistedCochainComplexMap k M f L).f n)) g = CategoryTheory.CategoryStruct.comp ((twistedChainComplexMap f L).f n) g

The degree-n component of the cochain map induced by a continuous map acts by precomposition with the induced morphism of twisted chains.

@[reducible, inline]

noncomputable abbrev TauCeti.LocalCoefficientSystem.twistedCohomologyMap {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) (L : LocalCoefficientSystem R Y) (n : ℕ) : twistedCohomology k M L n ⟶ twistedCohomology k M ((pullback (TopCat.Hom.hom f)).obj L) n

The map on twisted cohomology induced by a continuous map.

Equations

• TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M f L n = HomologicalComplex.homologyMap (TauCeti.LocalCoefficientSystem.twistedCochainComplexMap k M f L) n

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexMap_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) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) : CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M η) (twistedCochainComplexMap k M f L) = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f K) (twistedCochainComplexCoefficientMap k M ((pullback (TopCat.Hom.hom f)).map η))

The cochain map induced by a continuous map is natural in the coefficient system.

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexMap_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) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) {Z : CochainComplex (ModuleCat k) ℕ} (h : twistedCochainComplex k M ((pullback (TopCat.Hom.hom f)).obj L) ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M η) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f L) h) = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f K) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M ((pullback (TopCat.Hom.hom f)).map η)) h)

The cochain map induced by a continuous map is natural in the coefficient system.

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyMap_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) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) (n : ℕ) : CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M η n) (twistedCohomologyMap k M f L n) = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f K n) (twistedCohomologyCoefficientMap k M ((pullback (TopCat.Hom.hom f)).map η) n)

The map induced on twisted cohomology by a continuous map is natural in the coefficient system.

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyMap_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) {L K : LocalCoefficientSystem R Y} (η : L ⟶ K) (n : ℕ) {Z : ModuleCat k} (h : twistedCohomology k M ((pullback (TopCat.Hom.hom f)).obj L) n ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M η n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f L n) h) = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f K n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M ((pullback (TopCat.Hom.hom f)).map η) n) h)

The map induced on twisted cohomology by a continuous map is natural in the coefficient system.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexMap_id {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} (L : LocalCoefficientSystem R X) : twistedCochainComplexMap k M (CategoryTheory.CategoryStruct.id X) L = twistedCochainComplexCoefficientMap k M ((pullbackIdIso X).hom.app L)

The identity map induces on twisted cochains the map coming from the identification of a coefficient system with its pullback along the identity.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexMap_comp {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) : twistedCochainComplexMap k M (CategoryTheory.CategoryStruct.comp f g) L = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M g L) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f ((pullback (TopCat.Hom.hom g)).obj L)) (twistedCochainComplexCoefficientMap k M ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L)))

A composite of continuous maps induces on twisted cochains the composite of the two induced maps, after the identification of the pullback along the composite with the iterated pullback.

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexMap_comp_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) {Z✝ : CochainComplex (ModuleCat k) ℕ} (h : twistedCochainComplex k M ((pullback (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g))).obj L) ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M (CategoryTheory.CategoryStruct.comp f g) L) h = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M g L) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f ((pullback (TopCat.Hom.hom g)).obj L)) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexCoefficientMap k M ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L)) h))

A composite of continuous maps induces on twisted cochains the composite of the two induced maps, after the identification of the pullback along the composite with the iterated pullback.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyMap_id {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X : TopCat} (L : LocalCoefficientSystem R X) (n : ℕ) : twistedCohomologyMap k M (CategoryTheory.CategoryStruct.id X) L n = twistedCohomologyCoefficientMap k M ((pullbackIdIso X).hom.app L) n

The cohomology form of twistedCochainComplexMap_id.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyMap_comp {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) (n : ℕ) : twistedCohomologyMap k M (CategoryTheory.CategoryStruct.comp f g) L n = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M g L n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f ((pullback (TopCat.Hom.hom g)).obj L) n) (twistedCohomologyCoefficientMap k M ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L) n))

The cohomology form of twistedCochainComplexMap_comp.

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyMap_comp_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {X Y Z : TopCat} (f : X ⟶ Y) (g : Y ⟶ Z) (L : LocalCoefficientSystem R Z) (n : ℕ) {Z✝ : ModuleCat k} (h : twistedCohomology k M ((pullback (TopCat.Hom.hom (CategoryTheory.CategoryStruct.comp f g))).obj L) n ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M (CategoryTheory.CategoryStruct.comp f g) L n) h = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M g L n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f ((pullback (TopCat.Hom.hom g)).obj L) n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyCoefficientMap k M ((pullbackCompIso (TopCat.Hom.hom f) (TopCat.Hom.hom g)).hom.app L) n) h))

The cohomology form of twistedCochainComplexMap_comp.

noncomputable def TauCeti.LocalCoefficientSystem.twistedCochainComplexConstantIso {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (X : TopCat) (N : ModuleCat R) : twistedCochainComplex k M ((constantFunctor X).obj N) ≅ TopCat.singularCochainComplex N k M X

For a constant local coefficient system, the twisted cochain complex is the ordinary singular cochain complex with the same coefficient module.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexConstantIso_hom {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (X : TopCat) (N : ModuleCat R) : (twistedCochainComplexConstantIso k M X N).hom = (ChainComplex.linearYonedaFunctor k M).map (twistedChainComplexConstantIso X N).inv.op

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCochainComplexConstantIso_inv {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (X : TopCat) (N : ModuleCat R) : (twistedCochainComplexConstantIso k M X N).inv = (ChainComplex.linearYonedaFunctor k M).map (twistedChainComplexConstantIso X N).hom.op

noncomputable def TauCeti.LocalCoefficientSystem.twistedCohomologyConstantIso {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (X : TopCat) (N : ModuleCat R) (n : ℕ) : twistedCohomology k M ((constantFunctor X).obj N) n ≅ TopCat.singularCohomology N k M X n

For a constant local coefficient system, twisted cohomology is ordinary singular cohomology.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyConstantIso_hom {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (X : TopCat) (N : ModuleCat R) (n : ℕ) : (twistedCohomologyConstantIso k M X N n).hom = HomologicalComplex.homologyMap (twistedCochainComplexConstantIso k M X N).hom n

@[simp]

theorem TauCeti.LocalCoefficientSystem.twistedCohomologyConstantIso_inv {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (X : TopCat) (N : ModuleCat R) (n : ℕ) : (twistedCohomologyConstantIso k M X N n).inv = HomologicalComplex.homologyMap (twistedCochainComplexConstantIso k M X N).inv n