The infinite cyclic cover of a mapping torus

The mapping torus of a homeomorphism φ : F ≃ₜ F is the orbit space of the action of ℤ on the cylinder F × ℝ by n +ᵥ (x, t) = (φⁿ x, t + n). This action is free and every point has a neighbourhood, a slab of height less than one, whose translates are pairwise disjoint. So the quotient map F × ℝ → MappingTorus φ is a quotient covering map for this ℤ-action (TauCeti.MappingTorus.isAddQuotientCoveringMap_coverMap): it is the infinite cyclic cover of the mapping torus. (When F is disconnected the covering may have further deck transformations; only the ℤ-action is used here.)

The deck transformation generating the action is TauCeti.MappingTorus.deck φ, (x, t) ↦ (φ x, t + 1). It lies over the monodromy φ under the projection F × ℝ → F, which is a homotopy equivalence (TauCeti.MappingTorus.cylinderHomotopyEquiv). This is the starting point of Milnor's derivation of the Wang sequence from the infinite cyclic cover.

References

• J. Milnor, Infinite cyclic coverings, Conference on the Topology of Manifolds (1968), Section 1.
• A. Hatcher, Algebraic Topology, Section 2.2 (the mapping-torus construction).

def TauCeti.MappingTorus.coverMap {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : C(F × ℝ, MappingTorus φ)

The quotient map from the cylinder F × ℝ onto the mapping torus, as a continuous map.

@[simp]

theorem TauCeti.MappingTorus.coverMap_apply {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (p : F × ℝ) : (coverMap φ) p = mk φ p.1 p.2

theorem TauCeti.MappingTorus.isAddQuotientCoveringMap_coverMap {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : IsAddQuotientCoveringMap ⇑(coverMap φ) ℤ

The mapping torus is the quotient of the cylinder by a covering action of ℤ. The quotient map F × ℝ → MappingTorus φ is a quotient covering map for the action n +ᵥ (x, t) = (φⁿ x, t + n) of ℤ.

def TauCeti.MappingTorus.deck {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : F × ℝ ≃ₜ F × ℝ

The deck transformation (x, t) ↦ (φ x, t + 1) of the cylinder over the mapping torus: the action of the generator 1 : ℤ.

@[simp]

theorem TauCeti.MappingTorus.deck_apply {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (p : F × ℝ) : (deck φ) p = (φ p.1, p.2 + 1)

theorem TauCeti.MappingTorus.deck_eq_vadd {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (p : F × ℝ) : (deck φ) p = 1 +ᵥ p

The deck transformation is the action of 1 : ℤ.

theorem TauCeti.MappingTorus.coverMap_deck {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (p : F × ℝ) : (coverMap φ) ((deck φ) p) = (coverMap φ) p

The deck transformation covers the identity of the mapping torus.

def TauCeti.MappingTorus.cylinderHomotopyEquiv (F : Type u_1) [TopologicalSpace F] : ContinuousMap.HomotopyEquiv (F × ℝ) F

The projection of the cylinder F × ℝ onto F is a homotopy equivalence, whose homotopy inverse is the inclusion at height zero: the cylinder deformation retracts onto F × {0} by scaling the height.

@[simp]

theorem TauCeti.MappingTorus.cylinderHomotopyEquiv_apply {F : Type u_1} [TopologicalSpace F] (p : F × ℝ) : (cylinderHomotopyEquiv F).toFun p = p.1

@[simp]

theorem TauCeti.MappingTorus.cylinderHomotopyEquiv_invFun_apply {F : Type u_1} [TopologicalSpace F] (x : F) : (cylinderHomotopyEquiv F).invFun x = (x, 0)