Relative singular homology of a space modulo the empty subspace

This file identifies the relative singular chains of (X, ∅) with the ordinary singular chains of X. The quotient map supplies the comparison, naturally in X, and applying homology gives the corresponding natural isomorphism between ordinary and relative singular homology.

This is the quotient-chain comparison for the empty subspace, following the relative singular chain construction in Eilenberg--Steenrod, Foundations of Algebraic Topology, Chapters I--III. The formal infrastructure is Mathlib's relative simplicial chains: the comparison is the quotient natural transformation SSetPair.chainComplexFunctorπ, and its invertibility for a pair whose subcomplex is empty is Mathlib's SSetPair.isIso_chainComplexπ.

For any pair whose subspace is empty, the singular simplicial set of the subspace has no simplices (TopPair.hasDimensionLT_toSSetPair_left_of_isEmpty), so by Mathlib's SSetPair.isIso_chainComplexπ the quotient map TopPair.singularHomologyπ from ambient to relative singular homology is an isomorphism, found by instance resolution.

instance TopPair.isEmpty_incl_obj_snd (X : TopCat) : IsEmpty ↑snd

The subspace of the pair (X, ∅) is empty.

instance TopPair.hasDimensionLT_toSSetPair_left_of_isEmpty (P : TopPair) [IsEmpty ↑snd] : (toSSetPair.obj P).left.HasDimensionLT 0

The singular simplicial set of an empty subspace has no simplices.

theorem TopPair.singularChainComplexFunctor_eq_incl_chainComplexFunctorRight (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : (AlgebraicTopology.singularChainComplexFunctor C).obj R = (incl.comp toSSetPair).comp ((SSetPair.chainComplexFunctorRight C).obj R)

Ordinary singular chains are the ambient chains of the singular pair associated to (X, ∅).

theorem TopPair.incl_comp_singularChainComplexFunctor_eq (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : incl.comp ((singularChainComplexFunctor C).obj R) = (incl.comp toSSetPair).comp ((SSetPair.chainComplexFunctor C).obj R)

Restricting relative singular chains along TopPair.incl agrees with restricting relative simplicial chains along the singular-pair functor.

noncomputable def TopPair.singularChainComplexInclComparison (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : (AlgebraicTopology.singularChainComplexFunctor C).obj R ⟶ incl.comp ((singularChainComplexFunctor C).obj R)

The quotient map from ordinary singular chains to the relative singular chains of (X, ∅), as a natural transformation in X.

Equations

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

@[simp]

theorem TopPair.singularChainComplexInclComparison_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (X : TopCat) : (singularChainComplexInclComparison C R).app X = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp ((incl.obj X).singularChainComplexπ R) (CategoryTheory.eqToHom ⋯))

Each component of the comparison from ordinary to relative singular chains is the quotient map, up to the transports identifying the source and target chain complexes.

noncomputable def TopPair.singularChainComplexInclIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : (AlgebraicTopology.singularChainComplexFunctor C).obj R ≅ incl.comp ((singularChainComplexFunctor C).obj R)

Ordinary singular chains are naturally isomorphic to relative singular chains modulo the empty subspace.

Equations

• TopPair.singularChainComplexInclIso C R = CategoryTheory.NatIso.ofComponents (fun (X : TopCat) => CategoryTheory.asIso ((TopPair.singularChainComplexInclComparison C R).app X)) ⋯

@[simp]

theorem TopPair.singularChainComplexInclIso_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : (singularChainComplexInclIso C R).hom = singularChainComplexInclComparison C R

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

Restricting relative singular homology to pairs (X, ∅) agrees with taking homology after restricting the relative singular chain complex functor.

noncomputable def TopPair.singularHomologyInclIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : (AlgebraicTopology.singularHomologyFunctor C n).obj R ≅ incl.comp (singularHomologyFunctor R n)

Ordinary singular homology is naturally isomorphic to relative singular homology modulo the empty subspace. Its forward map is induced by the quotient map on singular chains.

Equations

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

@[simp]

theorem TopPair.singularHomologyInclIso_hom (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : (singularHomologyInclIso C R n).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (singularChainComplexInclComparison C R) (HomologicalComplex.homologyFunctor C (ComplexShape.down ℕ) n)) (CategoryTheory.eqToHom ⋯)

theorem TopPair.singularHomologyInclIso_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) (X : TopCat) : (singularHomologyInclIso C R n).hom.app X = CategoryTheory.CategoryStruct.comp ((incl.obj X).singularHomologyπ R n) (CategoryTheory.eqToHom ⋯)

The component at X of the comparison from ordinary singular homology to relative singular homology of (X, ∅) is the map induced by the quotient from ambient to relative chains.