Mapping tori and fibering over the circle

For a homeomorphism φ : F ≃ₜ F, the mapping torus identifies (φ x, t + 1) with (x, t). The quotient model below is deliberately topological: manifold charts are separate geometric input. Local product charts for the circle projection are constructed in TauCeti.Topology.MappingTorus.LocalProduct. MappingTorusPresentation stores the fibre and monodromy, while FibersOverCircle asserts that such a presentation exists.

Functions on the cylinder F × ℝ invariant under the integer action descend to the mapping torus through MappingTorus.lift, its universal property as a quotient.

The quotient projection to UnitAddCircle records the circle coordinate of each orbit; the fibre over 0 is MappingTorus.fiber, the image of the inclusion MappingTorus.incl. The map MappingTorus.incl includes the fibre at height zero. Moving once around the cylinder gives MappingTorus.monodromyHomotopy, a homotopy from this inclusion after the monodromy to the inclusion itself.

A continuous map g : F → G intertwining monodromies φ and ψ induces MappingTorus.map φ ψ g h : C(MappingTorus φ, MappingTorus ψ), acting on cylinder representatives by g in the fibre coordinate and the identity in the height coordinate. These induced maps lie over the circle (MappingTorus.proj_comp_map), restrict to g on the fibres at height zero (MappingTorus.map_comp_incl), and are functorial (MappingTorus.map_id, MappingTorus.map_comp). They are the maps needed to state naturality of constructions on mapping tori under commuting squares of monodromies.

The construction follows the standard mapping-torus model, e.g. Hatcher, Algebraic Topology, Section 2.2.

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

The integer action translating the real coordinate and applying monodromy.

@[instance_reducible]

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

The additive action whose orbits form the mapping torus.

@[simp]

theorem TauCeti.MappingTorus.action_vadd {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (n : ℤ) (p : F × ℝ) : n +ᵥ p = ((φ ^ n) p.1, p.2 + ↑n)

The defining integer action applies monodromy and translates the height.

@[reducible, inline]

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

The topological mapping torus of a self-homeomorphism.

def TauCeti.MappingTorus.mk {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (x : F) (t : ℝ) : MappingTorus φ

The quotient map from the cylinder used to construct the mapping torus.

@[simp]

theorem TauCeti.MappingTorus.mk_vadd {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (n : ℤ) (x : F) (t : ℝ) : mk φ ((φ ^ n) x) (t + ↑n) = mk φ x t

The quotient identifies (φ ^ n) x at height t + n with x at height t.

@[simp]

theorem TauCeti.MappingTorus.mk_apply_add_one {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (x : F) (t : ℝ) : mk φ (φ x) (t + 1) = mk φ x t

The quotient identifies φ x at height t + 1 with x at height t: the simp-normal form of mk_vadd at n = 1.

theorem TauCeti.MappingTorus.mk_eq_iff {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) {x y : F} {t s : ℝ} : mk φ x t = mk φ y s ↔ ∃ (n : ℤ), (φ ^ n) y = x ∧ s + ↑n = t

Two cylinder points represent the same mapping-torus point exactly when they differ by an integer translate in the monodromy orbit and the corresponding height translate.

theorem TauCeti.MappingTorus.mk_surjective {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : Function.Surjective fun (p : F × ℝ) => mk φ p.1 p.2

Every point of a mapping torus is represented by a point of the cylinder.

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

The quotient map from the cylinder to the mapping torus is continuous.

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

The cylinder quotient defining a mapping torus is an open map.

def TauCeti.MappingTorus.lift {F : Type u_1} [TopologicalSpace F] {β : Sort u_2} (φ : F ≃ₜ F) (f : F × ℝ → β) (hf : ∀ (n : ℤ) (x : F) (t : ℝ), f ((φ ^ n) x, t + ↑n) = f (x, t)) : MappingTorus φ → β

The universal property of the mapping torus. A function on the cylinder F × ℝ which is invariant under the integer action, f ((φ ^ n) x, t + n) = f (x, t), descends to the mapping torus.

@[simp]

theorem TauCeti.MappingTorus.lift_mk {F : Type u_1} [TopologicalSpace F] {β : Sort u_2} (φ : F ≃ₜ F) (f : F × ℝ → β) (hf : ∀ (n : ℤ) (x : F) (t : ℝ), f ((φ ^ n) x, t + ↑n) = f (x, t)) (x : F) (t : ℝ) : lift φ f hf (mk φ x t) = f (x, t)

theorem TauCeti.MappingTorus.continuous_lift {F : Type u_1} [TopologicalSpace F] {β : Type u_2} [TopologicalSpace β] (φ : F ≃ₜ F) {f : F × ℝ → β} (hf : ∀ (n : ℤ) (x : F) (t : ℝ), f ((φ ^ n) x, t + ↑n) = f (x, t)) (hc : Continuous f) : Continuous (lift φ f hf)

A continuous function on the cylinder descends to a continuous function on the mapping torus.

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

The canonical inclusion of the fibre at height zero into its mapping torus.

@[simp]

theorem TauCeti.MappingTorus.incl_apply {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (x : F) : (incl φ) x = mk φ x 0

The fibre inclusion sends a point to its class at height zero.

def TauCeti.MappingTorus.monodromyHomotopy {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : ((incl φ).comp { toFun := ⇑φ, continuous_toFun := ⋯ }).Homotopy (incl φ)

Going once around the mapping torus gives a homotopy from the fibre inclusion after monodromy to the fibre inclusion itself.

@[simp]

theorem TauCeti.MappingTorus.monodromyHomotopy_apply {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (t : ↑unitInterval) (x : F) : (monodromyHomotopy φ) (t, x) = mk φ (φ x) ↑t

The canonical monodromy homotopy moves linearly in the cylinder coordinate.

def TauCeti.MappingTorus.map {F : Type u_1} [TopologicalSpace F] {G : Type u_2} [TopologicalSpace G] (φ : F ≃ₜ F) (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : C(MappingTorus φ, MappingTorus ψ)

A continuous map intertwining two monodromies induces a map of their mapping tori.

@[simp]

theorem TauCeti.MappingTorus.map_mk {F : Type u_1} [TopologicalSpace F] {G : Type u_2} [TopologicalSpace G] (φ : F ≃ₜ F) (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) (x : F) (t : ℝ) : (map φ ψ g h) (mk φ x t) = mk ψ (g x) t

The map induced between mapping tori acts on cylinder representatives by the original map.

@[simp]

theorem TauCeti.MappingTorus.map_comp_incl {F : Type u_1} [TopologicalSpace F] {G : Type u_2} [TopologicalSpace G] (φ : F ≃ₜ F) (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : (map φ ψ g h).comp (incl φ) = (incl ψ).comp g

A map of mapping tori restricts on the fibre to the map intertwining the monodromies.

@[simp]

theorem TauCeti.MappingTorus.map_monodromyHomotopy {F : Type u_1} [TopologicalSpace F] {G : Type u_2} [TopologicalSpace G] (φ : F ≃ₜ F) (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) (t : ↑unitInterval) (x : F) : (map φ ψ g h) ((monodromyHomotopy φ) (t, x)) = (monodromyHomotopy ψ) (t, g x)

A map of mapping tori carries the canonical cylinder homotopy to the canonical cylinder homotopy of the image point.

@[simp]

theorem TauCeti.MappingTorus.map_id {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : map φ φ (ContinuousMap.id F) ⋯ = ContinuousMap.id (MappingTorus φ)

The map of a mapping torus induced by the identity map is the identity.

@[simp]

theorem TauCeti.MappingTorus.map_comp {F : Type u_1} [TopologicalSpace F] {G : Type u_2} [TopologicalSpace G] {H : Type u_3} [TopologicalSpace H] (φ : F ≃ₜ F) (ψ : G ≃ₜ G) (χ : H ≃ₜ H) (g : C(F, G)) (k : C(G, H)) (hg : Function.Semiconj ⇑g ⇑φ ⇑ψ) (hk : Function.Semiconj ⇑k ⇑ψ ⇑χ) : (map ψ χ k hk).comp (map φ ψ g hg) = map φ χ (k.comp g) ⋯

Maps of mapping tori respect composition of maps intertwining the monodromies.

def TauCeti.MappingTorus.proj {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : MappingTorus φ → UnitAddCircle

The canonical projection of a mapping torus to the circle.

@[simp]

theorem TauCeti.MappingTorus.proj_mk {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (x : F) (t : ℝ) : proj φ (mk φ x t) = ↑t

theorem TauCeti.MappingTorus.continuous_proj {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : Continuous (proj φ)

The canonical projection from a mapping torus to the additive circle is continuous.

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

The fibre of a mapping torus over 0 in the circle. It is the image of the fibre inclusion MappingTorus.incl (MappingTorus.range_incl).

@[simp]

theorem TauCeti.MappingTorus.mem_fiber_iff {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) {z : MappingTorus φ} : z ∈ fiber φ ↔ proj φ z = 0

theorem TauCeti.MappingTorus.isClosed_fiber {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : IsClosed (fiber φ)

The fibre over 0 is closed.

theorem TauCeti.MappingTorus.incl_mem_fiber {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) (x : F) : (incl φ) x ∈ fiber φ

The fibre inclusion lands in the fibre over 0.

@[simp]

theorem TauCeti.MappingTorus.range_incl {F : Type u_1} [TopologicalSpace F] (φ : F ≃ₜ F) : Set.range ⇑(incl φ) = fiber φ

The fibre over 0 is exactly the image of the fibre inclusion.

theorem TauCeti.MappingTorus.proj_surjective {F : Type u_1} [TopologicalSpace F] [Nonempty F] (φ : F ≃ₜ F) : Function.Surjective (proj φ)

The projection from the mapping torus of a nonempty space onto the circle is surjective.

@[simp]

theorem TauCeti.MappingTorus.proj_comp_map {F : Type u_1} [TopologicalSpace F] {G : Type u_2} [TopologicalSpace G] (φ : F ≃ₜ F) (ψ : G ≃ₜ G) (g : C(F, G)) (h : Function.Semiconj ⇑g ⇑φ ⇑ψ) : { toFun := proj ψ, continuous_toFun := ⋯ }.comp (map φ ψ g h) = { toFun := proj φ, continuous_toFun := ⋯ }

A map of mapping tori preserves the projection to the circle.

structure TauCeti.MappingTorusPresentation (M : Type u) [TopologicalSpace M] : Type (u + 1)

A mapping-torus presentation of a topological space, including its fibre and monodromy.

• Fiber : Type u

  The fibre type.

• nonemptyFiber : Nonempty self.Fiber

  The fibre is nonempty.

• fiberTopology : TopologicalSpace self.Fiber

  The topology carried by the fibre.

• monodromy : self.Fiber ≃ₜ self.Fiber

  The monodromy homeomorphism around the circle.

• equivalence : M ≃ₜ MappingTorus self.monodromy

  A homeomorphism from the presented space to the mapping torus.

def TauCeti.FibersOverCircle (M : Type u) [TopologicalSpace M] : Prop

A space fibres over the circle when it is homeomorphic to a mapping torus.

def TauCeti.MappingTorus.presentation {F : Type u_1} [TopologicalSpace F] [Nonempty F] (φ : F ≃ₜ F) : MappingTorusPresentation (MappingTorus φ)

The mapping torus has its canonical presentation.

theorem TauCeti.fibersOverCircle_mappingTorus {F : Type u_1} [TopologicalSpace F] [Nonempty F] (φ : F ≃ₜ F) : FibersOverCircle (MappingTorus φ)

The mapping torus carries its canonical fibering-over-the-circle presentation.

theorem Homeomorph.fibersOverCircle {M N : Type u} [TopologicalSpace M] [TopologicalSpace N] (h : M ≃ₜ N) (hN : TauCeti.FibersOverCircle N) : TauCeti.FibersOverCircle M

A homeomorphism transports a fibering-over-the-circle presentation.

theorem TauCeti.FibersOverCircle.infinite {M : Type u} [TopologicalSpace M] (h : FibersOverCircle M) : Infinite M

A space that fibers over the circle is infinite, since it maps onto the circle.