Reduced connecting morphism for relative singular homology

For every topological pair (X, A), the connecting morphism Hₖ₊₁(X, A) ⟶ Hₖ(A) of the long exact sequence lands in the reduced homology of A. In degree zero, this follows because the connecting morphism is killed by the map to H₀(X), which commutes with augmentation. The resulting morphism TopPair.reducedSingularHomologyδ is natural in maps of pairs and is an isomorphism when the reduced homology of X vanishes in degrees k and k + 1.

Coefficients are an object of an abelian category with coproducts.

The construction follows Hatcher, Algebraic Topology, Section 2.1, on the reduced long exact sequence of a pair.

noncomputable def TopPair.reducedSingularHomologyδ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (k : ℕ) : P.singularHomology R (k + 1) ⟶ (TauCeti.reducedSingularHomologyFunctor R k).obj snd

The connecting morphism Hₖ₊₁(X, A) ⟶ H~ₖ(A) of a topological pair (X, A), into the reduced singular homology of the subspace. It lifts the connecting morphism of the long exact sequence of the pair through the inclusion of reduced into ordinary homology (TopPair.reducedSingularHomologyδ_comp_ι).

Equations

• P.reducedSingularHomologyδ R 0 = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.lift (TopPair.snd.singularHomology₀ε R) (TopPair.δ✝ P R 0) ⋯) (CategoryTheory.eqToHom ⋯)
• P.reducedSingularHomologyδ R k.succ = CategoryTheory.CategoryStruct.comp (TopPair.δ✝ P R (k + 1)) ((TauCeti.reducedSingularHomologySuccIso R k).inv.app TopPair.snd)

@[simp]

theorem TopPair.reducedSingularHomologyδ_comp_ι {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (k : ℕ) : CategoryTheory.CategoryStruct.comp (P.reducedSingularHomologyδ R k) ((TauCeti.reducedSingularHomologyι R k).app snd) = P.singularHomologyδ R (k + 1) k ⋯

The reduced connecting morphism followed by the inclusion of reduced into ordinary homology is the connecting morphism of the long exact sequence of the pair.

@[simp]

theorem TopPair.reducedSingularHomologyδ_comp_ι_assoc {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) (k : ℕ) {Z : A} (h : ((AlgebraicTopology.singularHomologyFunctor A k).obj R).obj snd ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.reducedSingularHomologyδ R k) (CategoryTheory.CategoryStruct.comp ((TauCeti.reducedSingularHomologyι R k).app snd) h) = CategoryTheory.CategoryStruct.comp (P.singularHomologyδ R (k + 1) k ⋯) h

The reduced connecting morphism followed by the inclusion of reduced into ordinary homology is the connecting morphism of the long exact sequence of the pair.

theorem TopPair.reducedSingularHomologyδ_naturality {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {P P' : TopPair} (f : P ⟶ P') (k : ℕ) : CategoryTheory.CategoryStruct.comp (P.reducedSingularHomologyδ R k) ((TauCeti.reducedSingularHomologyFunctor R k).map (Hom.snd f)) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f R (k + 1)) (P'.reducedSingularHomologyδ R k)

Naturality of the reduced connecting morphism under maps of topological pairs.

theorem TopPair.reducedSingularHomologyδ_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') (k : ℕ) {Z : A} (h : (TauCeti.reducedSingularHomologyFunctor R k).obj snd ⟶ Z) : CategoryTheory.CategoryStruct.comp (P.reducedSingularHomologyδ R k) (CategoryTheory.CategoryStruct.comp ((TauCeti.reducedSingularHomologyFunctor R k).map (Hom.snd f)) h) = CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap f R (k + 1)) (CategoryTheory.CategoryStruct.comp (P'.reducedSingularHomologyδ R k) h)

Naturality of the reduced connecting morphism under maps of topological pairs.

theorem TopPair.isIso_reducedSingularHomologyδ {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (P : TopPair) (R : A) {k : ℕ} (h₁ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R (k + 1)).obj fst)) (h₀ : CategoryTheory.Limits.IsZero ((TauCeti.reducedSingularHomologyFunctor R k).obj fst)) : CategoryTheory.IsIso (P.reducedSingularHomologyδ R k)

The reduced connecting morphism is an isomorphism when the ambient space is acyclic in the adjacent degrees: if the reduced homology of X vanishes in degrees k and k + 1, then Hₖ₊₁(X, A) ⟶ H~ₖ(A) is an isomorphism.