Relative singular cohomology and the long exact sequence of a pair

The relative singular cochain complex of a topological pair (X, A) is obtained by applying the contravariant functor Hom(-, M) to its relative singular chain complex C(X, A). In each degree the short exact sequence of chain complexes 0 ⟶ C(A) ⟶ C(X) ⟶ C(X, A) ⟶ 0 splits, since the singular simplices of A form a subset of those of X. Applying Hom(-, M) therefore gives a short exact sequence of cochain complexes

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

whose long exact cohomology sequence is the long exact sequence of the pair

⋯ ⟶ Hⁿ(X, A) ⟶ Hⁿ(X) ⟶ Hⁿ(A) ⟶ Hⁿ⁺¹(X, A) ⟶ ⋯.

A map of pairs (X, A) ⟶ (Y, B) induces maps from the relative cochains and cohomology of (Y, B) to those of (X, A), and the connecting morphism is natural for these maps.

Main declarations

• TopPair.singularCochainComplex, TopPair.singularCohomology, and the maps TopPair.singularCochainComplexMap and TopPair.singularCohomologyMap induced by maps of pairs, with TopPair.singularCohomologyFunctor the functor TopPairᵒᵖ ⥤ ModuleCat k.
• TopPair.shortExact_singularCochainComplexShortComplex: the cochain sequence of a pair is short exact.
• TopPair.singularCohomologyδ: the connecting morphism Hⁿ(A) ⟶ Hᵐ(X, A) for n + 1 = m, with the three exactness statements TopPair.singularCohomology_exact_relative, TopPair.singularCohomology_exact_space and TopPair.singularCohomology_exact_subspace, and its naturality TopPair.singularCohomologyδ_naturality.

References

• A. Hatcher, Algebraic Topology, Section 3.1.
• S. Eilenberg and N. Steenrod, Foundations of Algebraic Topology, Chapters I--III.
• J. Riou and A. Yang, relative homology of simplicial-set pairs in Mathlib.

@[reducible, inline]

noncomputable abbrev TopPair.singularCochainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : CochainComplex (ModuleCat k) ℕ

The relative singular cochain complex of a topological pair: in degree n, the k-module of morphisms from the relative singular n-chains with coefficients in R to M.

Equations

• P.singularCochainComplex R k M = (P.singularChainComplex R).linearYonedaObj k M

@[reducible, inline]

noncomputable abbrev TopPair.singularCochainComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') : P'.singularCochainComplex R k M ⟶ P.singularCochainComplex R k M

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

Equations

• TopPair.singularCochainComplexMap f = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (TopPair.singularChainComplexMap f R).op

theorem TopPair.singularCochainComplexMap_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') : singularCochainComplexMap f = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (SSetPair.chainComplexMap (toSSetPair.map f) R).op

The relative cochain map is the image under Hom(-, M) of the relative singular chain map of the associated simplicial-set pair.

theorem TopPair.singularCochainComplexMap_fst_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') : TopCat.singularCochainComplexMap (Hom.fst f) = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (SSet.chainComplexMap (toSSetPair.map f).right R).op

The cochain map on ambient spaces is the image under Hom(-, M) of the ambient component of the induced simplicial-set-pair map.

@[simp]

theorem TopPair.singularCochainComplexMap_f_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') (n : ℕ) (g : ↑((P'.singularCochainComplex R k M).X n)) : (CategoryTheory.ConcreteCategory.hom ((singularCochainComplexMap f).f n)) g = CategoryTheory.CategoryStruct.comp ((singularChainComplexMap f R).f n) g

The degree-n component of the cochain map induced by f acts by precomposition with the degree-n component of the induced relative singular chain map.

@[simp]

theorem TopPair.singularCochainComplexMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} (P : TopPair) : singularCochainComplexMap (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id (P.singularCochainComplex R k M)

theorem TopPair.singularCochainComplexMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' P'' : TopPair} (f : P ⟶ P') (g : P' ⟶ P'') : singularCochainComplexMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (singularCochainComplexMap g) (singularCochainComplexMap f)

theorem TopPair.singularCochainComplexMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' P'' : TopPair} (f : P ⟶ P') (g : P' ⟶ P'') {Z : CochainComplex (ModuleCat k) ℕ} (h : P.singularCochainComplex R k M ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularCochainComplexMap (CategoryTheory.CategoryStruct.comp f g)) h = CategoryTheory.CategoryStruct.comp (singularCochainComplexMap g) (CategoryTheory.CategoryStruct.comp (singularCochainComplexMap f) h)

@[reducible, inline]

noncomputable abbrev TopPair.singularCohomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : ModuleCat k

The relative singular cohomology of a topological pair in degree n.

Equations

• P.singularCohomology R k M n = HomologicalComplex.homology (P.singularCochainComplex R k M) n

@[reducible, inline]

noncomputable abbrev TopPair.singularCohomologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') (n : ℕ) : P'.singularCohomology R k M n ⟶ P.singularCohomology R k M n

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

Equations

• TopPair.singularCohomologyMap f n = HomologicalComplex.homologyMap (TopPair.singularCochainComplexMap f) n

@[simp]

theorem TopPair.singularCohomologyMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} (P : TopPair) (n : ℕ) : TopPair.singularCohomologyMap (CategoryTheory.CategoryStruct.id P) n = CategoryTheory.CategoryStruct.id (P.singularCohomology R k M n)

theorem TopPair.singularCohomologyMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' P'' : TopPair} (f : P ⟶ P') (g : P' ⟶ P'') (n : ℕ) : TopPair.singularCohomologyMap (CategoryTheory.CategoryStruct.comp f g) n = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap g n) (TopPair.singularCohomologyMap f n)

theorem TopPair.singularCohomologyMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' P'' : TopPair} (f : P ⟶ P') (g : P' ⟶ P'') (n : ℕ) {Z : ModuleCat k} (h : P.singularCohomology R k M n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap (CategoryTheory.CategoryStruct.comp f g) n) h = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap g n) (CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap f n) h)

noncomputable def TopPair.singularCohomologyFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : CategoryTheory.Functor TopPairᵒᵖ (ModuleCat k)

Relative singular cohomology in degree n as a contravariant functor from topological pairs to k-modules.

Equations

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

@[simp]

theorem TopPair.singularCohomologyFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) (P : TopPairᵒᵖ) : (singularCohomologyFunctor R k M n).obj P = (Opposite.unop P).singularCohomology R k M n

@[simp]

theorem TopPair.singularCohomologyFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) {X✝ Y✝ : TopPairᵒᵖ} (f : X✝ ⟶ Y✝) : (singularCohomologyFunctor R k M n).map f = TopPair.singularCohomologyMap f.unop n

@[reducible, inline]

noncomputable abbrev TopPair.singularCochainComplexShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : CategoryTheory.ShortComplex (CochainComplex (ModuleCat k) ℕ)

The cochain sequence C*(X, A) ⟶ C*(X) ⟶ C*(A) of a topological pair (X, A): its maps are induced by the quotient map from the chains of X to the relative chains of (X, A), and by the inclusion of A into X.

Equations

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

theorem TopPair.singularCochainComplexShortComplex_eq_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : P.singularCochainComplexShortComplex R k M = (P.singularChainComplexShortComplex R).op.map (TauCeti.ChainComplex.linearYonedaFunctor k M)

The cochain sequence of a pair is the image under Hom(-, M) of its singular chain sequence.

@[simp]

theorem TopPair.singularCochainComplexShortComplex_f_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : (P.singularCochainComplexShortComplex R k M).f = (TauCeti.ChainComplex.linearYonedaFunctor k M).map (P.singularChainComplexπ R).op

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

@[simp]

theorem TopPair.singularCochainComplexShortComplex_g_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : (P.singularCochainComplexShortComplex R k M).g = TopCat.singularCochainComplexMap map

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

theorem TopPair.shortExact_singularCochainComplexShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : (P.singularCochainComplexShortComplex R k M).ShortExact

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

@[reducible, inline]

noncomputable abbrev TopPair.singularCohomologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : P.singularCohomology R k M n ⟶ TopCat.singularCohomology R k M fst n

The map Hⁿ(X, A) ⟶ Hⁿ(X) from relative to absolute singular cohomology, induced by the quotient map from the singular chains of X to the relative chains of (X, A).

Equations

• P.singularCohomologyπ R k M n = HomologicalComplex.homologyMap (P.singularCochainComplexShortComplex R k M).f n

@[reducible, inline]

noncomputable abbrev TopPair.singularCohomologyδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n m : ℕ) (h : n + 1 = m := by lia) : TopCat.singularCohomology R k M snd n ⟶ P.singularCohomology R k M m

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

Equations

• P.singularCohomologyδ R k M n m h = ⋯.δ n m ⋯

@[simp]

theorem TopPair.singularCohomologyπ_comp_singularCohomologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : CategoryTheory.CategoryStruct.comp (P.singularCohomologyπ R k M n) (TopCat.singularCohomologyMap map n) = 0

@[simp]

theorem TopPair.singularCohomologyπ_comp_singularCohomologyMap_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology R k M snd n ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.singularCohomologyπ R k M n) (CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap map n) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem TopPair.singularCohomologyMap_comp_singularCohomologyδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap map n) (P.singularCohomologyδ R k M n m h) = 0

@[simp]

theorem TopPair.singularCohomologyMap_comp_singularCohomologyδ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : P.singularCohomology R k M m ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap map n) (CategoryTheory.CategoryStruct.comp (P.singularCohomologyδ R k M n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

theorem TopPair.singularCohomology_exact_relative {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := (P.singularCochainComplexShortComplex R k M).X₃.homology n, X₂ := (P.singularCochainComplexShortComplex R k M).X₁.homology m, X₃ := (P.singularCochainComplexShortComplex R k M).X₂.homology m, f := ⋯.δ n m ⋯, g := HomologicalComplex.homologyMap (P.singularCochainComplexShortComplex R k M).f m, zero := ⋯ }.Exact

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

instance TopPair.instMonoModuleCatSingularCohomologyπOfNatNat {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) : CategoryTheory.Mono (P.singularCohomologyπ R k M 0)

The map from relative to absolute zeroth singular cohomology is a monomorphism.

theorem TopPair.singularCohomology_exact_space {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n : ℕ) : { X₁ := P.singularCohomology R k M n, X₂ := TopCat.singularCohomology R k M fst n, X₃ := TopCat.singularCohomology R k M snd n, f := P.singularCohomologyπ R k M n, g := TopCat.singularCohomologyMap map n, zero := ⋯ }.Exact

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

theorem TopPair.singularCohomology_exact_subspace {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (P : TopPair) (R : C) (k : Type u_1) [Ring k] [CategoryTheory.Linear k C] (M : C) (n m : ℕ) (h : n + 1 = m := by lia) : { X₁ := TopCat.singularCohomology R k M fst n, X₂ := TopCat.singularCohomology R k M snd n, X₃ := P.singularCohomology R k M m, f := TopCat.singularCohomologyMap map n, g := P.singularCohomologyδ R k M n m h, zero := ⋯ }.Exact

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

noncomputable def TopPair.singularCochainComplexShortComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') : P'.singularCochainComplexShortComplex R k M ⟶ P.singularCochainComplexShortComplex R k M

The morphism of cochain sequences C*(Y, B) ⟶ C*(Y) ⟶ C*(B) to C*(X, A) ⟶ C*(X) ⟶ C*(A) induced by a map of pairs (X, A) ⟶ (Y, B).

Equations

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

@[simp]

theorem TopPair.singularCochainComplexShortComplexMap_τ₁ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') : (singularCochainComplexShortComplexMap f).τ₁ = singularCochainComplexMap f

@[simp]

theorem TopPair.singularCochainComplexShortComplexMap_τ₂ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') : (singularCochainComplexShortComplexMap f).τ₂ = TopCat.singularCochainComplexMap (Hom.fst f)

@[simp]

theorem TopPair.singularCochainComplexShortComplexMap_τ₃ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') : (singularCochainComplexShortComplexMap f).τ₃ = TopCat.singularCochainComplexMap (Hom.snd f)

theorem TopPair.singularCohomologyπ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') (n : ℕ) : CategoryTheory.CategoryStruct.comp (P'.singularCohomologyπ R k M n) (TopCat.singularCohomologyMap (Hom.fst f) n) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap f n) (P.singularCohomologyπ R k M n)

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

theorem TopPair.singularCohomologyπ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') (n : ℕ) {Z : ModuleCat k} (h : TopCat.singularCohomology R k M fst n ⟶ Z) : CategoryTheory.CategoryStruct.comp (P'.singularCohomologyπ R k M n) (CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (Hom.fst f) n) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap f n) (CategoryTheory.CategoryStruct.comp (P.singularCohomologyπ R k M n) h)

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

theorem TopPair.singularCohomologyδ_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') (n m : ℕ) (h : n + 1 = m := by lia) : CategoryTheory.CategoryStruct.comp (P'.singularCohomologyδ R k M n m h) (TopPair.singularCohomologyMap f m) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (Hom.snd f) n) (P.singularCohomologyδ R k M n m h)

The connecting morphism of the long exact sequence of a topological pair is natural: for a map of pairs f : (X, A) ⟶ (Y, B), following Hⁿ(B) ⟶ Hᵐ(Y, B) by the map induced by f on relative cohomology agrees with following the map induced by f on Hⁿ(B) by Hⁿ(A) ⟶ Hᵐ(X, A).

theorem TopPair.singularCohomologyδ_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] {R : C} {k : Type u_1} [Ring k] [CategoryTheory.Linear k C] {M : C} {P P' : TopPair} (f : P ⟶ P') (n m : ℕ) (h : n + 1 = m := by lia) {Z : ModuleCat k} (h✝ : P.singularCohomology R k M m ⟶ Z) : CategoryTheory.CategoryStruct.comp (P'.singularCohomologyδ R k M n m h) (CategoryTheory.CategoryStruct.comp (TopPair.singularCohomologyMap f m) h✝) = CategoryTheory.CategoryStruct.comp (TopCat.singularCohomologyMap (Hom.snd f) n) (CategoryTheory.CategoryStruct.comp (P.singularCohomologyδ R k M n m h) h✝)

The connecting morphism of the long exact sequence of a topological pair is natural: for a map of pairs f : (X, A) ⟶ (Y, B), following Hⁿ(B) ⟶ Hᵐ(Y, B) by the map induced by f on relative cohomology agrees with following the map induced by f on Hⁿ(B) by Hⁿ(A) ⟶ Hᵐ(X, A).