The relative homology of a mapping torus modulo a fibre

Let T be the mapping torus of a homeomorphism φ : F ≃ₜ F, and regard F as the fibre of T over 0 in the circle (TauCeti.MappingTorus.fiber). The cylinder F × I maps onto T by (x, t) ↦ [φ x, t]; this is the monodromy homotopy TauCeti.MappingTorus.monodromyHomotopy read as a map out of the cylinder. It sends the ends F × ∂I into the fibre, so it is a map of pairs (F × I, F × ∂I) ⟶ (T, F) (TauCeti.MappingTorus.cylinderPairMap). On the bottom end it is the fibre inclusion after φ, and on the top end it is the fibre inclusion.

This map induces isomorphisms on relative singular homology in every degree (TauCeti.MappingTorus.isIso_singularHomologyMap_cylinderPairMap), with coefficients in an object of an abelian category with coproducts. Combined with the homology of the cylinder modulo its ends, this gives Hₙ₊₁(T, F) ≅ Hₙ(F) (TauCeti.MappingTorus.singularHomologyFiberPairIso) and H₀(T, F) = 0. Under this isomorphism the connecting morphism Hₙ₊₁(T, F) ⟶ Hₙ(F) of the pair is id - φ_* followed by the map induced by the fibre inclusion (TauCeti.MappingTorus.singularHomologyδ_fiberPair). This is the form in which the endomorphism id - φ_* of the Wang sequence of the mapping torus enters the long exact sequence of the pair (T, F).

The proof is the argument showing that the quotient map of a good pair induces isomorphisms on relative homology. Both pairs are first thickened. In T, the heights within 1/3 of an integer form an open neighbourhood of the fibre; in the cylinder, the heights within 1/3 of 0 or 1 form an open neighbourhood of the ends. Collapsing these heights onto the nearest integer is a deformation of each space, so thickening does not change relative homology (TopPair.isIso_singularHomologyMap_ofSubsetMap_id_of_homotopy). The open cylinder F × (0, 1) embeds openly in T, with image the complement of the fibre (TauCeti.MappingTorus.isOpenEmbedding_mk_Ioo and TauCeti.MappingTorus.range_mk_Ioo). So excision identifies both thickened pairs with the same pair on the open cylinder (TopPair.isIso_singularHomologyMap_excisionMap and TopPair.isIso_singularHomologyMap_of_open_cover).

Main declarations

• TauCeti.MappingTorus.fiberPair φ: the pair (T, F).
• TauCeti.MappingTorus.fiberPairIncl φ: the fibre inclusion F ⟶ fiber φ, an isomorphism (TauCeti.MappingTorus.isIso_fiberPairIncl).
• TauCeti.MappingTorus.cylinderPairMap φ: the map of pairs (F × I, F × ∂I) ⟶ (T, F).
• TauCeti.MappingTorus.isIso_singularHomologyMap_cylinderPairMap: it induces isomorphisms on relative singular homology.
• TauCeti.MappingTorus.singularHomologyFiberPairIso: Hₙ₊₁(T, F) ≅ Hₙ(F).
• TauCeti.MappingTorus.singularHomologyδ_fiberPair: the connecting morphism of (T, F) is id - φ_* followed by the fibre inclusion.

References

• A. Hatcher, Algebraic Topology, Section 2.1, Proposition 2.22 and its proof (good pairs), and Section 2.2 (the homology of a mapping torus).

@[reducible, inline]

abbrev TauCeti.MappingTorus.fiberPair {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : TopPair

The pair (T, F) formed by the mapping torus T of φ and its fibre over 0.

def TauCeti.MappingTorus.fiberPairIncl {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : ↧F ⟶ TopPair.snd

The fibre inclusion MappingTorus.incl, as a map into the subspace of fiberPair φ.

@[simp]

theorem TauCeti.MappingTorus.fiberPairIncl_apply {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) (x : F) : ↑((CategoryTheory.ConcreteCategory.hom (fiberPairIncl φ)) x) = (incl φ) x

@[simp]

theorem TauCeti.MappingTorus.fiberPairIncl_comp_map {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : CategoryTheory.CategoryStruct.comp (fiberPairIncl φ) (TopCat.ofHom (ContinuousMap.subtypeVal (fiber φ))) = TopCat.ofHom (incl φ)

The fibre inclusion into the subspace, followed by its inclusion into the mapping torus, is the usual fibre inclusion.

instance TauCeti.MappingTorus.isIso_fiberPairIncl {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : CategoryTheory.IsIso (fiberPairIncl φ)

The fibre inclusion is an isomorphism onto the fibre: it is MappingTorus.fiberHomeomorph.

def TauCeti.MappingTorus.cylinderMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : C(F × ↑unitInterval, MappingTorus φ)

The map (x, t) ↦ [φ x, t] from the cylinder onto the mapping torus. It is the monodromy homotopy MappingTorus.monodromyHomotopy, read as a map out of the cylinder F × I.

@[simp]

theorem TauCeti.MappingTorus.cylinderMap_apply {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) (p : F × ↑unitInterval) : (cylinderMap φ) p = mk φ (φ p.1) ↑p.2

def TauCeti.MappingTorus.cylinderPairMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : cylinderBoundaryPair ↧F ⟶ fiberPair φ

The map of pairs (F × I, F × ∂I) ⟶ (T, F) induced by MappingTorus.cylinderMap.

theorem TauCeti.MappingTorus.cylinderPairMap_fst {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : TopPair.Hom.fst (cylinderPairMap φ) = TopCat.ofHom (cylinderMap φ)

@[simp]

theorem TauCeti.MappingTorus.cylinderPairMap_fst_apply {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) (p : F × ↑unitInterval) : (CategoryTheory.ConcreteCategory.hom (TopPair.Hom.fst (cylinderPairMap φ))) p = mk φ (φ p.1) ↑p.2

@[simp]

theorem TauCeti.MappingTorus.cylinderPairMap_snd_apply {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) (p : ↑TopPair.snd) : ↑((CategoryTheory.ConcreteCategory.hom (TopPair.Hom.snd (cylinderPairMap φ))) p) = mk φ (φ (↑p).1) ↑(↑p).2

@[simp]

theorem TauCeti.MappingTorus.cylinderBoundaryι₀_comp_cylinderPairMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₀ ↧F) (TopPair.Hom.snd (cylinderPairMap φ)) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom { toFun := ⇑φ, continuous_toFun := ⋯ }) (fiberPairIncl φ)

On the bottom end of the cylinder, the cylinder map is the fibre inclusion after φ.

@[simp]

theorem TauCeti.MappingTorus.cylinderBoundaryι₀_comp_cylinderPairMap_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {Z : TopCat} (h : TopPair.snd ⟶ Z) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₀ ↧F) (CategoryTheory.CategoryStruct.comp (TopPair.Hom.snd (cylinderPairMap φ)) h) = CategoryTheory.CategoryStruct.comp (TopCat.ofHom { toFun := ⇑φ, continuous_toFun := ⋯ }) (CategoryTheory.CategoryStruct.comp (fiberPairIncl φ) h)

On the bottom end of the cylinder, the cylinder map is the fibre inclusion after φ.

@[simp]

theorem TauCeti.MappingTorus.cylinderBoundaryι₁_comp_cylinderPairMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₁ ↧F) (TopPair.Hom.snd (cylinderPairMap φ)) = fiberPairIncl φ

On the top end of the cylinder, the cylinder map is the fibre inclusion.

@[simp]

theorem TauCeti.MappingTorus.cylinderBoundaryι₁_comp_cylinderPairMap_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {Z : TopCat} (h : TopPair.snd ⟶ Z) : CategoryTheory.CategoryStruct.comp (cylinderBoundaryι₁ ↧F) (CategoryTheory.CategoryStruct.comp (TopPair.Hom.snd (cylinderPairMap φ)) h) = CategoryTheory.CategoryStruct.comp (fiberPairIncl φ) h

On the top end of the cylinder, the cylinder map is the fibre inclusion.

Thickening the fibre and the ends of the cylinder

theorem TauCeti.MappingTorus.isIso_singularHomologyMap_cylinderPairMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.IsIso (TopPair.singularHomologyMap (cylinderPairMap φ) R n)

The cylinder map induces isomorphisms on relative homology: the map of pairs (F × I, F × ∂I) ⟶ (T, F) given by (x, t) ↦ [φ x, t] induces isomorphisms Hₙ(F × I, F × ∂I) ≅ Hₙ(T, F) in every degree.

theorem TauCeti.MappingTorus.isZero_singularHomology_fiberPair_zero {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) : CategoryTheory.Limits.IsZero ((fiberPair φ).singularHomology R 0)

The relative homology H₀(T, F) vanishes, like that of the cylinder modulo its ends.

noncomputable def TauCeti.MappingTorus.singularHomologyFiberPairIso {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (fiberPair φ).singularHomology R (n + 1) ≅ ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F

The homology of a mapping torus modulo a fibre: Hₙ₊₁(T, F) ≅ Hₙ(F). It is the inverse of the isomorphism induced by the cylinder map, followed by the homology of the cylinder modulo its ends, singularHomologyCylinderBoundaryPairIso.

@[simp]

theorem TauCeti.MappingTorus.singularHomologyMap_cylinderPairMap_comp_singularHomologyFiberPairIso_hom {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (cylinderPairMap φ) R (n + 1)) (singularHomologyFiberPairIso φ R n).hom = (singularHomologyCylinderBoundaryPairIso (↧F) R n).hom

The isomorphism Hₙ₊₁(T, F) ≅ Hₙ(F) after the map induced by the cylinder map is the homology of the cylinder modulo its ends.

@[simp]

theorem TauCeti.MappingTorus.singularHomologyMap_cylinderPairMap_comp_singularHomologyFiberPairIso_hom_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) {Z : A} (h : ((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F ⟶ Z) : CategoryTheory.CategoryStruct.comp (TopPair.singularHomologyMap (cylinderPairMap φ) R (n + 1)) (CategoryTheory.CategoryStruct.comp (singularHomologyFiberPairIso φ R n).hom h) = CategoryTheory.CategoryStruct.comp (singularHomologyCylinderBoundaryPairIso (↧F) R n).hom h

The isomorphism Hₙ₊₁(T, F) ≅ Hₙ(F) after the map induced by the cylinder map is the homology of the cylinder modulo its ends.

theorem TauCeti.MappingTorus.singularHomologyδ_fiberPair {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {A : Type u} [CategoryTheory.Category.{v, u} A] [CategoryTheory.Limits.HasCoproducts A] [CategoryTheory.Abelian A] (R : A) (n : ℕ) : (fiberPair φ).singularHomologyδ R (n + 1) n ⋯ = CategoryTheory.CategoryStruct.comp (singularHomologyFiberPairIso φ R n).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (((AlgebraicTopology.singularHomologyFunctor A n).obj R).obj ↧F) - ((AlgebraicTopology.singularHomologyFunctor A n).obj R).map (TopCat.ofHom { toFun := ⇑φ, continuous_toFun := ⋯ })) (((AlgebraicTopology.singularHomologyFunctor A n).obj R).map (fiberPairIncl φ)))

The connecting morphism of a mapping torus modulo a fibre. Under Hₙ₊₁(T, F) ≅ Hₙ(F), the connecting morphism Hₙ₊₁(T, F) ⟶ Hₙ(F) of the pair is id - φ_* followed by the map induced by the fibre inclusion.