The singular chains of the infinite cyclic cover of a mapping torus

Let φ : F ≃ₜ F be a homeomorphism. The mapping torus T_φ is the quotient of the cylinder F × ℝ by the covering action of ℤ generated by the deck transformation τ : (x, t) ↦ (φ x, t + 1). This file proves that the singular chains of the cover and of the mapping torus form a short exact sequence of chain complexes 0 ⟶ C(F × ℝ; R) ⟶ C(F × ℝ; R) ⟶ C(T_φ; R) ⟶ 0, whose first map is 𝟙 - τ_* and whose second map is induced by the covering map.

• TauCeti.MappingTorus.isColimitCyclicCoverCokernelCofork: the chains of the mapping torus are the cokernel of 𝟙 - τ_*. Since the mapping torus is the quotient of F × ℝ by a covering action, its chains are the coinvariants of the action of ℤ on the chains of F × ℝ (IsQuotientCoveringMap.isColimitMapCoconeSingularChainComplex), and coinvariants of ℤ are a cokernel of 𝟙 - τ_*.
• TauCeti.MappingTorus.isSplitMono_id_sub_deckChainMap_f: in each degree, 𝟙 - τ_* is a split monomorphism. The deck transformation permutes the singular simplices of F × ℝ freely, raising the integer part of the height of the initial vertex by one, so the retraction telescopes along each orbit (TauCeti.isSplitMono_id_sub).
• TauCeti.MappingTorus.cyclicCoverShortComplex_shortExact: the short exact sequence, for coefficients in an abelian category with coproducts.

The projection F × ℝ → F is a homotopy equivalence carrying τ to φ. Through it, the long exact homology sequence of this short exact sequence is the Wang sequence ⋯ ⟶ Hₙ(F) ⟶ Hₙ(F) ⟶ Hₙ(T_φ) ⟶ Hₙ₋₁(F) ⟶ ⋯ of the mapping torus, with first map 𝟙 - φ_*; see TauCeti.AlgebraicTopology.Singular.MappingTorus.Wang.

References

• J. Milnor, Infinite cyclic coverings, Conference on the Topology of Manifolds (1968), Section 1, for the exact sequence of the chains of an infinite cyclic cover.
• A. Hatcher, Algebraic Topology, Section 2.2, Example 2.48, for the Wang sequence of a mapping torus.

noncomputable def TauCeti.MappingTorus.deckChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(F × ℝ) ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(F × ℝ)

The endomorphism τ_* of the singular chains of the cylinder F × ℝ induced by the deck transformation τ : (x, t) ↦ (φ x, t + 1).

theorem TauCeti.MappingTorus.deckChainMap_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : deckChainMap φ R = ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom ↑(deck φ))

The deck chain map is the singular-chain functor applied to the deck transformation.

noncomputable def TauCeti.MappingTorus.coverChainMap {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(F × ℝ) ⟶ ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus φ)

The map from the singular chains of the cylinder F × ℝ to those of the mapping torus induced by the covering map.

theorem TauCeti.MappingTorus.coverChainMap_def {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) : coverChainMap φ R = ((AlgebraicTopology.singularChainComplexFunctor C).obj R).map (TopCat.ofHom (coverMap φ))

The cover chain map is the singular-chain functor applied to the covering map.

@[simp]

theorem TauCeti.MappingTorus.deckChainMap_comp_coverChainMap {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.CategoryStruct.comp (deckChainMap φ R) (coverChainMap φ R) = coverChainMap φ R

The covering map is invariant under the deck transformation, so the cover chain map kills 𝟙 - τ_*.

@[simp]

theorem TauCeti.MappingTorus.deckChainMap_comp_coverChainMap_assoc {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) {Z : ChainComplex C ℕ} (h : ((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(MappingTorus φ) ⟶ Z) : CategoryTheory.CategoryStruct.comp (deckChainMap φ R) (CategoryTheory.CategoryStruct.comp (coverChainMap φ R) h) = CategoryTheory.CategoryStruct.comp (coverChainMap φ R) h

The covering map is invariant under the deck transformation, so the cover chain map kills 𝟙 - τ_*.

noncomputable def TauCeti.MappingTorus.isColimitCyclicCoverCokernelCofork {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.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (coverChainMap φ R) ⋯)

The chains of a mapping torus are a cokernel. The singular chains of the mapping torus of φ are the cokernel of 𝟙 - τ_* on the singular chains of the cylinder F × ℝ, with projection the cover chain map.

theorem TauCeti.MappingTorus.isSplitMono_id_sub_deckChainMap_f {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Preadditive C] (R : C) (n : ℕ) : CategoryTheory.IsSplitMono (CategoryTheory.CategoryStruct.id ((((AlgebraicTopology.singularChainComplexFunctor C).obj R).obj ↧(F × ℝ)).X n) - (deckChainMap φ R).f n)

In each degree, 𝟙 - τ_* is a split monomorphism on the singular chains of the cylinder. The deck transformation raises the integer part of the height of the initial vertex of a singular simplex by one, so it permutes the simplices freely and the retraction telescopes along each orbit.

@[reducible, inline]

noncomputable abbrev TauCeti.MappingTorus.cyclicCoverShortComplex {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.ShortComplex (ChainComplex C ℕ)

The chain-level short complex of the infinite cyclic cover of a mapping torus C(F × ℝ; R) ⟶ C(F × ℝ; R) ⟶ C(T_φ; R), with first map 𝟙 - τ_* and second map induced by the covering map.

theorem TauCeti.MappingTorus.cyclicCoverShortComplex_shortExact {F : Type w} [TopologicalSpace F] (φ : F ≃ₜ F) {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.Limits.HasCoproducts C] (R : C) : (cyclicCoverShortComplex φ R).ShortExact

The short exact sequence of the infinite cyclic cover of a mapping torus. For coefficients in an abelian category with coproducts, the sequence of singular chains 0 ⟶ C(F × ℝ; R) ⟶ C(F × ℝ; R) ⟶ C(T_φ; R) ⟶ 0, with first map 𝟙 - τ_* and second map induced by the covering map, is short exact.