The long exact sequence of a triple in relative singular homology

For a triple B ⊆ A ⊆ X of topological spaces the relative singular chain complexes of the three pairs it determines form a short exact sequence

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

because each of them is the quotient of the singular chains of the ambient space by those of the subspace. The associated long homology sequence is the long exact sequence of the triple

⋯ ⟶ Hₙ(A, B) ⟶ Hₙ(X, B) ⟶ Hₙ(X, A) ⟶ Hₙ₋₁(A, B) ⟶ ⋯.

Each of the three pairs is a functor of the triple, so the three relative homology groups are functorial as well, and the connecting morphism is natural for morphisms of triples.

The source is Eilenberg--Steenrod, Foundations of Algebraic Topology, Chapters I--III.

theorem TauCeti.TopTriple.singularChainComplexπ_comp_innerToTotal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (T : TopTriple) (R : C) : CategoryTheory.CategoryStruct.comp ((innerPair.obj T).singularChainComplexπ R) (TopPair.singularChainComplexMap (innerToTotal.app T) R) = CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map T.outerMap) R) ((totalPair.obj T).singularChainComplexπ R)

theorem TauCeti.TopTriple.singularChainComplexπ_comp_innerToTotal_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (T : TopTriple) (R : C) {Z : ChainComplex C ℕ} (h : TopPair.singularChainComplex { left := T.thd, right := T.fst, hom := T.totalMap, prop := ⋯ } R ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularChainComplexπ { left := T.thd, right := T.snd, hom := T.innerMap, prop := ⋯ } R) (CategoryTheory.CategoryStruct.comp (TopPair.singularChainComplexMap (innerToTotal.app T) R) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map T.outerMap) R) (TopPair.singularChainComplexπ { left := T.thd, right := T.fst, hom := T.totalMap, prop := ⋯ } R)) h

theorem TauCeti.TopTriple.singularChainComplexπ_comp_totalToOuter {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (T : TopTriple) (R : C) : CategoryTheory.CategoryStruct.comp ((totalPair.obj T).singularChainComplexπ R) (TopPair.singularChainComplexMap (totalToOuter.app T) R) = (outerPair.obj T).singularChainComplexπ R

theorem TauCeti.TopTriple.singularChainComplexπ_comp_totalToOuter_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (T : TopTriple) (R : C) {Z : ChainComplex C ℕ} (h : TopPair.singularChainComplex { left := T.snd, right := T.fst, hom := T.outerMap, prop := ⋯ } R ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularChainComplexπ { left := T.thd, right := T.fst, hom := T.totalMap, prop := ⋯ } R) (CategoryTheory.CategoryStruct.comp (TopPair.singularChainComplexMap (totalToOuter.app T) R) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularChainComplexπ { left := T.snd, right := T.fst, hom := T.outerMap, prop := ⋯ } R) h

theorem TauCeti.TopTriple.singularChainComplexMap_innerToTotal_comp_totalToOuter {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (T : TopTriple) (R : C) : CategoryTheory.CategoryStruct.comp (TopPair.singularChainComplexMap (innerToTotal.app T) R) (TopPair.singularChainComplexMap (totalToOuter.app T) R) = 0

@[reducible, inline]

noncomputable abbrev TauCeti.TopTriple.singularChainComplexShortComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (T : TopTriple) (R : C) : CategoryTheory.ShortComplex (ChainComplex C ℕ)

The chain complex sequence of a triple (X, A, B): the relative singular chains of (A, B), of (X, B) and of (X, A).

Equations

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

theorem TauCeti.TopTriple.shortExact_singularChainComplexShortComplex {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) : (T.singularChainComplexShortComplex R).ShortExact

The relative singular chain sequence of a triple is short exact.

noncomputable def TauCeti.TopTriple.singularHomologyδ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : (outerPair.obj T).singularHomology R n ⟶ (innerPair.obj T).singularHomology R m

The connecting morphism Hₙ(X, A) ⟶ Hₘ(A, B) in the long exact sequence of a triple, for m + 1 = n.

Equations

• T.singularHomologyδ R n m h = ⋯.δ n m ⋯

@[simp]

theorem TauCeti.TopTriple.singularHomologyδ_comp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (T.singularHomologyδ R n m h) (TopPair.singularHomologyMap (innerToTotal.app T) R m) = 0

@[simp]

theorem TauCeti.TopTriple.singularHomologyδ_comp_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : TopPair.singularHomology { left := T.thd, right := T.fst, hom := T.totalMap, prop := ⋯ } R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.singularHomologyδ R n m h) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (innerToTotal.app T) R m) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TauCeti.TopTriple.comp_singularHomologyδ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (totalToOuter.app T) R n) (T.singularHomologyδ R n m h) = 0

@[simp]

theorem TauCeti.TopTriple.comp_singularHomologyδ_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : TopPair.singularHomology { left := T.thd, right := T.snd, hom := T.innerMap, prop := ⋯ } R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (totalToOuter.app T) R n) (CategoryTheory.CategoryStruct.comp (T.singularHomologyδ R n m h) h✝) = CategoryTheory.CategoryStruct.comp 0 h✝

@[simp]

theorem TauCeti.TopTriple.singularHomologyMap_innerToTotal_comp_totalToOuter {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (innerToTotal.app T) R n) (TopPair.singularHomologyMap (totalToOuter.app T) R n) = 0

@[simp]

theorem TauCeti.TopTriple.singularHomologyMap_innerToTotal_comp_totalToOuter_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n : ℕ) {Z : A} (h : TopPair.singularHomology { left := T.snd, right := T.fst, hom := T.outerMap, prop := ⋯ } R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (innerToTotal.app T) R n) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (totalToOuter.app T) R n) h) = CategoryTheory.CategoryStruct.comp 0 h

theorem TauCeti.TopTriple.singularHomology_exact_inner {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (outerPair.obj T).singularHomology R n, X₂ := (innerPair.obj T).singularHomology R m, X₃ := (totalPair.obj T).singularHomology R m, f := T.singularHomologyδ R n m h, g := TopPair.singularHomologyMap (innerToTotal.app T) R m, zero := ⋯ }.Exact

Exactness at Hₘ(A, B) in the long exact sequence of a triple.

theorem TauCeti.TopTriple.singularHomology_exact_total {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n : ℕ) : { X₁ := (innerPair.obj T).singularHomology R n, X₂ := (totalPair.obj T).singularHomology R n, X₃ := (outerPair.obj T).singularHomology R n, f := TopPair.singularHomologyMap (innerToTotal.app T) R n, g := TopPair.singularHomologyMap (totalToOuter.app T) R n, zero := ⋯ }.Exact

Exactness at Hₙ(X, B) in the long exact sequence of a triple.

theorem TauCeti.TopTriple.singularHomology_exact_outer {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (totalPair.obj T).singularHomology R n, X₂ := (outerPair.obj T).singularHomology R n, X₃ := (innerPair.obj T).singularHomology R m, f := TopPair.singularHomologyMap (totalToOuter.app T) R n, g := T.singularHomologyδ R n m h, zero := ⋯ }.Exact

Exactness at Hₙ(X, A) in the long exact sequence of a triple.

theorem TauCeti.TopTriple.singularHomologyδ_eq_comp_singularHomologyπ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : T.singularHomologyδ R n m h = CategoryTheory.CategoryStruct.comp ((outerPair.obj T).singularHomologyδ R n m h) ((innerPair.obj T).singularHomologyπ R m)

The connecting morphism of a triple (X, A, B) is the connecting morphism of the pair (X, A) followed by the map Hₘ(A) ⟶ Hₘ(A, B). This factorization is what makes two consecutive connecting morphisms of a filtration compose to zero.

theorem TauCeti.TopTriple.singularHomologyδ_eq_comp_singularHomologyπ_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : TopPair.singularHomology { left := T.thd, right := T.snd, hom := T.innerMap, prop := ⋯ } R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.singularHomologyδ R n m h) h✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyδ { left := T.snd, right := T.fst, hom := T.outerMap, prop := ⋯ } R n m h) (TopPair.singularHomologyπ { left := T.thd, right := T.snd, hom := T.innerMap, prop := ⋯ } R m)) h✝

The connecting morphism of a triple (X, A, B) is the connecting morphism of the pair (X, A) followed by the map Hₘ(A) ⟶ Hₘ(A, B). This factorization is what makes two consecutive connecting morphisms of a filtration compose to zero.

theorem TauCeti.TopTriple.singularHomologyδ_naturality {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {T T' : TopTriple} (φ : T ⟶ T') (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (T.singularHomologyδ R n m h) (TopPair.singularHomologyMap (innerPair.map φ) R m) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (outerPair.map φ) R n) (T'.singularHomologyδ R n m h)

The connecting morphism of the long exact sequence of a triple is natural: for a morphism of triples φ : (X, A, B) ⟶ (X', A', B'), following Hₙ(X, A) ⟶ Hₘ(A, B) by the map induced by φ on Hₘ(A, B) agrees with following the map induced by φ on Hₙ(X, A) by Hₙ(X', A') ⟶ Hₘ(A', B').

theorem TauCeti.TopTriple.singularHomologyδ_naturality_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] {T T' : TopTriple} (φ : T ⟶ T') (R : A) (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : TopPair.singularHomology { left := T'.thd, right := T'.snd, hom := T'.innerMap, prop := ⋯ } R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (T.singularHomologyδ R n m h) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofHom (Hom.snd φ) (Hom.thd φ) ⋯) R m) h✝) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (TopPair.ofHom (Hom.fst φ) (Hom.snd φ) ⋯) R n) (CategoryTheory.CategoryStruct.comp (T'.singularHomologyδ R n m h) h✝)

The connecting morphism of the long exact sequence of a triple is natural: for a morphism of triples φ : (X, A, B) ⟶ (X', A', B'), following Hₙ(X, A) ⟶ Hₘ(A, B) by the map induced by φ on Hₘ(A, B) agrees with following the map induced by φ on Hₙ(X, A) by Hₙ(X', A') ⟶ Hₘ(A', B').

instance TauCeti.TopTriple.instEpiSingularHomologyMapAppTopPairTotalToOuterOfNatNat {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (T : TopTriple) (R : A) : CategoryTheory.Epi (TopPair.singularHomologyMap (totalToOuter.app T) R 0)

The map H₀(X, B) ⟶ H₀(X, A) at the end of the long exact sequence of a triple is an epimorphism.