Relative singular chains and homology with local coefficients

Let (X, A) be a topological pair and let L be a local coefficient system on X. Restricting L along the inclusion of A twists the singular chains of A, and because the singular simplices of A inject into those of X the resulting map into the twisted chains of X is a monomorphism in every degree. Its cokernel is the relative twisted chain complex of the pair, whose homology is relative singular homology with coefficients in L.

This file constructs that complex, records the short exact sequence of chain complexes it sits in, and derives from it the long exact sequence relating the twisted homology of A, of X, and of the pair. For a constant system the relative complex is the ordinary relative singular chain complex, compatibly with the quotient maps from the chains of the ambient space, and the same comparison in homology identifies relative twisted homology with ordinary relative homology.

Relative homology with local coefficients is the form in which cap products against the orientation system express manifold duality, which is what makes the relative theory, and not only the absolute one of TauCeti.AlgebraicTopology.Singular.Twisted.Basic, necessary.

Main declarations

• TopPair.twistedChainComplex: the relative twisted singular chain complex of a pair, presented as a cokernel by TopPair.isColimitCokernelCoforkTwistedChainComplex.
• TopPair.twistedChainComplexCoefficientMap: change of local coefficients on relative chains, with the corresponding TopPair.twistedHomologyCoefficientMap.
• TopPair.shortExact_twistedChainComplexShortComplex: the twisted chains of the subspace, of the ambient space and of the pair form a short exact sequence of chain complexes.
• TopPair.twistedHomology, TopPair.twistedHomologyπ and TopPair.twistedHomologyδ, with the three exactness statements TopPair.twistedHomology_exact_subspace, TopPair.twistedHomology_exact_space and TopPair.twistedHomology_exact_relative.
• TopPair.twistedHomologyConstantIso: for a constant system, relative twisted homology is ordinary relative singular homology.

The cokernel presentation, the short exact sequence and the shape of the three exactness statements follow Mathlib's relative simplicial homology (Mathlib.AlgebraicTopology.SimplicialSet.Homology.Relative, by Joël Riou and Andrew Yang), of which this is the twisted analogue; TauCeti.AlgebraicTopology.Singular.Relative is its untwisted topological specialization.

References

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

@[reducible, inline]

noncomputable abbrev TopPair.subspaceSystem {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : TauCeti.LocalCoefficientSystem R snd

The restriction to the subspace of a topological pair of a local coefficient system on its ambient space, that is, the pullback of the system along the inclusion.

Equations

• P.subspaceSystem L = (TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom TopPair.map)).obj L

noncomputable def TopPair.twistedChainComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : ChainComplex (ModuleCat R) ℕ

The relative twisted singular chain complex of a topological pair (X, A) with coefficients in a local coefficient system L on X: the quotient of the twisted chains of X by the twisted chains of A.

Equations

• P.twistedChainComplex L = CategoryTheory.Limits.cokernel (TauCeti.LocalCoefficientSystem.twistedChainComplexMap TopPair.map L)

noncomputable def TopPair.twistedChainComplexπ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : L.twistedChainComplex ⟶ P.twistedChainComplex L

The quotient map from the twisted chains of the ambient space onto the relative twisted chains of the pair.

Equations

• P.twistedChainComplexπ L = CategoryTheory.Limits.cokernel.π (TauCeti.LocalCoefficientSystem.twistedChainComplexMap TopPair.map L)

instance TopPair.instEpiChainComplexModuleCatNatTwistedChainComplexπ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.Epi (P.twistedChainComplexπ L)

@[simp]

theorem TopPair.twistedChainComplexMap_comp_twistedChainComplexπ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L) (P.twistedChainComplexπ L) = 0

@[simp]

theorem TopPair.twistedChainComplexMap_comp_twistedChainComplexπ_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) {Z : ChainComplex (ModuleCat R) ℕ} (h : P.twistedChainComplex L ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def TopPair.cokernelCoforkTwistedChainComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.Limits.CokernelCofork (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L)

The cokernel cofork presenting the relative twisted chain complex of a pair as the quotient of the ambient twisted chains by the twisted chains of the subspace.

Equations

• P.cokernelCoforkTwistedChainComplex L = CategoryTheory.Limits.CokernelCofork.ofπ (P.twistedChainComplexπ L) ⋯

noncomputable def TopPair.isColimitCokernelCoforkTwistedChainComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.Limits.IsColimit (P.cokernelCoforkTwistedChainComplex L)

The relative twisted chain complex of a pair is the cokernel of the inclusion of the twisted chains of its subspace.

Equations

• P.isColimitCokernelCoforkTwistedChainComplex L = CategoryTheory.Limits.cokernelIsCokernel (TauCeti.LocalCoefficientSystem.twistedChainComplexMap TopPair.map L)

noncomputable def TopPair.twistedChainComplexDesc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) {K : ChainComplex (ModuleCat R) ℕ} (k : L.twistedChainComplex ⟶ K) (hk : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L) k = 0) : P.twistedChainComplex L ⟶ K

Descend a map out of the ambient twisted chains to the relative twisted chain complex when it vanishes on the chains of the subspace.

Equations

• P.twistedChainComplexDesc L k hk = CategoryTheory.Limits.cokernel.desc (TauCeti.LocalCoefficientSystem.twistedChainComplexMap TopPair.map L) k hk

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexDesc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) {K : ChainComplex (ModuleCat R) ℕ} (k : L.twistedChainComplex ⟶ K) (hk : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L) k = 0) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) (P.twistedChainComplexDesc L k hk) = k

The map descended to relative twisted chains agrees with the original map after the quotient map from the ambient twisted chains.

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexDesc_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) {K : ChainComplex (ModuleCat R) ℕ} (k : L.twistedChainComplex ⟶ K) (hk : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L) k = 0) {Z : ChainComplex (ModuleCat R) ℕ} (h : K ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexDesc L k hk) h) = CategoryTheory.CategoryStruct.comp k h

The map descended to relative twisted chains agrees with the original map after the quotient map from the ambient twisted chains.

theorem TopPair.twistedChainComplex_hom_ext {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) {K : ChainComplex (ModuleCat R) ℕ} {f g : P.twistedChainComplex L ⟶ K} (h : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) f = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) g) : f = g

Two maps out of a relative twisted chain complex agree if they agree after the quotient map from ambient twisted chains.

theorem TopPair.twistedChainComplex_hom_ext_iff {R : Type u} [Ring R] {P : TopPair} {L : TauCeti.LocalCoefficientSystem R fst} {K : ChainComplex (ModuleCat R) ℕ} {f g : P.twistedChainComplex L ⟶ K} : f = g ↔ CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) f = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) g

noncomputable def TopPair.twistedChainComplexCoefficientMap {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) : P.twistedChainComplex L ⟶ P.twistedChainComplex K

A morphism of local coefficient systems induces a map of relative twisted chain complexes.

Equations

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

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexCoefficientMap {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) (P.twistedChainComplexCoefficientMap η) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap η) (P.twistedChainComplexπ K)

The relative coefficient map commutes with the quotient maps from ambient twisted chains.

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexCoefficientMap_assoc {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) {Z : ChainComplex (ModuleCat R) ℕ} (h : P.twistedChainComplex K ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ L) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap η) h) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap η) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ K) h)

The relative coefficient map commutes with the quotient maps from ambient twisted chains.

@[simp]

theorem TopPair.twistedChainComplexCoefficientMap_id {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : P.twistedChainComplexCoefficientMap (CategoryTheory.CategoryStruct.id L) = CategoryTheory.CategoryStruct.id (P.twistedChainComplex L)

The identity of a coefficient system induces the identity on relative twisted chains.

@[simp]

theorem TopPair.twistedChainComplexCoefficientMap_comp {R : Type u} [Ring R] (P : TopPair) {L K J : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (θ : K ⟶ J) : P.twistedChainComplexCoefficientMap (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap η) (P.twistedChainComplexCoefficientMap θ)

Relative twisted chain maps respect composition of coefficient morphisms.

theorem TopPair.twistedChainComplexCoefficientMap_comp_assoc {R : Type u} [Ring R] (P : TopPair) {L K J : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (θ : K ⟶ J) {Z : ChainComplex (ModuleCat R) ℕ} (h : P.twistedChainComplex J ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap η) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap θ) h)

Relative twisted chain maps respect composition of coefficient morphisms.

noncomputable def TopPair.twistedChainComplexCoefficientIso {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (e : L ≅ K) : P.twistedChainComplex L ≅ P.twistedChainComplex K

An isomorphism of coefficient systems induces an isomorphism of relative twisted chain complexes.

Equations

• P.twistedChainComplexCoefficientIso e = { hom := P.twistedChainComplexCoefficientMap e.hom, inv := P.twistedChainComplexCoefficientMap e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem TopPair.twistedChainComplexCoefficientIso_hom {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (e : L ≅ K) : (P.twistedChainComplexCoefficientIso e).hom = P.twistedChainComplexCoefficientMap e.hom

@[simp]

theorem TopPair.twistedChainComplexCoefficientIso_inv {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (e : L ≅ K) : (P.twistedChainComplexCoefficientIso e).inv = P.twistedChainComplexCoefficientMap e.inv

@[reducible, inline]

noncomputable abbrev TopPair.twistedChainComplexShortComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.ShortComplex (ChainComplex (ModuleCat R) ℕ)

The twisted chain sequence of a topological pair: the twisted chains of the subspace, of the ambient space, and of the pair.

Equations

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

noncomputable def TopPair.twistedChainComplexShortComplexCoefficientMap {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) : P.twistedChainComplexShortComplex L ⟶ P.twistedChainComplexShortComplex K

A coefficient morphism gives a morphism of the short exact twisted chain sequences of a pair.

Equations

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

@[simp]

theorem TopPair.twistedChainComplexShortComplexCoefficientMap_τ₁ {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) : (P.twistedChainComplexShortComplexCoefficientMap f).τ₁ = TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).map f)

@[simp]

theorem TopPair.twistedChainComplexShortComplexCoefficientMap_τ₂ {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) : (P.twistedChainComplexShortComplexCoefficientMap f).τ₂ = TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap f

@[simp]

theorem TopPair.twistedChainComplexShortComplexCoefficientMap_τ₃ {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) : (P.twistedChainComplexShortComplexCoefficientMap f).τ₃ = P.twistedChainComplexCoefficientMap f

theorem TopPair.shortExact_twistedChainComplexShortComplex {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : (P.twistedChainComplexShortComplex L).ShortExact

The twisted chain sequence of a topological pair is short exact.

@[reducible, inline]

noncomputable abbrev TopPair.twistedHomology {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : ModuleCat R

The relative singular homology of a topological pair in degree k, with coefficients in a local coefficient system on the ambient space.

Equations

• P.twistedHomology L k = HomologicalComplex.homology (P.twistedChainComplex L) k

@[reducible, inline]

noncomputable abbrev TopPair.twistedHomologyπ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : L.twistedHomology k ⟶ P.twistedHomology L k

The map from the twisted homology of the ambient space of a pair to the relative twisted homology of the pair.

Equations

• P.twistedHomologyπ L k = HomologicalComplex.homologyMap (P.twistedChainComplexπ L) k

@[reducible, inline]

noncomputable abbrev TopPair.twistedHomologyCoefficientMap {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) (k : ℕ) : P.twistedHomology L k ⟶ P.twistedHomology K k

A morphism of local coefficient systems induces a map on relative twisted homology.

Equations

• P.twistedHomologyCoefficientMap f k = HomologicalComplex.homologyMap (P.twistedChainComplexCoefficientMap f) k

@[simp]

theorem TopPair.twistedHomologyπ_comp_twistedHomologyCoefficientMap {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) (k : ℕ) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ L k) (P.twistedHomologyCoefficientMap f k) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap f k) (P.twistedHomologyπ K k)

Relative coefficient maps commute with the quotient maps from ambient to relative twisted homology.

@[simp]

theorem TopPair.twistedHomologyπ_comp_twistedHomologyCoefficientMap_assoc {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) (k : ℕ) {Z : ModuleCat R} (h : P.twistedHomology K k ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ L k) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap f k) h) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap f k) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ K k) h)

Relative coefficient maps commute with the quotient maps from ambient to relative twisted homology.

@[simp]

theorem TopPair.twistedHomologyCoefficientMap_id {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : P.twistedHomologyCoefficientMap (CategoryTheory.CategoryStruct.id L) k = CategoryTheory.CategoryStruct.id (P.twistedHomology L k)

The identity coefficient morphism induces the identity on relative twisted homology.

@[simp]

theorem TopPair.twistedHomologyCoefficientMap_comp {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) {K J : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) (g : K ⟶ J) (k : ℕ) : P.twistedHomologyCoefficientMap (CategoryTheory.CategoryStruct.comp f g) k = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap f k) (P.twistedHomologyCoefficientMap g k)

Relative twisted homology maps respect composition of coefficient morphisms.

theorem TopPair.twistedHomologyCoefficientMap_comp_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) {K J : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) (g : K ⟶ J) (k : ℕ) {Z : ModuleCat R} (h : P.twistedHomology J k ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap (CategoryTheory.CategoryStruct.comp f g) k) h = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap f k) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap g k) h)

Relative twisted homology maps respect composition of coefficient morphisms.

@[simp]

theorem TopPair.twistedHomologyMap_comp_twistedHomologyπ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyMap map L k) (P.twistedHomologyπ L k) = 0

@[simp]

theorem TopPair.twistedHomologyMap_comp_twistedHomologyπ_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) {Z : ModuleCat R} (h : P.twistedHomology L k ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyMap map L k) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ L k) h) = CategoryTheory.CategoryStruct.comp 0 h

instance TopPair.instEpiModuleCatTwistedHomologyπOfNatNat {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.Epi (P.twistedHomologyπ L 0)

The map from ambient twisted homology to relative twisted homology is an epimorphism in degree zero.

@[reducible, inline]

noncomputable abbrev TopPair.twistedHomologyδ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : m + 1 = n := by lia) : P.twistedHomology L n ⟶ (P.subspaceSystem L).twistedHomology m

The connecting morphism from the relative twisted homology of a pair in degree n to the twisted homology of its subspace in degree m, where m + 1 = n.

Equations

• P.twistedHomologyδ L n m h = ⋯.δ n m ⋯

theorem TopPair.twistedHomologyδ_naturality_coefficient {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyδ L n m h) (TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).map f) m) = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap f n) (P.twistedHomologyδ K n m h)

The connecting morphism in relative twisted homology commutes with change of local coefficients.

theorem TopPair.twistedHomologyδ_naturality_coefficient_assoc {R : Type u} [Ring R] (P : TopPair) {L K : TauCeti.LocalCoefficientSystem R fst} (f : L ⟶ K) (n m : ℕ) (h : m + 1 = n := by lia) {Z : ModuleCat R} (h✝ : ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).obj K).twistedHomology m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyδ L n m h) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).map f) m) h✝) = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap f n) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyδ K n m h) h✝)

The connecting morphism in relative twisted homology commutes with change of local coefficients.

@[simp]

theorem TopPair.twistedHomologyδ_comp {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyδ L n m h) (TauCeti.LocalCoefficientSystem.twistedHomologyMap map L m) = 0

@[simp]

theorem TopPair.twistedHomologyδ_comp_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : m + 1 = n := by lia) {Z : ModuleCat R} (h✝ : L.twistedHomology m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyδ L n m h) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyMap map L m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TopPair.twistedHomologyπ_comp_twistedHomologyδ {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ L n) (P.twistedHomologyδ L n m h) = 0

@[simp]

theorem TopPair.twistedHomologyπ_comp_twistedHomologyδ_assoc {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : m + 1 = n := by lia) {Z : ModuleCat R} (h✝ : (P.subspaceSystem L).twistedHomology m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ L n) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyδ L n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopPair.twistedHomology_exact_subspace {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := P.twistedHomology L n, X₂ := (P.subspaceSystem L).twistedHomology m, X₃ := L.twistedHomology m, f := P.twistedHomologyδ L n m h, g := TauCeti.LocalCoefficientSystem.twistedHomologyMap map L m, zero := ⋯ }.Exact

Exactness at the twisted homology of the subspace in the long exact sequence of a pair.

theorem TopPair.twistedHomology_exact_space {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : { X₁ := ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom map)).obj L).twistedHomology k, X₂ := L.twistedHomology k, X₃ := P.twistedHomology L k, f := TauCeti.LocalCoefficientSystem.twistedHomologyMap map L k, g := P.twistedHomologyπ L k, zero := ⋯ }.Exact

Exactness at the twisted homology of the ambient space in the long exact sequence of a pair.

theorem TopPair.twistedHomology_exact_relative {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := L.twistedHomology n, X₂ := P.twistedHomology L n, X₃ := (P.subspaceSystem L).twistedHomology m, f := P.twistedHomologyπ L n, g := P.twistedHomologyδ L n m h, zero := ⋯ }.Exact

Exactness at the relative twisted homology in the long exact sequence of a pair.

noncomputable def TopPair.twistedChainComplexConstantIso {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) : P.twistedChainComplex ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M) ≅ P.singularChainComplex M

For a constant local coefficient system, the relative twisted chain complex of a pair is the ordinary relative singular chain complex with the same coefficient module: both are the cokernel of the same inclusion of subspace chains, once the restriction of a constant system is identified with the constant system.

Equations

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

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexConstantIso_hom {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M)) (P.twistedChainComplexConstantIso M).hom = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso fst M).hom (P.singularChainComplexπ M)

The comparison of relative twisted chains with ordinary relative singular chains is compatible with the quotient maps from the chains of the ambient space.

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexConstantIso_hom_assoc {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) {Z : ChainComplex (ModuleCat R) ℕ} (h : P.singularChainComplex M ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M)) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexConstantIso M).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso fst M).hom (P.singularChainComplexπ M)) h

The comparison of relative twisted chains with ordinary relative singular chains is compatible with the quotient maps from the chains of the ambient space.

noncomputable def TopPair.twistedHomologyConstantIso {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) (k : ℕ) : P.twistedHomology ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M) k ≅ P.singularHomology M k

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

Equations

• P.twistedHomologyConstantIso M k = (HomologicalComplex.homologyFunctor (ModuleCat R) (ComplexShape.down ℕ) k).mapIso (P.twistedChainComplexConstantIso M)

theorem TopPair.twistedHomologyConstantIso_hom {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) (k : ℕ) : (P.twistedHomologyConstantIso M k).hom = HomologicalComplex.homologyMap (P.twistedChainComplexConstantIso M).hom k

The comparison of relative twisted homology with ordinary relative singular homology is the map induced on homology by the comparison of the relative chain complexes.

theorem TopPair.twistedHomologyConstantIso_inv {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) (k : ℕ) : (P.twistedHomologyConstantIso M k).inv = HomologicalComplex.homologyMap (P.twistedChainComplexConstantIso M).inv k

The inverse of the comparison of relative twisted homology with ordinary relative singular homology is the map induced on homology by the inverse comparison of the relative chain complexes.

@[simp]

theorem TopPair.twistedHomologyπ_comp_twistedHomologyConstantIso_hom {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) (k : ℕ) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M) k) (P.twistedHomologyConstantIso M k).hom = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso fst M k).hom (P.singularHomologyπ M k)

The comparison of relative twisted homology with ordinary relative singular homology is compatible with the maps from the homology of the ambient space.

@[simp]

theorem TopPair.twistedHomologyπ_comp_twistedHomologyConstantIso_hom_assoc {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) (k : ℕ) {Z : ModuleCat R} (h : P.singularHomology M k ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M) k) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyConstantIso M k).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso fst M k).hom (P.singularHomologyπ M k)) h

The comparison of relative twisted homology with ordinary relative singular homology is compatible with the maps from the homology of the ambient space.