Seifert fibrations

A Seifert fibration of a 3-manifold M is a decomposition of M into disjoint circles, the fibres, such that every fibre has a neighbourhood which is a union of fibres and is isomorphic, fibres to fibres, to a model fibred solid torus. Seifert-fibred pieces are, together with the atoroidal ones, the pieces of the JSJ decomposition of a 3-manifold, and six of Thurston's eight geometries are the geometries of Seifert-fibred spaces.

The model fibred solid torus V(p, q), for an integer q > 0 and an integer p coprime to q, is the solid torus D² × S¹ decomposed into the orbits of the circle action t • (z, w) = (t ^ p * z, t ^ q * w). The core {0} × S¹ is one fibre; every other fibre winds q times around the core direction. Cutting along a meridian disc presents V(p, q) as [0, 1] × D², decomposed into the segments [0, 1] × {x}, with its ends identified by the rotation through 2πp/q; this is the description of Hatcher and Scott.

The decomposition is recorded as a Setoid M whose classes are the fibres. The local condition is stated with open partial homeomorphisms onto open subsets of the closed model V(p, q), so that fibres in the boundary of M (modelled on fibres in the boundary torus of V(p, q)) are allowed and no separate model for boundary fibres is needed. Both the chart's source and its target are required to be unions of fibres; it follows that every fibre is a circle (TauCeti.IsSeifertFibration.nonempty_homeomorph_circle).

Only fibred solid tori occur as local models, as in Seifert's original definition. Scott also allows fibred solid Klein bottles, which are nonorientable; in an orientable 3-manifold, the case relevant to the JSJ decomposition and geometrization, the two definitions agree.

The predicate is a property of the decomposition alone. It forces M to be locally homeomorphic to open subsets of D² × S¹, but separation and countability hypotheses are kept separate, as in TauCeti.IsCompactConnectedThreeManifold.

Main definitions

• TauCeti.SolidTorus: the closed solid torus D² × S¹.
• TauCeti.SolidTorus.fiberSetoid p q: the fibres of the model fibred solid torus V(p, q).
• TauCeti.IsSeifertChart r p q e: the chart e carries the classes of r in its source onto the fibres of V(p, q) in its target.
• TauCeti.IsSeifertFibration r: the classes of r form a Seifert fibration.
• TauCeti.IsSeifertFibered M: M admits a Seifert fibration.

Main results

• TauCeti.IsSeifertFibration.nonempty_homeomorph_circle: every fibre of a Seifert fibration is homeomorphic to a circle.
• TauCeti.SolidTorus.isSeifertFibration_fiberSetoid: the model V(p, q) is Seifert fibred.
• TauCeti.isSeifertFibration_ker_fst: for a boundaryless surface F, the circles {x} × S¹ form a Seifert fibration of F × S¹.
• Homeomorph.isSeifertFibered_iff: being Seifert fibred is invariant under homeomorphism.

References

• H. Seifert, Topologie dreidimensionaler gefaserter Räume, Acta Math. 60 (1933), 147–238.
• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983), 401–487, Section 3.
• A. Hatcher, Notes on Basic 3-Manifold Topology, Section 2.1.

@[reducible, inline]

abbrev TauCeti.SolidTorus : Type

The closed solid torus D² × S¹, where D² is the closed unit disc of ℂ.

noncomputable def TauCeti.SolidTorus.homeomorphBallSphere : SolidTorus ≃ₜ ↑(Metric.closedBall 0 1) × ↑(Metric.sphere 0 1)

The solid torus identified with the product of the closed unit disc and the unit sphere of ℂ, for use with APIs stated in terms of metric balls and spheres.

@[simp]

theorem TauCeti.SolidTorus.homeomorphBallSphere_apply (p : SolidTorus) : homeomorphBallSphere p = (p.1, Circle.homeomorphSphere p.2)

@[simp]

theorem TauCeti.SolidTorus.homeomorphBallSphere_symm_apply (p : ↑(Metric.closedBall 0 1) × ↑(Metric.sphere 0 1)) : homeomorphBallSphere.symm p = (p.1, Circle.homeomorphSphere.symm p.2)

def TauCeti.SolidTorus.fiberSetoid (p q : ℤ) : Setoid SolidTorus

The fibres of the model fibred solid torus V(p, q): two points of D² × S¹ lie in the same fibre when they lie in the same orbit of the circle action t • (z, w) = (t ^ p * z, t ^ q * w). For q ≠ 0 the core {0} × S¹ is a single fibre. When moreover p is coprime to q, every other fibre winds q times around the core direction and p times around the meridian of the torus {|z| = r} × S¹ containing it.

theorem TauCeti.SolidTorus.fiberSetoid_iff {p q : ℤ} {a b : SolidTorus} : (fiberSetoid p q) a b ↔ ∃ (t : Circle), ↑(t ^ p) * ↑a.1 = ↑b.1 ∧ t ^ q * a.2 = b.2

The defining orbit condition of the fibres of V(p, q).

@[simp]

theorem TauCeti.SolidTorus.fiberSetoid_zero_one {a b : SolidTorus} : (fiberSetoid 0 1) a b ↔ a.1 = b.1

The fibres of V(0, 1) are the circles {z} × S¹ of the product fibration.

theorem TauCeti.SolidTorus.nonempty_homeomorph_circle {p q : ℤ} (hq : q ≠ 0) (hpq : IsCoprime p q) (a : SolidTorus) : Nonempty (↑{b : SolidTorus | (fiberSetoid p q) a b} ≃ₜ Circle)

Every fibre of the model fibred solid torus V(p, q), for q ≠ 0 and p coprime to q, is homeomorphic to a circle.

structure TauCeti.IsSeifertChart {M : Type u_1} [TopologicalSpace M] (r : Setoid M) (p q : ℤ) (e : OpenPartialHomeomorph M SolidTorus) : Prop

An open partial homeomorphism e from M to the solid torus is a Seifert chart of r onto the model V(p, q) when its source is a union of classes of r, its target is a union of fibres of V(p, q), and on its source e carries the classes of r onto fibres of V(p, q).

• source_saturated (x : M) : x ∈ e.source → ∀ (y : M), r x y → y ∈ e.source

  The source of the chart is a union of classes of r.

• target_saturated (a : SolidTorus) : a ∈ e.target → ∀ (b : SolidTorus), (SolidTorus.fiberSetoid p q) a b → b ∈ e.target

  The target of the chart is a union of fibres of V(p, q).

• rel_iff (x : M) : x ∈ e.source → ∀ y ∈ e.source, r x y ↔ (SolidTorus.fiberSetoid p q) (↑e x) (↑e y)

  On its source the chart carries the classes of r onto the fibres of V(p, q).

theorem TauCeti.IsSeifertChart.image_setOf_rel {M : Type u_1} [TopologicalSpace M] {r : Setoid M} {p q : ℤ} {e : OpenPartialHomeomorph M SolidTorus} (he : IsSeifertChart r p q e) {x : M} (hx : x ∈ e.source) : ↑e '' {y : M | r x y} = {b : SolidTorus | (SolidTorus.fiberSetoid p q) (↑e x) b}

A Seifert chart maps the class of a point of its source onto the fibre of V(p, q) through its image.

def TauCeti.IsSeifertFibration {M : Type u_1} [TopologicalSpace M] (r : Setoid M) : Prop

An equivalence relation on M is a Seifert fibration when every point of M lies in the source of a Seifert chart of r onto a model fibred solid torus V(p, q), with q > 0 and p coprime to q. Its classes, the fibres, are then circles.

theorem TauCeti.isSeifertFibration_iff {M : Type u_1} [TopologicalSpace M] {r : Setoid M} : IsSeifertFibration r ↔ ∀ (x : M), ∃ (p : ℤ) (q : ℤ), 0 < q ∧ IsCoprime p q ∧ ∃ (e : OpenPartialHomeomorph M SolidTorus), x ∈ e.source ∧ IsSeifertChart r p q e

The defining local condition of a Seifert fibration.

def TauCeti.IsSeifertFibered (M : Type u_1) [TopologicalSpace M] : Prop

A space is Seifert fibred when it admits a Seifert fibration.

theorem TauCeti.isSeifertFibered_iff {M : Type u_1} [TopologicalSpace M] : IsSeifertFibered M ↔ ∃ (r : Setoid M), IsSeifertFibration r

The defining condition of a Seifert-fibred space.

theorem TauCeti.IsSeifertFibration.nonempty_homeomorph_circle {M : Type u_1} [TopologicalSpace M] {r : Setoid M} (h : IsSeifertFibration r) (x : M) : Nonempty (↑{y : M | r x y} ≃ₜ Circle)

Every fibre of a Seifert fibration is homeomorphic to a circle.

theorem TauCeti.IsSeifertFibration.comap_homeomorph {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {r : Setoid M} (h : IsSeifertFibration r) (φ : N ≃ₜ M) : IsSeifertFibration (Setoid.comap (⇑φ) r)

A Seifert fibration pulls back along a homeomorphism.

theorem Homeomorph.isSeifertFibered_iff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] (φ : N ≃ₜ M) : TauCeti.IsSeifertFibered N ↔ TauCeti.IsSeifertFibered M

Being Seifert fibred is invariant under homeomorphism.

theorem TauCeti.SolidTorus.isSeifertFibration_fiberSetoid {p q : ℤ} (hq : 0 < q) (hpq : IsCoprime p q) : IsSeifertFibration (fiberSetoid p q)

The model fibred solid torus V(p, q), for q > 0 and p coprime to q, is Seifert fibred.

theorem TauCeti.SolidTorus.isSeifertFibered : IsSeifertFibered SolidTorus

The solid torus is Seifert fibred.

theorem TauCeti.isSeifertFibration_ker_fst {F : Type u_3} [TopologicalSpace F] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) F] : IsSeifertFibration (Setoid.ker Prod.fst)

For a boundaryless surface F, the circles {x} × S¹ form a Seifert fibration of F × S¹: near each fibre, a chart of F identifies it with the product fibration V(0, 1).

theorem TauCeti.isSeifertFibered_prod_circle (F : Type u_3) [TopologicalSpace F] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) F] : IsSeifertFibered (F × Circle)

The product of a boundaryless surface with a circle is Seifert fibred.