Local products for mapping tori

The projection of the mapping torus of a homeomorphism φ : F ≃ₜ F to the circle is locally a product with fibre F. Cutting the circle at the class of a : ℝ chooses the unique representative of each remaining height in (a, a + 1). The corresponding open cylinder embeds in the mapping torus and covers precisely the inverse image of the cut circle.

MappingTorus.localProduct identifies that inverse image with the cut circle times F, commuting with the projections. Thus mapping-torus presentations supply actual local product charts for fibering over the circle, for arbitrary topological fibres and monodromies.

The fibre inclusion MappingTorus.incl factors through such an open cylinder, so it is an embedding (MappingTorus.isEmbedding_incl) and a homeomorphism onto the fibre over 0 (MappingTorus.fiberHomeomorph).

References

• A. Hatcher, Algebraic Topology, Section 2.2 (the mapping-torus construction).

theorem TauCeti.MappingTorus.isOpenEmbedding_mk_Ioo {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (a : ℝ) : Topology.IsOpenEmbedding fun (p : F × ↑(Set.Ioo a (a + 1))) => mk φ p.1 ↑p.2

The cylinder over an open interval of length one embeds openly in the mapping torus.

theorem TauCeti.MappingTorus.range_mk_Ioo {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (a : ℝ) : (Set.range fun (p : F × ↑(Set.Ioo a (a + 1))) => mk φ p.1 ↑p.2) = (proj φ ⁻¹' {↑a})ᶜ

The cylinder over (a, a + 1) covers precisely the part of the mapping torus lying over the circle cut at a.

theorem TauCeti.MappingTorus.isEmbedding_incl {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : Topology.IsEmbedding ⇑(incl φ)

The fibre inclusion at height zero is an embedding: it factors through the open cylinder over (-1/2, 1/2).

noncomputable def TauCeti.MappingTorus.fiberHomeomorph {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : F ≃ₜ ↑(fiber φ)

The fibre inclusion MappingTorus.incl is a homeomorphism onto the fibre over 0.

@[simp]

theorem TauCeti.MappingTorus.coe_fiberHomeomorph_apply {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (x : F) : ↑((fiberHomeomorph φ) x) = (incl φ) x

noncomputable def TauCeti.MappingTorus.localProduct {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (a : ℝ) : ↑(proj φ ⁻¹' {↑a})ᶜ ≃ₜ ↑{↑a}ᶜ × F

A local product chart for the mapping-torus projection on the circle cut at a. The inverse inserts the unique height representative in (a, a + 1).

@[simp]

theorem TauCeti.MappingTorus.localProduct_fst {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (a : ℝ) (z : ↑(proj φ ⁻¹' {↑a})ᶜ) : ↑((localProduct φ a) z).1 = proj φ ↑z

The local product preserves the circle coordinate.

@[simp]

theorem TauCeti.MappingTorus.localProduct_symm_apply {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (a : ℝ) (p : ↑{↑a}ᶜ × F) : ↑((localProduct φ a).symm p) = mk φ p.2 ↑((AddCircle.equivIco 1 a) ↑p.1)

The inverse local product chart uses the representative in (a, a + 1) and leaves the fibre coordinate unchanged.

@[simp]

theorem TauCeti.MappingTorus.localProduct_mk {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (a : ℝ) (x : F) (t : ℝ) (ht : t ∈ Set.Ioo a (a + 1)) : ((localProduct φ a) ⟨mk φ x t, ⋯⟩).2 = x

The local product chart recovers the fibre coordinate of a cylinder point whose height lies in the chosen interval.

theorem TauCeti.MappingTorus.isHomeomorphicTrivialFiberBundle_proj {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (a : ℝ) : IsHomeomorphicTrivialFiberBundle F fun (z : ↑(proj φ ⁻¹' {↑a})ᶜ) => ⟨proj φ ↑z, ⋯⟩

Over the cut circle, the mapping-torus projection is a trivial fibre bundle with fibre F.

theorem TauCeti.MappingTorus.exists_isHomeomorphicTrivialFiberBundle_proj {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (θ : UnitAddCircle) : ∃ (U : Set UnitAddCircle), IsOpen U ∧ θ ∈ U ∧ IsHomeomorphicTrivialFiberBundle F fun (z : ↑(proj φ ⁻¹' U)) => ⟨proj φ ↑z, ⋯⟩

Every circle point has an open neighbourhood on which the mapping-torus projection is a trivial fibre bundle with the original fibre.