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 and the local-triviality theorem are separate geometric input. MappingTorusPresentation stores the fibre and monodromy, while FibersOverCircle asserts that such a presentation exists.

The quotient projection to UnitAddCircle records the circle coordinate of each orbit. 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.

Equations

• TauCeti.MappingTorus.vadd φ n p = ((φ ^ n) p.1, p.2 + ↑n)

@[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.

Equations

• TauCeti.MappingTorus.action φ = { vadd := TauCeti.MappingTorus.vadd φ, add_vadd := ⋯, zero_vadd := ⋯ }

@[reducible, inline]

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

The topological mapping torus of a self-homeomorphism.

Equations

• TauCeti.MappingTorus φ = AddAction.orbitRel.Quotient ℤ (F × ℝ)

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.

Equations

• TauCeti.MappingTorus.mk φ x t = Quotient.mk'' (x, t)

@[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.

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.

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.

Equations

• TauCeti.MappingTorus.incl φ = { toFun := fun (x : F) => TauCeti.MappingTorus.mk φ x 0, continuous_toFun := ⋯ }

@[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.

Equations

• TauCeti.MappingTorus.monodromyHomotopy φ = { toFun := fun (p : ↑unitInterval × F) => TauCeti.MappingTorus.mk φ (φ p.2) ↑p.1, continuous_toFun := ⋯, map_zero_left := ⋯, map_one_left := ⋯ }

@[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.

Equations

• TauCeti.MappingTorus.map φ ψ g h = { toFun := Quotient.lift (fun (p : F × ℝ) => TauCeti.MappingTorus.mk ψ (g p.1) p.2) ⋯, continuous_toFun := ⋯ }

@[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_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.

Equations

• TauCeti.MappingTorus.proj φ = Quotient.lift (fun (z : F × ℝ) => ↑z.2) ⋯

@[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.

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.

Equations

• TauCeti.FibersOverCircle M = Nonempty (TauCeti.MappingTorusPresentation M)

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

The mapping torus has its canonical presentation.

Equations

• TauCeti.MappingTorus.presentation φ = { Fiber := F, nonemptyFiber := ⋯, fiberTopology := inferInstance, monodromy := φ, equivalence := Homeomorph.refl (TauCeti.MappingTorus φ) }

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.