Documentation

TauCeti.AlgebraicTopology.Cohomology.Twisted.Relative

Relative singular cohomology with local coefficients #

Let (X, A) be a topological pair and let L be a local coefficient system of R-modules on X. Applying Hom(-, M) to the relative twisted chains of the pair gives its relative twisted cochain complex, whose cohomology is the relative singular cohomology of (X, A) with coefficients in L and values in M.

The twisted chains of A sit inside those of X as the summands indexed by the singular simplices of A, so that inclusion is split in each degree. Applying Hom(-, M) to the short exact sequence 0 ⟶ C(A; L) ⟶ C(X; L) ⟶ C(X, A; L) ⟶ 0 therefore again gives a short exact sequence

0 ⟶ C*(X, A; L) ⟶ C*(X; L) ⟶ C*(A; L) ⟶ 0,

and its long exact cohomology sequence is the long exact sequence of the pair with local coefficients. This is the sequence in which the cap product with the orientation system expresses Poincaré--Lefschetz duality, so the twisted theory, and not only the untwisted one of TauCeti.AlgebraicTopology.Cohomology.Relative, is needed.

Main declarations #

TopPair.twistedCochainComplex and TopPair.twistedCohomology: the relative twisted cochain complex of a pair and its cohomology.
TopPair.twistedCochainComplexCoefficientMap and TopPair.twistedCohomologyCoefficientMap: change of local coefficient system.
TopPair.twistedCochainComplexMap and TopPair.twistedCohomologyMap: the maps induced by a map of topological pairs.
TopPair.shortExact_twistedCochainComplexShortComplex: the twisted cochain sequence of a pair is short exact.
TopPair.twistedCohomologyδ: the connecting morphism Hⁿ(A; L) ⟶ Hᵐ(X, A; L) for n + 1 = m, with the exactness statements TopPair.twistedCohomology_exact_relative, TopPair.twistedCohomology_exact_space and TopPair.twistedCohomology_exact_subspace, and its naturality TopPair.twistedCohomologyδ_naturality in maps of pairs and TopPair.twistedCohomologyδ_naturality_coefficient in morphisms of local coefficient systems.
TopPair.twistedCohomologyConstantIso: for a constant system, relative twisted cohomology is ordinary relative 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 TopPair.twistedCochainComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) :

CochainComplex (ModuleCat k) ℕ

The relative singular cochain complex of a topological pair with coefficients in a local coefficient system L on its ambient space and values in M: in degree n, the k-module of morphisms from the relative twisted n-chains to M.

Equations

P.twistedCochainComplex L k M = (P.twistedChainComplex L).linearYonedaObj k M

Instances For

@[reducible, inline]

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

The relative singular cohomology of a topological pair in degree n, with coefficients in a local coefficient system on its ambient space and values in M.

Equations

P.twistedCohomology L k M n = HomologicalComplex.homology (P.twistedCochainComplex L k M) n

Instances For

@[reducible, inline]

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

P.twistedCochainComplex K k M ⟶ P.twistedCochainComplex L k M

The cochain map on relative twisted cochains induced by a morphism of local coefficient systems.

Equations

P.twistedCochainComplexCoefficientMap k M η = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (P.twistedChainComplexCoefficientMap η).op

Instances For

@[simp]

theorem TopPair.twistedCochainComplexCoefficientMap_id {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (L : TauCeti.LocalCoefficientSystem R fst) :

P.twistedCochainComplexCoefficientMap k M (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id (P.twistedCochainComplex L k M)

theorem TopPair.twistedCochainComplexCoefficientMap_comp {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K J : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (θ : K ⟶ J) :

P.twistedCochainComplexCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (P.twistedCochainComplexCoefficientMap k M θ) (P.twistedCochainComplexCoefficientMap k M η)

theorem TopPair.twistedCochainComplexCoefficientMap_comp_assoc {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K J : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (θ : K ⟶ J) {Z : CochainComplex (ModuleCat k) ℕ} (h : P.twistedCochainComplex L k M ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.twistedCochainComplexCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (P.twistedCochainComplexCoefficientMap k M θ) (CategoryTheory.CategoryStruct.comp (P.twistedCochainComplexCoefficientMap k M η) h)

@[simp]

theorem TopPair.twistedCochainComplexCoefficientMap_f_apply {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (n : ℕ) (g : ↑((P.twistedCochainComplex K k M).X n)) :

(CategoryTheory.ConcreteCategory.hom ((P.twistedCochainComplexCoefficientMap k M η).f n)) g = CategoryTheory.CategoryStruct.comp ((P.twistedChainComplexCoefficientMap η).f n) g

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

@[reducible, inline]

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

P.twistedCohomology K k M n ⟶ P.twistedCohomology L k M n

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

Equations

P.twistedCohomologyCoefficientMap k M η n = HomologicalComplex.homologyMap (P.twistedCochainComplexCoefficientMap k M η) n

Instances For

@[simp]

theorem TopPair.twistedCohomologyCoefficientMap_id {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (L : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) :

P.twistedCohomologyCoefficientMap k M (CategoryTheory.CategoryStruct.id L) n = CategoryTheory.CategoryStruct.id (P.twistedCohomology L k M n)

theorem TopPair.twistedCohomologyCoefficientMap_comp {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K J : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (θ : K ⟶ J) (n : ℕ) :

P.twistedCohomologyCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ) n = CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M θ n) (P.twistedCohomologyCoefficientMap k M η n)

theorem TopPair.twistedCohomologyCoefficientMap_comp_assoc {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K J : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (θ : K ⟶ J) (n : ℕ) {Z : ModuleCat k} (h : P.twistedCohomology L k M n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M (CategoryTheory.CategoryStruct.comp η θ) n) h = CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M θ n) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M η n) h)

@[reducible, inline]

noncomputable abbrev TopPair.twistedCochainComplexShortComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) :

CategoryTheory.ShortComplex (CochainComplex (ModuleCat k) ℕ)

The twisted cochain sequence C*(X, A; L) ⟶ C*(X; L) ⟶ C*(A; L) of a topological pair (X, A): the image under Hom(-, M) of the twisted chain sequence of the pair.

Equations

P.twistedCochainComplexShortComplex L k M = (P.twistedChainComplexShortComplex L).op.map (TauCeti.ChainComplex.linearYonedaFunctor k M)

Instances For

theorem TopPair.twistedCochainComplexShortComplex_f_eq {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) :

(P.twistedCochainComplexShortComplex L k M).f = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (P.twistedChainComplexπ L).op

The first map of the twisted cochain sequence of a pair is the image under Hom(-, M) of the quotient map from ambient to relative twisted chains.

theorem TopPair.twistedCochainComplexShortComplex_g_eq {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) :

(P.twistedCochainComplexShortComplex L k M).g = TauCeti.LocalCoefficientSystem.twistedCochainComplexMap k M map L

The second map of the twisted cochain sequence of a pair is restriction from the ambient space to the subspace.

theorem TopPair.shortExact_twistedCochainComplexShortComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) :

(P.twistedCochainComplexShortComplex L k M).ShortExact

The twisted cochain sequence 0 ⟶ C*(X, A; L) ⟶ C*(X; L) ⟶ C*(A; L) ⟶ 0 of a topological pair is short exact.

@[reducible, inline]

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

P.twistedCohomology L k M n ⟶ TauCeti.LocalCoefficientSystem.twistedCohomology k M L n

The map Hⁿ(X, A; L) ⟶ Hⁿ(X; L) from relative to absolute twisted cohomology.

Equations

P.twistedCohomologyπ L k M n = HomologicalComplex.homologyMap (P.twistedCochainComplexShortComplex L k M).f n

Instances For

@[reducible, inline]

noncomputable abbrev TopPair.twistedCohomologyδ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n m : ℕ) (h : n + 1 = m := by lia) :

TauCeti.LocalCoefficientSystem.twistedCohomology k M (P.subspaceSystem L) n ⟶ P.twistedCohomology L k M m

The connecting morphism Hⁿ(A; L) ⟶ Hᵐ(X, A; L) of the long exact sequence of a topological pair, where n + 1 = m.

Equations

P.twistedCohomologyδ L k M n m h = ⋯.δ n m ⋯

Instances For

@[simp]

theorem TopPair.twistedCohomologyπ_comp_twistedCohomologyMap {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n : ℕ) :

CategoryTheory.CategoryStruct.comp (P.twistedCohomologyπ L k M n) (TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M map L n) = 0

@[simp]

theorem TopPair.twistedCohomologyπ_comp_twistedCohomologyMap_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n : ℕ) {Z : ModuleCat k} (h : TauCeti.LocalCoefficientSystem.twistedCohomology k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).obj L) n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.twistedCohomologyπ L k M n) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M map L n) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem TopPair.twistedCohomologyMap_comp_twistedCohomologyδ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n m : ℕ) (h : n + 1 = m := by lia) :

CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M map L n) (P.twistedCohomologyδ L k M n m h) = 0

@[simp]

theorem TopPair.twistedCohomologyMap_comp_twistedCohomologyδ_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : P.twistedCohomology L k M m ⟶ Z) :

CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M map L n) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyδ L k M n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopPair.twistedCohomology_exact_relative {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n m : ℕ) (h : n + 1 = m := by lia) :

{ X₁ := (P.twistedCochainComplexShortComplex L k M).X₃.homology n, X₂ := (P.twistedCochainComplexShortComplex L k M).X₁.homology m, X₃ := (P.twistedCochainComplexShortComplex L k M).X₂.homology m, f := ⋯.δ n m ⋯, g := HomologicalComplex.homologyMap (P.twistedCochainComplexShortComplex L k M).f m, zero := ⋯ }.Exact

Exactness at relative cohomology: Hⁿ(A; L) ⟶ Hᵐ(X, A; L) ⟶ Hᵐ(X; L) is exact for n + 1 = m.

theorem TopPair.twistedCohomology_exact_space {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n : ℕ) :

{ X₁ := P.twistedCohomology L k M n, X₂ := TauCeti.LocalCoefficientSystem.twistedCohomology k M L n, X₃ := TauCeti.LocalCoefficientSystem.twistedCohomology k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).obj L) n, f := P.twistedCohomologyπ L k M n, g := TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M map L n, zero := ⋯ }.Exact

Exactness at ambient cohomology: Hⁿ(X, A; L) ⟶ Hⁿ(X; L) ⟶ Hⁿ(A; L) is exact.

theorem TopPair.twistedCohomology_exact_subspace {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (n m : ℕ) (h : n + 1 = m := by lia) :

{ X₁ := TauCeti.LocalCoefficientSystem.twistedCohomology k M L n, X₂ := TauCeti.LocalCoefficientSystem.twistedCohomology k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).obj L) n, X₃ := P.twistedCohomology L k M m, f := TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M map L n, g := P.twistedCohomologyδ L k M n m h, zero := ⋯ }.Exact

Exactness at subspace cohomology: Hⁿ(X; L) ⟶ Hⁿ(A; L) ⟶ Hᵐ(X, A; L) is exact for n + 1 = m.

instance TopPair.instMonoModuleCatTwistedCohomologyπOfNatNat {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) :

CategoryTheory.Mono (P.twistedCohomologyπ L k M 0)

The map from relative to absolute twisted cohomology is a monomorphism in degree zero.

noncomputable def TopPair.twistedCochainComplexShortComplexCoefficientMap {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) :

P.twistedCochainComplexShortComplex K k M ⟶ P.twistedCochainComplexShortComplex L k M

The morphism between the twisted cochain sequences of a pair induced by a morphism of local coefficient systems.

Equations

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

Instances For

@[simp]

theorem TopPair.twistedCochainComplexShortComplexCoefficientMap_τ₁ {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) :

(P.twistedCochainComplexShortComplexCoefficientMap k M η).τ₁ = P.twistedCochainComplexCoefficientMap k M η

@[simp]

theorem TopPair.twistedCochainComplexShortComplexCoefficientMap_τ₂ {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) :

(P.twistedCochainComplexShortComplexCoefficientMap k M η).τ₂ = TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap k M η

@[simp]

theorem TopPair.twistedCochainComplexShortComplexCoefficientMap_τ₃ {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) :

(P.twistedCochainComplexShortComplexCoefficientMap k M η).τ₃ = TauCeti.LocalCoefficientSystem.twistedCochainComplexCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).map η)

theorem TopPair.twistedCohomologyπ_naturality_coefficient {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (n : ℕ) :

CategoryTheory.CategoryStruct.comp (P.twistedCohomologyπ K k M n) (TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap k M η n) = CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M η n) (P.twistedCohomologyπ L k M n)

The map from relative to absolute twisted cohomology commutes with a change of local coefficient system.

theorem TopPair.twistedCohomologyπ_naturality_coefficient_assoc {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (n : ℕ) {Z : ModuleCat k} (h : TauCeti.LocalCoefficientSystem.twistedCohomology k M L n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.twistedCohomologyπ K k M n) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap k M η n) h) = CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M η n) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyπ L k M n) h)

The map from relative to absolute twisted cohomology commutes with a change of local coefficient system.

theorem TopPair.twistedCohomologyδ_naturality_coefficient {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (n m : ℕ) (h : n + 1 = m := by lia) :

CategoryTheory.CategoryStruct.comp (P.twistedCohomologyδ K k M n m h) (P.twistedCohomologyCoefficientMap k M η m) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).map η) n) (P.twistedCohomologyδ L k M n m h)

The connecting morphism of the long exact sequence in relative twisted cohomology commutes with a change of local coefficient system.

theorem TopPair.twistedCohomologyδ_naturality_coefficient_assoc {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : P.twistedCohomology L k M m ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.twistedCohomologyδ K k M n m h) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M η m) h✝) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).map η) n) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyδ L k M n m h) h✝)

The connecting morphism of the long exact sequence in relative twisted cohomology commutes with a change of local coefficient system.

@[reducible, inline]

noncomputable abbrev TopPair.twistedCochainComplexMap {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) :

Q.twistedCochainComplex L k M ⟶ P.twistedCochainComplex ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M

The cochain map on relative twisted cochains induced by a map of topological pairs.

Equations

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

Instances For

@[simp]

theorem TopPair.twistedCochainComplexMap_f_apply {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) (g : ↑((Q.twistedCochainComplex L k M).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 relative cochain map induced by a map of pairs acts by precomposition with the induced morphism of relative twisted chains.

@[reducible, inline]

noncomputable abbrev TopPair.twistedCohomologyMap {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) :

Q.twistedCohomology L k M n ⟶ P.twistedCohomology ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M n

The map on relative twisted cohomology induced by a map of topological pairs.

Equations

TopPair.twistedCohomologyMap k M f L n = HomologicalComplex.homologyMap (TopPair.twistedCochainComplexMap k M f L) n

Instances For

theorem TopPair.twistedCochainComplexMap_naturality {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) :

CategoryTheory.CategoryStruct.comp (Q.twistedCochainComplexCoefficientMap k M η) (twistedCochainComplexMap k M f L) = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f K) (P.twistedCochainComplexCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η))

The relative cochain map induced by a map of pairs commutes with a change of coefficients on the target pair.

theorem TopPair.twistedCochainComplexMap_naturality_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) {Z : CochainComplex (ModuleCat k) ℕ} (h : P.twistedCochainComplex ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M ⟶ Z) :

CategoryTheory.CategoryStruct.comp (Q.twistedCochainComplexCoefficientMap k M η) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f L) h) = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f K) (CategoryTheory.CategoryStruct.comp (P.twistedCochainComplexCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η)) h)

The relative cochain map induced by a map of pairs commutes with a change of coefficients on the target pair.

theorem TopPair.twistedCohomologyMap_naturality {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (n : ℕ) :

CategoryTheory.CategoryStruct.comp (Q.twistedCohomologyCoefficientMap k M η n) (twistedCohomologyMap k M f L n) = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f K n) (P.twistedCohomologyCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η) n)

The cohomology form of TopPair.twistedCochainComplexMap_naturality.

theorem TopPair.twistedCohomologyMap_naturality_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (n : ℕ) {Z : ModuleCat k} (h : P.twistedCohomology ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (Q.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 (P.twistedCohomologyCoefficientMap k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η) n) h)

The cohomology form of TopPair.twistedCochainComplexMap_naturality.

@[simp]

theorem TopPair.twistedCochainComplexMap_id {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) :

twistedCochainComplexMap k M (CategoryTheory.CategoryStruct.id P) L = P.twistedCochainComplexCoefficientMap k M (P.fstPullbackIdIso L).hom

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

@[simp]

theorem TopPair.twistedCohomologyMap_id {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) :

twistedCohomologyMap k M (CategoryTheory.CategoryStruct.id P) L n = P.twistedCohomologyCoefficientMap k M (P.fstPullbackIdIso L).hom n

The cohomology form of TopPair.twistedCochainComplexMap_id.

@[simp]

theorem TopPair.twistedCochainComplexMap_comp {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) :

twistedCochainComplexMap k M (CategoryTheory.CategoryStruct.comp f g) K = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M g K) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K)) (P.twistedCochainComplexCoefficientMap k M (fstPullbackCompIso f g K).hom))

Maps of relative twisted cochain complexes respect composition of maps of pairs, after the canonical comparison between pullback along a composite and iterated pullback.

theorem TopPair.twistedCochainComplexMap_comp_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) {Z : CochainComplex (ModuleCat k) ℕ} (h : P.twistedCochainComplex ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst (CategoryTheory.CategoryStruct.comp f g)))).obj K) k M ⟶ Z) :

CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M (CategoryTheory.CategoryStruct.comp f g) K) h = CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M g K) (CategoryTheory.CategoryStruct.comp (twistedCochainComplexMap k M f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K)) (CategoryTheory.CategoryStruct.comp (P.twistedCochainComplexCoefficientMap k M (fstPullbackCompIso f g K).hom) h))

Maps of relative twisted cochain complexes respect composition of maps of pairs, after the canonical comparison between pullback along a composite and iterated pullback.

@[simp]

theorem TopPair.twistedCohomologyMap_comp {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) :

twistedCohomologyMap k M (CategoryTheory.CategoryStruct.comp f g) K n = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M g K n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K) n) (P.twistedCohomologyCoefficientMap k M (fstPullbackCompIso f g K).hom n))

The cohomology form of TopPair.twistedCochainComplexMap_comp.

theorem TopPair.twistedCohomologyMap_comp_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) {Z : ModuleCat k} (h : P.twistedCohomology ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst (CategoryTheory.CategoryStruct.comp f g)))).obj K) k M n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M (CategoryTheory.CategoryStruct.comp f g) K n) h = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M g K n) (CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K) n) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyCoefficientMap k M (fstPullbackCompIso f g K).hom n) h))

The cohomology form of TopPair.twistedCochainComplexMap_comp.

@[reducible, inline]

noncomputable abbrev TopPair.twistedSubspaceCochainComplexMap {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) :

TauCeti.LocalCoefficientSystem.twistedCochainComplex k M (Q.subspaceSystem L) ⟶ TauCeti.LocalCoefficientSystem.twistedCochainComplex k M (P.subspaceSystem ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L))

The cochain map on subspace twisted cochains induced by a map of pairs: restriction along the subspace component, after the canonical comparison of the pulled-back coefficient systems.

Equations

TopPair.twistedSubspaceCochainComplexMap k M f L = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (TopPair.twistedSubspaceChainComplexMap f L).op

Instances For

noncomputable def TopPair.twistedCochainComplexShortComplexMap {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) :

Q.twistedCochainComplexShortComplex L k M ⟶ P.twistedCochainComplexShortComplex ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M

The morphism between the twisted cochain sequences of two pairs induced by a map of pairs.

Equations

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

Instances For

@[simp]

theorem TopPair.twistedCochainComplexShortComplexMap_τ₁ {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) :

(twistedCochainComplexShortComplexMap k M f L).τ₁ = twistedCochainComplexMap k M f L

@[simp]

theorem TopPair.twistedCochainComplexShortComplexMap_τ₂ {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) :

(twistedCochainComplexShortComplexMap k M f L).τ₂ = TauCeti.LocalCoefficientSystem.twistedCochainComplexMap k M (Hom.fst f) L

@[simp]

theorem TopPair.twistedCochainComplexShortComplexMap_τ₃ {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) :

(twistedCochainComplexShortComplexMap k M f L).τ₃ = twistedSubspaceCochainComplexMap k M f L

theorem TopPair.twistedCohomologyπ_naturality {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) :

CategoryTheory.CategoryStruct.comp (Q.twistedCohomologyπ L k M n) (TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M (Hom.fst f) L n) = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f L n) (P.twistedCohomologyπ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M n)

The map from relative to absolute twisted cohomology is natural in the pair.

theorem TopPair.twistedCohomologyπ_naturality_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (n : ℕ) {Z : ModuleCat k} (h : TauCeti.LocalCoefficientSystem.twistedCohomology k M ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) n ⟶ Z) :

CategoryTheory.CategoryStruct.comp (Q.twistedCohomologyπ L k M n) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedCohomologyMap k M (Hom.fst f) L n) h) = CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f L n) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyπ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M n) h)

The map from relative to absolute twisted cohomology is natural in the pair.

theorem TopPair.twistedCohomologyδ_naturality {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : n + 1 = m := by lia) :

CategoryTheory.CategoryStruct.comp (Q.twistedCohomologyδ L k M n m h) (twistedCohomologyMap k M f L m) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (twistedSubspaceCochainComplexMap k M f L) n) (P.twistedCohomologyδ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M n m h)

The connecting morphism of the long exact sequence in relative twisted cohomology is natural in maps of topological pairs.

theorem TopPair.twistedCohomologyδ_naturality_assoc {R : Type u} [Ring R] (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M : ModuleCat R) {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : P.twistedCohomology ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M m ⟶ Z) :

CategoryTheory.CategoryStruct.comp (Q.twistedCohomologyδ L k M n m h) (CategoryTheory.CategoryStruct.comp (twistedCohomologyMap k M f L m) h✝) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (twistedSubspaceCochainComplexMap k M f L) n) (CategoryTheory.CategoryStruct.comp (P.twistedCohomologyδ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k M n m h) h✝)

The connecting morphism of the long exact sequence in relative twisted cohomology is natural in maps of topological pairs.

noncomputable def TopPair.twistedCochainComplexConstantIso {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M N : ModuleCat R) :

P.twistedCochainComplex ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj N) k M ≅ P.singularCochainComplex N k M

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

Equations

P.twistedCochainComplexConstantIso k M N = ((TauCeti.ChainComplex.linearYonedaFunctor k M).mapIso (P.twistedChainComplexConstantIso N).op).symm

Instances For

@[simp]

theorem TopPair.twistedCochainComplexConstantIso_hom {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M N : ModuleCat R) :

(P.twistedCochainComplexConstantIso k M N).hom = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (P.twistedChainComplexConstantIso N).inv.op

@[simp]

theorem TopPair.twistedCochainComplexConstantIso_inv {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M N : ModuleCat R) :

(P.twistedCochainComplexConstantIso k M N).inv = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (P.twistedChainComplexConstantIso N).hom.op

noncomputable def TopPair.twistedCohomologyConstantIso {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M N : ModuleCat R) (n : ℕ) :

P.twistedCohomology ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj N) k M n ≅ P.singularCohomology N k M n

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

Equations

P.twistedCohomologyConstantIso k M N n = (HomologicalComplex.homologyFunctor (ModuleCat k) (ComplexShape.up ℕ) n).mapIso (P.twistedCochainComplexConstantIso k M N)

Instances For

@[simp]

theorem TopPair.twistedCohomologyConstantIso_hom {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M N : ModuleCat R) (n : ℕ) :

(P.twistedCohomologyConstantIso k M N n).hom = HomologicalComplex.homologyMap (P.twistedCochainComplexConstantIso k M N).hom n

@[simp]

theorem TopPair.twistedCohomologyConstantIso_inv {R : Type u} [Ring R] (P : TopPair) (k : Type u_1) [Ring k] [CategoryTheory.Linear k (ModuleCat R)] (M N : ModuleCat R) (n : ℕ) :

(P.twistedCohomologyConstantIso k M N n).inv = HomologicalComplex.homologyMap (P.twistedCochainComplexConstantIso k M N).inv n