Singular chains of a mapping torus

The fibre of the mapping torus of φ : F ≃ₜ F has a canonical inclusion at height zero. Traversing the cylinder from height zero to height one gives a homotopy from this inclusion after φ to the inclusion itself. This file transfers that homotopy to singular chains and homology.

Thus the inclusion coequalizes the identity and monodromy maps, first up to chain homotopy and then on homology. This is the elementary chain-level relation behind the endomorphism id - φ_* in the Wang sequence of a mapping torus.

Main declarations

• TauCeti.MappingTorus.singularChainHomotopy: the composite of the monodromy chain map with the fibre-inclusion chain map is chain-homotopic to the fibre-inclusion map.
• TauCeti.MappingTorus.homologyMap_monodromy_comp_incl: the corresponding equality on singular homology.

The construction follows the mapping-torus derivation of the Wang sequence; see A. Hatcher, Algebraic Topology, Section 2.2. The chain homotopy itself is obtained from Mathlib's homotopy invariance of singular chains, TopCat.Homotopy.singularChainComplexFunctorObjMap.

noncomputable def TauCeti.MappingTorus.singularChainHomotopy {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : Homotopy (CategoryTheory.CategoryStruct.comp (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom { toFun := ⇑φ, continuous_toFun := ⋯ })) (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom (incl φ)))) (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom (incl φ)))

The singular-chain map induced by monodromy followed by fibre inclusion is chain-homotopic to the fibre-inclusion chain map.

Equations

• TauCeti.MappingTorus.singularChainHomotopy φ R = (Homotopy.ofEq ⋯).trans ((have this := TauCeti.MappingTorus.monodromyHomotopy φ; this).singularChainComplexFunctorObjMap R)

@[simp]

theorem TauCeti.MappingTorus.homologyMap_monodromy_comp_incl {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) [CategoryTheory.CategoryWithHomology C] (n : ℕ) : CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom { toFun := ⇑φ, continuous_toFun := ⋯ })) n) (HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom (incl φ))) n) = HomologicalComplex.homologyMap (((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom (incl φ))) n

On singular homology, the map induced by the fibre inclusion is unchanged after precomposition with the monodromy map.