Singular homology as a homology pretheory

This file packages relative singular homology with coefficients in an object R of an abelian category as a TopPair.HomologyPretheory indexed by ComplexShape.down ℕ: the relative homology functors are TopPair.singularHomologyFunctor R n, the absolute ones are Mathlib's singular homology functors, the two are compared on pairs (X, ∅) by TopPair.singularHomologyInclIso, and the boundary morphisms are the connecting morphisms Hₙ(X, A) ⟶ Hₘ(A) (for m + 1 = n) of the long exact sequence of a pair, which are natural in the pair.

The pretheory satisfies the homotopy axiom HomologyPretheory.IsHomotopyInvariant, because homotopic maps of pairs induce chain-homotopic maps of relative singular chains; the exactness axiom HomologyPretheory.HasPairSequence, by the long exact sequence of a pair; and the dimension axiom HomologyPretheory.HasDimensionAxiom, because the singular homology of a point vanishes in positive degrees. When coproducts are exact in the coefficient category (axiom AB4, as for modules over a ring), it also satisfies the additivity axiom HomologyPretheory.IsAdditive, because singular homology of a disjoint union is the coproduct of the singular homologies of the summands.

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

noncomputable def TopPair.singularHomologyδNatTrans {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n m : ℕ) (h : m + 1 = n := by lia) : singularHomologyFunctor R n ⟶ proj₂.comp ((AlgebraicTopology.singularHomologyFunctor A m).obj R)

The connecting morphism Hₙ(X, A) ⟶ Hₘ(A) of the long exact sequence of a topological pair, for m + 1 = n, as a natural transformation from relative singular homology to the singular homology of the subspace.

Equations

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

@[simp]

theorem TopPair.singularHomologyδNatTrans_app {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n m : ℕ) (h : m + 1 = n) (P : TopPair) : (singularHomologyδNatTrans R n m h).app P = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (P.singularHomologyδ R n m h) (CategoryTheory.eqToHom ⋯))

noncomputable def TopPair.singularHomologyPretheory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : HomologyPretheory A (ComplexShape.down ℕ)

Relative singular homology with coefficients in R as a homology pretheory: relative singular homology of pairs, singular homology of spaces, their comparison on pairs (X, ∅), and the connecting morphisms Hₙ(X, A) ⟶ Hₘ(A) for m + 1 = n.

Equations

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

@[simp]

theorem TopPair.singularHomologyPretheory_iso {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (singularHomologyPretheory R).iso n = singularHomologyInclIso A R n

@[simp]

theorem TopPair.singularHomologyPretheory_Hₚ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (singularHomologyPretheory R).Hₚ n = singularHomologyFunctor R n

@[simp]

theorem TopPair.singularHomologyPretheory_H {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (singularHomologyPretheory R).H n = (AlgebraicTopology.singularHomologyFunctor A n).obj R

@[simp]

theorem TopPair.singularHomologyPretheory_δ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n m : ℕ) (h : m + 1 = n) : (singularHomologyPretheory R).δ n m = singularHomologyδNatTrans R n m h

theorem TopPair.singularHomologyPretheory_hFstToHₚ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) (P : TopPair) : (singularHomologyPretheory R).hFstToHₚ n P = CategoryTheory.CategoryStruct.comp (P.singularHomologyπ R n) (CategoryTheory.eqToHom ⋯)

The map from the singular homology of the ambient space of a pair to the relative singular homology of the pair is the map induced by the quotient from ambient to relative chains.

instance TopPair.instIsHomotopyInvariantNatSingularHomologyPretheory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : (singularHomologyPretheory R).IsHomotopyInvariant

Singular homology satisfies the homotopy axiom: homotopic maps of topological pairs induce the same map on relative singular homology.

instance TopPair.instIsAdditiveNatSingularHomologyPretheoryOfAB4OfSize {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) [CategoryTheory.AB4OfSize.{w, v, u} A] : (singularHomologyPretheory R).IsAdditive

Singular homology satisfies the additivity axiom when coproducts are exact in the coefficient category: the singular homology of a disjoint union is the coproduct of the singular homologies of the summands.

instance TopPair.instHasPairSequenceNatSingularHomologyPretheory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : (singularHomologyPretheory R).HasPairSequence

Singular homology satisfies the exactness axiom: the long exact sequence of every topological pair.

instance TopPair.instHasDimensionAxiomSingularHomologyPretheory {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : (singularHomologyPretheory R).HasDimensionAxiom

Singular homology satisfies the dimension axiom: the singular homology of a point vanishes in positive degrees.