The relative homology of a cylinder modulo its ends

For a topological space X, the cylinder pair (X × I, X × ∂I), where ∂I = {0, 1}, has relative singular homology Hₙ₊₁(X × I, X × ∂I) ≅ Hₙ(X), naturally in X, and H₀(X × I, X × ∂I) = 0. Coefficients are an object of an abelian category with coproducts.

The isomorphism comes from the triple (X × I, X × ∂I, X × {0}). The bottom end X × {0} is a strong deformation retract of the cylinder, so the relative homology of (X × I, X × {0}) vanishes and the connecting morphism Hₙ₊₁(X × I, X × ∂I) ⟶ Hₙ(X × ∂I, X × {0}) of the triple is an isomorphism. Excising the bottom end, the top end x ↦ (x, 1) induces an isomorphism Hₙ(X) ⟶ Hₙ(X × ∂I, X × {0}).

The isomorphism is characterized by the connecting morphism of the pair: under Hₙ₊₁(X × I, X × ∂I) ≅ Hₙ(X), the connecting morphism Hₙ₊₁(X × I, X × ∂I) ⟶ Hₙ(X × ∂I) is the difference ι₁ - ι₀ of the maps induced by the two ends (TauCeti.singularHomologyδ_cylinderBoundaryPair). This is the form in which the computation enters the homology of spaces obtained by gluing the two ends of a cylinder, such as mapping tori: after the gluing, ι₁ - ι₀ becomes f_* - id for the gluing map f.

Main declarations

• TauCeti.cylinderBoundaryPair X: the pair (X × I, X × ∂I), with the inclusions TauCeti.cylinderBoundaryι₀ and TauCeti.cylinderBoundaryι₁ of the two ends and the maps of pairs TauCeti.cylinderBoundaryPairMap induced by maps of spaces.
• TauCeti.singularHomologyCylinderBoundaryPairIso: Hₙ₊₁(X × I, X × ∂I) ≅ Hₙ(X), natural in X (TauCeti.singularHomologyCylinderBoundaryPairIso_hom_naturality).
• TauCeti.singularHomologyδ_cylinderBoundaryPair: the connecting morphism of the pair is the difference of the maps induced by the two ends.
• TauCeti.isZero_singularHomology_cylinderBoundaryPair_zero: H₀(X × I, X × ∂I) = 0.

References

• A. Hatcher, Algebraic Topology, Section 2.1: the long exact sequence of a triple and excision (Theorem 2.20).

def TauCeti.cylinderBoundary (X : TopCat) : Set (↑X × ↑unitInterval)

The ends X × ∂I = X × {0, 1} of the cylinder X × I.

@[simp]

theorem TauCeti.mem_cylinderBoundary (X : TopCat) {p : ↑X × ↑unitInterval} : p ∈ cylinderBoundary X ↔ p.2 = 0 ∨ p.2 = 1

@[reducible, inline]

abbrev TauCeti.cylinderBoundaryPair (X : TopCat) : TopPair

The cylinder pair (X × I, X × ∂I).

def TauCeti.cylinderBoundaryι₀ (X : TopCat) : X ⟶ TopPair.snd

The inclusion x ↦ (x, 0) of X as the bottom end of the cylinder.

def TauCeti.cylinderBoundaryι₁ (X : TopCat) : X ⟶ TopPair.snd

The inclusion x ↦ (x, 1) of X as the top end of the cylinder.

@[simp]

theorem TauCeti.cylinderBoundaryι₀_apply (X : TopCat) (x : ↑X) : ↑((CategoryTheory.ConcreteCategory.hom (cylinderBoundaryι₀ X)) x) = (x, 0)

@[simp]

theorem TauCeti.cylinderBoundaryι₁_apply (X : TopCat) (x : ↑X) : ↑((CategoryTheory.ConcreteCategory.hom (cylinderBoundaryι₁ X)) x) = (x, 1)

theorem TauCeti.isEmbedding_cylinderBoundaryι₀ (X : TopCat) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (cylinderBoundaryι₀ X))

theorem TauCeti.isEmbedding_cylinderBoundaryι₁ (X : TopCat) : Topology.IsEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (cylinderBoundaryι₁ X))

def TauCeti.cylinderBoundaryPairMap {X Y : TopCat} (g : X ⟶ Y) : cylinderBoundaryPair X ⟶ cylinderBoundaryPair Y

The map of cylinder pairs (X × I, X × ∂I) ⟶ (Y × I, Y × ∂I) induced by g : X ⟶ Y.

@[simp]

theorem TauCeti.cylinderBoundaryPairMap_fst_apply {X Y : TopCat} (g : X ⟶ Y) (p : ↑X × ↑unitInterval) : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (cylinderBoundaryPairMap g))) p = ((CategoryTheory.ConcreteCategory.hom g) p.1, p.2)

@[simp]

theorem TauCeti.cylinderBoundaryPairMap_snd_apply {X Y : TopCat} (g : X ⟶ Y) (p : ↑TopPair.snd) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (cylinderBoundaryPairMap g))) p) = ((CategoryTheory.ConcreteCategory.hom g) (↑p).1, (↑p).2)

@[simp]

theorem TauCeti.cylinderBoundaryPairMap_id (X : TopCat) : cylinderBoundaryPairMap (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (cylinderBoundaryPair X)

theorem TauCeti.cylinderBoundaryPairMap_comp {X Y Z : TopCat} (g : X ⟶ Y) (g' : Y ⟶ Z) : cylinderBoundaryPairMap (CategoryTheory.CategoryStruct.comp g g') = CategoryTheory.CategoryStruct.comp (cylinderBoundaryPairMap g) (cylinderBoundaryPairMap g')

theorem TauCeti.cylinderBoundaryPairMap_comp_assoc {X Y Z : TopCat} (g : X ⟶ Y) (g' : Y ⟶ Z) {Z✝ : TopPair} (h : cylinderBoundaryPair Z ⟶ Z✝) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryPairMap (CategoryTheory.CategoryStruct.comp g g')) h = CategoryTheory.CategoryStruct.comp (cylinderBoundaryPairMap g) (CategoryTheory.CategoryStruct.comp (cylinderBoundaryPairMap g') h)

@[simp]

theorem TauCeti.cylinderBoundaryι₀_comp_cylinderBoundaryPairMap {X Y : TopCat} (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₀ X) (TopPair.Hom.snd (cylinderBoundaryPairMap g)) = CategoryTheory.CategoryStruct.comp g (cylinderBoundaryι₀ Y)

@[simp]

theorem TauCeti.cylinderBoundaryι₀_comp_cylinderBoundaryPairMap_assoc {X Y : TopCat} (g : X ⟶ Y) {Z : TopCat} (h : TopPair.snd ⟶ Z) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₀ X) (CategoryTheory.CategoryStruct.comp (TopPair.Hom.snd (cylinderBoundaryPairMap g)) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₀ Y) h)

@[simp]

theorem TauCeti.cylinderBoundaryι₁_comp_cylinderBoundaryPairMap {X Y : TopCat} (g : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₁ X) (TopPair.Hom.snd (cylinderBoundaryPairMap g)) = CategoryTheory.CategoryStruct.comp g (cylinderBoundaryι₁ Y)

@[simp]

theorem TauCeti.cylinderBoundaryι₁_comp_cylinderBoundaryPairMap_assoc {X Y : TopCat} (g : X ⟶ Y) {Z : TopCat} (h : TopPair.snd ⟶ Z) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₁ X) (CategoryTheory.CategoryStruct.comp (TopPair.Hom.snd (cylinderBoundaryPairMap g)) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₁ Y) h)

theorem TauCeti.isZero_singularHomology_cylinderBoundaryPair_zero (X : TopCat) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : CategoryTheory.Limits.IsZero ((cylinderBoundaryPair X).singularHomology R 0)

The relative homology H₀(X × I, X × ∂I) vanishes: every point of the cylinder is joined to its ends by a path.

noncomputable def TauCeti.singularHomologyCylinderBoundaryPairIso (X : TopCat) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (cylinderBoundaryPair X).singularHomology R (n + 1) ≅ ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj X

The homology of a cylinder modulo its ends: Hₙ₊₁(X × I, X × ∂I) ≅ Hₙ(X). It is the connecting morphism of the triple (X × I, X × ∂I, X × {0}) followed by the inverse of the map Hₙ(X) ⟶ Hₙ(X × ∂I, X × {0}) induced by the top end.

theorem TauCeti.singularHomologyδ_cylinderBoundaryPair (X : TopCat) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (cylinderBoundaryPair X).singularHomologyδ R (n + 1) n ⋯ = CategoryTheory.CategoryStruct.comp (singularHomologyCylinderBoundaryPairIso X R n).hom (((AlgebraicTopology.singularHomologyFunctor A n).obj R).map (cylinderBoundaryι₁ X) - ((AlgebraicTopology.singularHomologyFunctor A n).obj R).map (cylinderBoundaryι₀ X))

The connecting morphism of the cylinder pair. Under Hₙ₊₁(X × I, X × ∂I) ≅ Hₙ(X), the connecting morphism to Hₙ(X × ∂I) is the difference of the maps induced by the top and bottom ends.

theorem TauCeti.singularHomologyCylinderBoundaryPairIso_hom_naturality (X : TopCat) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {Y : TopCat} (g : X ⟶ Y) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (cylinderBoundaryPairMap g) R (n + 1)) (singularHomologyCylinderBoundaryPairIso Y R n).hom = CategoryTheory.CategoryStruct.comp (singularHomologyCylinderBoundaryPairIso X R n).hom (((AlgebraicTopology.singularHomologyFunctor A n).obj R).map g)

Naturality of Hₙ₊₁(X × I, X × ∂I) ≅ Hₙ(X) in maps g : X ⟶ Y.

theorem TauCeti.singularHomologyCylinderBoundaryPairIso_hom_naturality_assoc (X : TopCat) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) {Y : TopCat} (g : X ⟶ Y) (n : ℕ) {Z : A} (h : ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (cylinderBoundaryPairMap g) R (n + 1)) (CategoryTheory.CategoryStruct.comp (singularHomologyCylinderBoundaryPairIso Y R n).hom h) = CategoryTheory.CategoryStruct.comp (singularHomologyCylinderBoundaryPairIso X R n).hom (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularHomologyFunctor A n).obj R).map g) h)

Naturality of Hₙ₊₁(X × I, X × ∂I) ≅ Hₙ(X) in maps g : X ⟶ Y.