Relative singular chains

This file sends a topological pair to the corresponding pair of singular simplicial sets and defines its relative singular chain complex. The complex is the cokernel of the inclusion of the singular chains of the subspace into those of the ambient space. In an abelian coefficient category this gives the short exact sequence of chain complexes used to construct the connecting morphisms in relative singular homology. A simplex of the singular pair restricted to a subcomplex of the ambient simplicial set comes from the subspace exactly when its image lies in the subspace (TopPair.mem_range_restrict_hom_app_iff).

The construction follows the quotient-chain presentation in Eilenberg--Steenrod, Foundations of Algebraic Topology, Chapters I--III, and is implemented using Mathlib's SSetPair relative-chain functor.

@[simp]

theorem TopPair.Hom.fst_id (P : TopPair) : fst (CategoryTheory.CategoryStruct.id P) = CategoryTheory.CategoryStruct.id TopPair.fst

The ambient component of the identity map of a topological pair is the identity.

@[simp]

theorem TopPair.Hom.fst_comp {P Q S : TopPair} (f : P ⟶ Q) (g : Q ⟶ S) : fst (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (fst f) (fst g)

The ambient component of a composite map of topological pairs is the composite of the ambient components.

instance TopPair.instMonoTopCatMap_tauCeti (P : TopPair) : CategoryTheory.Mono map

The inclusion of the subspace of a topological pair is a monomorphism, since an embedding is injective.

instance TopPair.instMonoSSetMapTopCatToSSetMap_tauCeti (P : TopPair) : CategoryTheory.Mono (TopCat.toSSet.map map)

An embedding of topological spaces induces a monomorphism of singular simplicial sets.

noncomputable def TopPair.toSSetPair : CategoryTheory.Functor TopPair SSetPair

The singular simplicial-set pair associated to a topological pair.

Equations

• TopPair.toSSetPair = CategoryTheory.MorphismProperty.Comma.lift ((CategoryTheory.MorphismProperty.Arrow.forget TopCat.isEmbedding ⊤ ⊤).comp TopCat.toSSet.mapArrow) ⋯ ⋯ ⋯

@[simp]

theorem TopPair.toSSetPair_obj_left (P : TopPair) : (toSSetPair.obj P).left = TopCat.toSSet.obj snd

@[simp]

theorem TopPair.toSSetPair_obj_right (P : TopPair) : (toSSetPair.obj P).right = TopCat.toSSet.obj fst

@[simp]

theorem TopPair.toSSetPair_obj_hom (P : TopPair) : (toSSetPair.obj P).hom = TopCat.toSSet.map map

@[simp]

theorem TopPair.toSSetPair_map_left {P P' : TopPair} (f : P ⟶ P') : (toSSetPair.map f).left = TopCat.toSSet.map (Hom.snd f)

@[simp]

theorem TopPair.toSSetPair_map_right {P P' : TopPair} (f : P ⟶ P') : (toSSetPair.map f).right = TopCat.toSSet.map (Hom.fst f)

theorem TopPair.mem_range_restrict_hom_app_iff (P : TopPair) (S : (toSSetPair.obj P).right.Subcomplex) {n : SimplexCategoryᵒᵖ} (x : ((toSSetPair.obj P).restrict S).right.obj n) : x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (((toSSetPair.obj P).restrict S).hom.app n)) ↔ Set.range ⇑((fst.toSSetObjEquiv n) ↑x) ⊆ Set.range ⇑(CategoryTheory.ConcreteCategory.hom map)

A simplex of the singular pair of P restricted to a subcomplex S comes from the subspace exactly when its image lies in the subspace.

noncomputable def TopPair.singularChainComplexFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] : CategoryTheory.Functor C (CategoryTheory.Functor TopPair (ChainComplex C ℕ))

The relative singular chain complex functor on topological pairs.

Equations

• TopPair.singularChainComplexFunctor C = (SSetPair.chainComplexFunctor C).comp ((CategoryTheory.Functor.whiskeringLeft TopPair SSetPair (ChainComplex C ℕ)).obj TopPair.toSSetPair)

@[reducible, inline]

noncomputable abbrev TopPair.singularChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) : ChainComplex C ℕ

The relative singular chain complex of a topological pair.

Equations

• P.singularChainComplex R = (TopPair.toSSetPair.obj P).chainComplex R

@[simp]

theorem TopPair.singularChainComplexFunctor_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) : ((singularChainComplexFunctor C).obj R).obj P = P.singularChainComplex R

@[simp]

theorem TopPair.singularChainComplexFunctor_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) {R R' : C} (g : R ⟶ R') : ((singularChainComplexFunctor C).map g).app P = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (((SSetPair.chainComplexFunctor C).map g).app (toSSetPair.obj P)) (CategoryTheory.eqToHom ⋯))

@[reducible, inline]

noncomputable abbrev TopPair.singularChainComplexMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : TopPair} (f : P ⟶ P') (R : C) : P.singularChainComplex R ⟶ P'.singularChainComplex R

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

Equations

• TopPair.singularChainComplexMap f R = SSetPair.chainComplexMap (TopPair.toSSetPair.map f) R

@[simp]

theorem TopPair.singularChainComplexFunctor_obj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P P' : TopPair) (f : P ⟶ P') (R : C) : ((singularChainComplexFunctor C).obj R).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (singularChainComplexMap f R) (CategoryTheory.eqToHom ⋯))

@[reducible, inline]

noncomputable abbrev TopPair.singularChainComplexπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) : (toSSetPair.obj P).right.chainComplex R ⟶ P.singularChainComplex R

The quotient map from ambient singular chains to relative singular chains.

Equations

• P.singularChainComplexπ R = (TopPair.toSSetPair.obj P).chainComplexπ R

@[simp]

theorem TopPair.singularChainComplexπ_pair_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P Q : TopPair} (f : P ⟶ Q) (M : C) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map (Hom.fst f)) M) (Q.singularChainComplexπ M) = CategoryTheory.CategoryStruct.comp (P.singularChainComplexπ M) (singularChainComplexMap f M)

The quotient map from ambient to relative singular chains is natural in maps of pairs.

theorem TopPair.singularChainComplexπ_pair_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P Q : TopPair} (f : P ⟶ Q) (M : C) {Z : ChainComplex C ℕ} (h : Q.singularChainComplex M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map (Hom.fst f)) M) (Q.singularChainComplexπ M)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (P.singularChainComplexπ M) (singularChainComplexMap f M)) h

The quotient map from ambient to relative singular chains is natural in maps of pairs.

theorem TopPair.singularChainComplexπ_coefficient_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) {M N : C} (φ : M ⟶ N) : CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor C).map φ).app fst) (P.singularChainComplexπ N) = CategoryTheory.CategoryStruct.comp (P.singularChainComplexπ M) (((SSetPair.chainComplexFunctor C).map φ).app (toSSetPair.obj P))

The quotient map from ambient to relative singular chains is natural in the coefficient object.

theorem TopPair.singularChainComplexπ_coefficient_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) {M N : C} (φ : M ⟶ N) {Z : ChainComplex C ℕ} (h : P.singularChainComplex N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor C).map φ).app fst) (P.singularChainComplexπ N)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (P.singularChainComplexπ M) (((SSetPair.chainComplexFunctor C).map φ).app (toSSetPair.obj P))) h

The quotient map from ambient to relative singular chains is natural in the coefficient object.

@[simp]

theorem TopPair.chainComplexMap_comp_singularChainComplexπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) : CategoryTheory.CategoryStruct.comp (SSet.chainComplexMap (TopCat.toSSet.map map) R) (P.singularChainComplexπ R) = 0

@[reducible, inline]

noncomputable abbrev TopPair.cokernelCoforkSingularChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) : CategoryTheory.Limits.CokernelCofork (SSet.chainComplexMap (toSSetPair.obj P).hom R)

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

Equations

• P.cokernelCoforkSingularChainComplex R = (TopPair.toSSetPair.obj P).cokernelCoforkChainComplex R

noncomputable def TopPair.isColimitCokernelCoforkSingularChainComplex {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) : CategoryTheory.Limits.IsColimit (P.cokernelCoforkSingularChainComplex R)

The relative singular chain complex is the cokernel of the map from the singular chains of the subspace to those of the ambient space.

Equations

• P.isColimitCokernelCoforkSingularChainComplex R = (TopPair.toSSetPair.obj P).isColimitCokernelCoforkChainComplex R

@[reducible, inline]

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

The chain complex sequence of a topological pair: subspace chains, ambient chains, and relative chains.

Equations

• P.singularChainComplexShortComplex R = (TopPair.toSSetPair.obj P).chainComplexShortComplex R

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

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

@[reducible, inline]

noncomputable abbrev TopPair.singularHomology {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : C

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

Equations

• P.singularHomology R n = (TopPair.toSSetPair.obj P).homology R n

@[reducible, inline]

noncomputable abbrev TopPair.singularHomologyMap {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : TopPair} (f : P ⟶ P') (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : P.singularHomology R n ⟶ P'.singularHomology R n

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

Equations

• TopPair.singularHomologyMap f R n = SSetPair.homologyMap (TopPair.toSSetPair.map f) R n

@[simp]

theorem TopPair.singularHomologyMap_id {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : TopPair.singularHomologyMap (CategoryTheory.CategoryStruct.id P) R n = CategoryTheory.CategoryStruct.id (P.singularHomology R n)

Relative singular homology sends the identity map of a pair to the identity.

theorem TopPair.singularHomologyMap_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : TopPair} (f : P ⟶ P') (R : C) [CategoryTheory.CategoryWithHomology C] {P'' : TopPair} (g : P' ⟶ P'') (n : ℕ) : TopPair.singularHomologyMap (CategoryTheory.CategoryStruct.comp f g) R n = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f R n) (TopPair.singularHomologyMap g R n)

Relative singular homology sends a composite of maps of pairs to the composite of the induced maps.

theorem TopPair.singularHomologyMap_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] {P P' : TopPair} (f : P ⟶ P') (R : C) [CategoryTheory.CategoryWithHomology C] {P'' : TopPair} (g : P' ⟶ P'') (n : ℕ) {Z : C} (h : P''.singularHomology R n ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (CategoryTheory.CategoryStruct.comp f g) R n) h = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f R n) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap g R n) h)

Relative singular homology sends a composite of maps of pairs to the composite of the induced maps.

noncomputable def TopPair.singularHomologyFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.Functor TopPair C

Relative singular homology as a functor on topological pairs.

Equations

• TopPair.singularHomologyFunctor R n = TopPair.toSSetPair.comp (SSetPair.homologyFunctor R n)

@[simp]

theorem TopPair.singularHomologyFunctor_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : (singularHomologyFunctor R n).obj P = P.singularHomology R n

@[simp]

theorem TopPair.singularHomologyFunctor_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P P' : TopPair) (f : P ⟶ P') (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : (singularHomologyFunctor R n).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f R n) (CategoryTheory.eqToHom ⋯))

theorem TopPair.singularHomologyFunctor_eq_toSSetPair_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : singularHomologyFunctor R n = toSSetPair.comp (SSetPair.homologyFunctor R n)

Relative singular homology is the relative homology of the singular simplicial-set pair.

theorem TopPair.proj₂_comp_singularHomologyFunctor_obj_eq_toSSetPair_comp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : proj₂.comp ((AlgebraicTopology.singularHomologyFunctor C n).obj R) = toSSetPair.comp ((SSetPair.forget.comp CategoryTheory.Arrow.leftFunc).comp (SSet.homologyFunctor R n))

The singular homology of the subspace of a topological pair is the homology of the source of its singular simplicial-set pair.

theorem TopPair.singularHomologyFunctor_eq_chainComplexFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : singularHomologyFunctor R n = ((singularChainComplexFunctor C).obj R).comp (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n)

Relative singular homology is obtained by applying homology to the relative singular chain complex functor.

@[reducible, inline]

noncomputable abbrev TopPair.singularHomologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : (toSSetPair.obj P).right.homology R n ⟶ P.singularHomology R n

The map from ambient singular homology to relative singular homology.

Equations

• P.singularHomologyπ R n = (TopPair.toSSetPair.obj P).homologyπ R n

@[simp]

theorem TopPair.homologyMap_comp_singularHomologyπ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (P : TopPair) (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.CategoryStruct.comp (SSet.homologyMap (TopCat.toSSet.map map) R n) (P.singularHomologyπ R n) = 0

@[reducible, inline]

noncomputable abbrev TopPair.singularHomologyδ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : P.singularHomology R n ⟶ (toSSetPair.obj P).left.homology R m

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

Equations

• P.singularHomologyδ R n m h = (TopPair.toSSetPair.obj P).homologyδ R n m h

@[simp]

theorem TopPair.singularHomologyδ_comp {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.singularHomologyδ R n m h) (SSet.homologyMap (TopCat.toSSet.map map) R m) = 0

@[simp]

theorem TopPair.singularHomologyπ_comp_singularHomologyδ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.singularHomologyπ R n) (P.singularHomologyδ R n m h) = 0

theorem TopPair.singularHomology_exact_subspace {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := P.singularHomology R n, X₂ := (toSSetPair.obj P).left.homology R m, X₃ := (TopCat.toSSet.obj fst).homology R m, f := P.singularHomologyδ R n m h, g := SSet.homologyMap (TopCat.toSSet.map map) R m, zero := ⋯ }.Exact

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

theorem TopPair.singularHomology_exact_space {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (n : ℕ) : { X₁ := (TopCat.toSSet.obj snd).homology R n, X₂ := (TopCat.toSSet.obj fst).homology R n, X₃ := P.singularHomology R n, f := SSet.homologyMap (TopCat.toSSet.map map) R n, g := P.singularHomologyπ R n, zero := ⋯ }.Exact

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

theorem TopPair.singularHomology_exact_relative {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : { X₁ := (toSSetPair.obj P).right.homology R n, X₂ := P.singularHomology R n, X₃ := (toSSetPair.obj P).left.homology R m, f := P.singularHomologyπ R n, g := P.singularHomologyδ R n m h, zero := ⋯ }.Exact

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

theorem TopPair.singularHomologyδ_naturality {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {P P' : TopPair} (f : P ⟶ P') (n m : ℕ) (h : m + 1 = n := by lia) : CategoryTheory.CategoryStruct.comp (P.singularHomologyδ R n m h) (SSet.homologyMap (TopCat.toSSet.map (Hom.snd f)) R m) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f R n) (P'.singularHomologyδ R 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) ⟶ (X', A'), following Hₙ(X, A) ⟶ Hₘ(A) by the map induced by f on Hₘ(A) agrees with following the map induced by f on Hₙ(X, A) by Hₙ(X', A') ⟶ Hₘ(A').

theorem TopPair.singularHomologyδ_naturality_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {P P' : TopPair} (f : P ⟶ P') (n m : ℕ) (h : m + 1 = n := by lia) {Z : A} (h✝ : (TopCat.toSSet.obj snd).homology R m ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (P.singularHomologyδ R n m h) (SSet.homologyMap (TopCat.toSSet.map (Hom.snd f)) R m)) h✝ = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f R n) (P'.singularHomologyδ R 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) ⟶ (X', A'), following Hₙ(X, A) ⟶ Hₘ(A) by the map induced by f on Hₘ(A) agrees with following the map induced by f on Hₙ(X, A) by Hₙ(X', A') ⟶ Hₘ(A').

instance TopPair.instEpiSingularHomologyπOfNatNat {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) : CategoryTheory.Epi (P.singularHomologyπ R 0)

The map from ambient zeroth homology to relative zeroth homology is an epimorphism.