Documentation

TauCeti.AlgebraicTopology.Singular.Twisted.ConstantNaturality

The constant-system comparison for relative singular homology #

The comparison of relative twisted chains with ordinary relative singular chains commutes with maps of pairs and changes of the coefficient module. It identifies the short exact sequences of chains, and hence the connecting maps in the long exact sequences, with no change of sign. These identities allow calculations with ordinary relative homology to be used in the local-coefficient theory.

The restriction and pullback of a constant system are identified with the constant system by LocalCoefficientSystem.pullbackConstantIso. In particular, the pair-map square retains the coefficient comparison on its source rather than treating pullback as a strict equality.

References #

A. Hatcher, Algebraic Topology, Section 3.H.
A. Dold, Lectures on Algebraic Topology, Chapters VII–VIII.

theorem TopPair.twistedChainComplexConstantIso_hom_pair_naturality {R : Type u} [Ring R] {P Q : TopPair} (M : ModuleCat R) (f : P ⟶ Q) :

CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M)) (Q.twistedChainComplexConstantIso M).hom = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap (TauCeti.LocalCoefficientSystem.pullbackConstantIso (TopCat.Hom.hom (Hom.fst f)) M).hom) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexConstantIso M).hom (singularChainComplexMap f M))

The constant-system comparison on relative chains is natural in maps of pairs, after identifying the pullback of the target constant system with the source constant system.

theorem TopPair.twistedChainComplexConstantIso_hom_pair_naturality_assoc {R : Type u} [Ring R] {P Q : TopPair} (M : ModuleCat R) (f : P ⟶ Q) {Z : ChainComplex (ModuleCat R) ℕ} (h : Q.singularChainComplex M ⟶ Z) :

The constant-system comparison on relative chains is natural in maps of pairs, after identifying the pullback of the target constant system with the source constant system.

theorem TopPair.twistedHomologyConstantIso_hom_pair_naturality {R : Type u} [Ring R] {P Q : TopPair} (M : ModuleCat R) (f : P ⟶ Q) (n : ℕ) :

CategoryTheory.CategoryStruct.comp (twistedHomologyMap f ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M) n) (Q.twistedHomologyConstantIso M n).hom = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap (TauCeti.LocalCoefficientSystem.pullbackConstantIso (TopCat.Hom.hom (Hom.fst f)) M).hom n) (CategoryTheory.CategoryStruct.comp (P.twistedHomologyConstantIso M n).hom (TopPair.singularHomologyMap f M n))

The constant-system comparison on relative homology is natural in maps of pairs.

theorem TopPair.twistedHomologyConstantIso_hom_pair_naturality_assoc {R : Type u} [Ring R] {P Q : TopPair} (M : ModuleCat R) (f : P ⟶ Q) (n : ℕ) {Z : ModuleCat R} (h : Q.singularHomology M n ⟶ Z) :

The constant-system comparison on relative homology is natural in maps of pairs.

theorem TopPair.twistedChainComplexConstantIso_hom_naturality {R : Type u} [Ring R] (P : TopPair) {M N : ModuleCat R} (φ : M ⟶ N) :

CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap ((TauCeti.LocalCoefficientSystem.constantFunctor fst).map φ)) (P.twistedChainComplexConstantIso N).hom = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexConstantIso M).hom (((SSetPair.chainComplexFunctor (ModuleCat R)).map φ).app (toSSetPair.obj P))

The constant-system comparison on relative chains is natural in the coefficient module.

theorem TopPair.twistedChainComplexConstantIso_hom_naturality_assoc {R : Type u} [Ring R] (P : TopPair) {M N : ModuleCat R} (φ : M ⟶ N) {Z : ChainComplex (ModuleCat R) ℕ} (h : P.singularChainComplex N ⟶ Z) :

CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap ((TauCeti.LocalCoefficientSystem.constantFunctor fst).map φ)) (CategoryTheory.CategoryStruct.comp (P.twistedChainComplexConstantIso N).hom h) = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexConstantIso M).hom (CategoryTheory.CategoryStruct.comp (((SSetPair.chainComplexFunctor (ModuleCat R)).map φ).app (toSSetPair.obj P)) h)

The constant-system comparison on relative chains is natural in the coefficient module.

theorem TopPair.twistedHomologyConstantIso_hom_naturality {R : Type u} [Ring R] (P : TopPair) {M N : ModuleCat R} (φ : M ⟶ N) (n : ℕ) :

CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap ((TauCeti.LocalCoefficientSystem.constantFunctor fst).map φ) n) (P.twistedHomologyConstantIso N n).hom = CategoryTheory.CategoryStruct.comp (P.twistedHomologyConstantIso M n).hom (HomologicalComplex.homologyMap (((SSetPair.chainComplexFunctor (ModuleCat R)).map φ).app (toSSetPair.obj P)) n)

The constant-system comparison on relative homology is natural in the coefficient module. The ordinary coefficient map is induced by the relative singular chain bifunctor.

theorem TopPair.twistedHomologyConstantIso_hom_naturality_assoc {R : Type u} [Ring R] (P : TopPair) {M N : ModuleCat R} (φ : M ⟶ N) (n : ℕ) {Z : ModuleCat R} (h : P.singularHomology N n ⟶ Z) :

The constant-system comparison on relative homology is natural in the coefficient module. The ordinary coefficient map is induced by the relative singular chain bifunctor.

noncomputable def TopPair.twistedChainComplexShortComplexConstantIso {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) :

P.twistedChainComplexShortComplex ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M) ≅ P.singularChainComplexShortComplex M

The constant-system comparison identifies the entire short exact chain sequence of a pair with its ordinary singular chain sequence. On subspace chains it first identifies the restriction of the ambient constant system with the constant system on the subspace.

Equations

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

Instances For

@[simp]

theorem TopPair.twistedChainComplexShortComplexConstantIso_hom_τ₁ {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) :

(P.twistedChainComplexShortComplexConstantIso M).hom.τ₁ = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap (TauCeti.LocalCoefficientSystem.pullbackConstantIso (TopCat.Hom.hom map) M).hom) (TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso snd M).hom

@[simp]

theorem TopPair.twistedChainComplexShortComplexConstantIso_hom_τ₂ {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) :

(P.twistedChainComplexShortComplexConstantIso M).hom.τ₂ = (TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso fst M).hom

@[simp]

theorem TopPair.twistedChainComplexShortComplexConstantIso_hom_τ₃ {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) :

(P.twistedChainComplexShortComplexConstantIso M).hom.τ₃ = (P.twistedChainComplexConstantIso M).hom

@[simp]

theorem TopPair.twistedChainComplexShortComplexConstantIso_inv_τ₁ {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) :

(P.twistedChainComplexShortComplexConstantIso M).inv.τ₁ = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso snd M).inv (TauCeti.LocalCoefficientSystem.twistedChainComplexCoefficientMap (TauCeti.LocalCoefficientSystem.pullbackConstantIso (TopCat.Hom.hom map) M).inv)

@[simp]

theorem TopPair.twistedChainComplexShortComplexConstantIso_inv_τ₂ {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) :

(P.twistedChainComplexShortComplexConstantIso M).inv.τ₂ = (TauCeti.LocalCoefficientSystem.twistedChainComplexConstantIso fst M).inv

@[simp]

theorem TopPair.twistedChainComplexShortComplexConstantIso_inv_τ₃ {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) :

(P.twistedChainComplexShortComplexConstantIso M).inv.τ₃ = (P.twistedChainComplexConstantIso M).inv

@[simp]

theorem TopPair.twistedHomologyδ_comp_twistedHomologyConstantIso_hom {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) (n m : ℕ) (h : m + 1 = n := by lia) :

CategoryTheory.CategoryStruct.comp (P.twistedHomologyδ ((TauCeti.LocalCoefficientSystem.constantFunctor fst).obj M) n m h) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap (TauCeti.LocalCoefficientSystem.pullbackConstantIso (TopCat.Hom.hom map) M).hom m) (TauCeti.LocalCoefficientSystem.twistedHomologyConstantIso snd M m).hom) = CategoryTheory.CategoryStruct.comp (P.twistedHomologyConstantIso M n).hom (P.singularHomologyδ M n m h)

The constant-system comparison preserves the connecting morphism of relative homology. The boundary convention is the same on the twisted and ordinary sides.

@[simp]

theorem TopPair.twistedHomologyδ_comp_twistedHomologyConstantIso_hom_assoc {R : Type u} [Ring R] (P : TopPair) (M : ModuleCat R) (n m : ℕ) (h : m + 1 = n := by lia) {Z : ModuleCat R} (h✝ : ((AlgebraicTopology.singularHomologyFunctor (ModuleCat R) m).obj M).obj snd ⟶ Z) :

The constant-system comparison preserves the connecting morphism of relative homology. The boundary convention is the same on the twisted and ordinary sides.