Functoriality of relative singular homology with local coefficients

A map of topological pairs f : (X, A) ⟶ (Y, B) and a local coefficient system L on Y induce maps from the relative twisted chains and homology of (X, A) with coefficients in f⁎L to those of (Y, B) with coefficients in L. The construction descends the map on ambient twisted chains through the quotient by the subspace chains.

The coefficient system on A obtained by first pulling L back to X and then restricting to A is canonically isomorphic to the pullback to A of the restriction of L to B. This comparison makes the maps on subspace and ambient chains into a morphism of the short exact sequences of a pair. Consequently the relative map commutes with the connecting morphism in the long exact sequence.

Together with TauCeti.AlgebraicTopology.Singular.Twisted.Basic, this supplies functoriality of twisted singular homology for maps of spaces and maps of pairs.

References

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

noncomputable def TopPair.subspaceSystemPullbackIso {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : P.subspaceSystem ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) ≅ (TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.snd f))).obj (Q.subspaceSystem L)

Restricting a pulled-back local coefficient system to the subspace agrees canonically with pulling the restricted system back along the subspace component of a map of pairs.

Equations

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

noncomputable def TopPair.twistedSubspaceChainComplexMap {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : (P.subspaceSystem ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L)).twistedChainComplex ⟶ (Q.subspaceSystem L).twistedChainComplex

The map on twisted chains of the subspaces induced by a map of pairs. Its source is first identified with the pullback of the target subspace system.

Equations

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

theorem TopPair.twistedChainComplexMap_naturality_pair {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L)) (TauCeti.LocalCoefficientSystem.twistedChainComplexMap (Hom.fst f) L) = CategoryTheory.CategoryStruct.comp (twistedSubspaceChainComplexMap f L) (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L)

The maps induced by a map of pairs on subspace and ambient twisted chains form a commutative square.

theorem TopPair.twistedChainComplexMap_naturality_pair_assoc {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {Z : ChainComplex (ModuleCat R) ℕ} (h : L.twistedChainComplex ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L)) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap (Hom.fst f) L) h) = CategoryTheory.CategoryStruct.comp (twistedSubspaceChainComplexMap f L) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap map L) h)

The maps induced by a map of pairs on subspace and ambient twisted chains form a commutative square.

noncomputable def TopPair.twistedChainComplexMap {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : P.twistedChainComplex ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) ⟶ Q.twistedChainComplex L

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

Equations

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

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexMap {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L)) (twistedChainComplexMap f L) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap (Hom.fst f) L) (Q.twistedChainComplexπ L)

The relative twisted chain map is characterized by compatibility with the quotient maps from the ambient twisted chain complexes.

@[simp]

theorem TopPair.twistedChainComplexπ_comp_twistedChainComplexMap_assoc {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {Z : ChainComplex (ModuleCat R) ℕ} (h : Q.twistedChainComplex L ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.twistedChainComplexπ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f L) h) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedChainComplexMap (Hom.fst f) L) (CategoryTheory.CategoryStruct.comp (Q.twistedChainComplexπ L) h)

The relative twisted chain map is characterized by compatibility with the quotient maps from the ambient twisted chain complexes.

theorem TopPair.twistedChainComplexMap_naturality {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f L) (Q.twistedChainComplexCoefficientMap η) = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η)) (twistedChainComplexMap f K)

Relative maps of pairs commute with a change of coefficients on the target pair.

theorem TopPair.twistedChainComplexMap_naturality_assoc {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) {Z : ChainComplex (ModuleCat R) ℕ} (h : Q.twistedChainComplex K ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f L) (CategoryTheory.CategoryStruct.comp (Q.twistedChainComplexCoefficientMap η) h) = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f K) h)

Relative maps of pairs commute with a change of coefficients on the target pair.

noncomputable def TopPair.fstPullbackIdIso {R : Type u} [Ring R] (P : TopPair) (L : TauCeti.LocalCoefficientSystem R fst) : (TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst (CategoryTheory.CategoryStruct.id P)))).obj L ≅ L

The pullback along the ambient component of the identity map of a pair is canonically isomorphic to the original coefficient system.

Equations

• P.fstPullbackIdIso L = CategoryTheory.eqToIso ⋯ ≪≫ (TauCeti.LocalCoefficientSystem.pullbackIdIso TopPair.fst).app L

@[simp]

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

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

noncomputable def TopPair.fstPullbackCompIso {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) : (TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst (CategoryTheory.CategoryStruct.comp f g)))).obj K ≅ (TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K)

Pullback along the ambient component of a composite of pair maps agrees canonically with iterated pullback along their ambient components.

Equations

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

@[simp]

theorem TopPair.twistedChainComplexMap_comp {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) : twistedChainComplexMap (CategoryTheory.CategoryStruct.comp f g) K = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap (fstPullbackCompIso f g K).hom) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K)) (twistedChainComplexMap g K))

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

theorem TopPair.twistedChainComplexMap_comp_assoc {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) {Z : ChainComplex (ModuleCat R) ℕ} (h : S.twistedChainComplex K ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedChainComplexMap (CategoryTheory.CategoryStruct.comp f g) K) h = CategoryTheory.CategoryStruct.comp (P.twistedChainComplexCoefficientMap (fstPullbackCompIso f g K).hom) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K)) (CategoryTheory.CategoryStruct.comp (twistedChainComplexMap g K) h))

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

noncomputable def TopPair.twistedChainComplexShortComplexMap {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : P.twistedChainComplexShortComplex ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) ⟶ Q.twistedChainComplexShortComplex L

The morphism between the short exact sequences of twisted chains induced by a map of topological pairs.

Equations

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

@[simp]

theorem TopPair.twistedChainComplexShortComplexMap_τ₁ {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : (twistedChainComplexShortComplexMap f L).τ₁ = twistedSubspaceChainComplexMap f L

@[simp]

theorem TopPair.twistedChainComplexShortComplexMap_τ₂ {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : (twistedChainComplexShortComplexMap f L).τ₂ = TauCeti.LocalCoefficientSystem.twistedChainComplexMap (Hom.fst f) L

@[simp]

theorem TopPair.twistedChainComplexShortComplexMap_τ₃ {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) : (twistedChainComplexShortComplexMap f L).τ₃ = twistedChainComplexMap f L

@[reducible, inline]

noncomputable abbrev TopPair.twistedHomologyMap {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : P.twistedHomology ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k ⟶ Q.twistedHomology L k

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

Equations

• TopPair.twistedHomologyMap f L k = HomologicalComplex.homologyMap (TopPair.twistedChainComplexMap f L) k

theorem TopPair.twistedHomologyMap_naturality {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (k : ℕ) : CategoryTheory.CategoryStruct.comp (twistedHomologyMap f L k) (Q.twistedHomologyCoefficientMap η k) = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η) k) (twistedHomologyMap f K k)

The homology maps of pairs commute with a change of coefficients on the target pair.

theorem TopPair.twistedHomologyMap_naturality_assoc {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) {K : TauCeti.LocalCoefficientSystem R fst} (η : L ⟶ K) (k : ℕ) {Z : ModuleCat R} (h : Q.twistedHomology K k ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedHomologyMap f L k) (CategoryTheory.CategoryStruct.comp (Q.twistedHomologyCoefficientMap η k) h) = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).map η) k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap f K k) h)

The homology maps of pairs commute with a change of coefficients on the target pair.

@[simp]

theorem TopPair.twistedHomologyπ_naturality {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyMap (Hom.fst f) L k) (Q.twistedHomologyπ L k) = CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k) (twistedHomologyMap f L k)

The quotient maps from ambient to relative twisted homology are natural in maps of topological pairs.

@[simp]

theorem TopPair.twistedHomologyπ_naturality_assoc {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) {Z : ModuleCat R} (h : Q.twistedHomology L k ⟶ Z) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyMap (Hom.fst f) L k) (CategoryTheory.CategoryStruct.comp (Q.twistedHomologyπ L k) h) = CategoryTheory.CategoryStruct.comp (P.twistedHomologyπ ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap f L k) h)

The quotient maps from ambient to relative twisted homology are natural in maps of topological pairs.

@[simp]

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

The identity law for maps on relative twisted homology.

@[simp]

theorem TopPair.twistedHomologyMap_comp {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : twistedHomologyMap (CategoryTheory.CategoryStruct.comp f g) K k = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap (fstPullbackCompIso f g K).hom k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K) k) (twistedHomologyMap g K k))

The composition law for maps on relative twisted homology.

theorem TopPair.twistedHomologyMap_comp_assoc {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) {S : TopPair} (g : Q ⟶ S) (K : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) {Z : ModuleCat R} (h : S.twistedHomology K k ⟶ Z) : CategoryTheory.CategoryStruct.comp (twistedHomologyMap (CategoryTheory.CategoryStruct.comp f g) K k) h = CategoryTheory.CategoryStruct.comp (P.twistedHomologyCoefficientMap (fstPullbackCompIso f g K).hom k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap f ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst g))).obj K) k) (CategoryTheory.CategoryStruct.comp (twistedHomologyMap g K k) h))

The composition law for maps on relative twisted homology.

theorem TopPair.homologyMap_twistedSubspaceChainComplexMap {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : HomologicalComplex.homologyMap (twistedSubspaceChainComplexMap f L) k = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap (subspaceSystemPullbackIso f L).hom k) (TauCeti.LocalCoefficientSystem.twistedHomologyMap (Hom.snd f) (Q.subspaceSystem L) k)

The homology map induced by the map on subspace chains is the coefficient comparison followed by the map induced by the subspace component.

theorem TopPair.twistedHomologyMap_naturality_pair {R : Type u} [Ring R] {P Q : TopPair} (f : P ⟶ Q) (L : TauCeti.LocalCoefficientSystem R fst) (k : ℕ) : CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyMap map ((TauCeti.LocalCoefficientSystem.pullback (TopCat.Hom.hom (Hom.fst f))).obj L) k) (TauCeti.LocalCoefficientSystem.twistedHomologyMap (Hom.fst f) L k) = CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyCoefficientMap (subspaceSystemPullbackIso f L).hom k) (CategoryTheory.CategoryStruct.comp (TauCeti.LocalCoefficientSystem.twistedHomologyMap (Hom.snd f) (Q.subspaceSystem L) k) (TauCeti.LocalCoefficientSystem.twistedHomologyMap map L k))

The homology maps induced by a map of pairs commute with the inclusions of the subspaces, after the canonical comparison of their pulled-back coefficient systems.

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

The connecting morphism in relative twisted homology is natural in maps of topological pairs.

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

The connecting morphism in relative twisted homology is natural in maps of topological pairs.