Geometric structures modelled on Thurston's eight geometries

A space M has a geometric structure modelled on one of Thurston's eight geometries G, with model space X = G.Space, when M is homeomorphic to an orbit space X / Γ of a subgroup Γ of the full isometry group Isom X acting freely and properly discontinuously on X. This is the notion in the statement of the geometrization theorem: each piece of the prime and torus decomposition of a closed orientable 3-manifold admits a geometric structure.

Thurston and Scott equivalently describe a geometric structure as a complete (Isom X, X)-structure on M, that is, a complete locally homogeneous metric locally isometric to X. Every model space X is simply connected, so the developing map of a complete structure identifies M with such a quotient X / Γ; the quotient description is therefore taken as the definition here. In the other direction, the orbit space X / Γ carries the (Isom X, X)-atlas pushed forward from X (TauCeti.hasGroupoid_smulGroupoid_quotient_subgroup), so a space with a geometric structure is an (Isom X, X)-manifold (TauCeti.HasGeometricStructure.exists_hasGroupoid). In particular it is a smooth manifold and inherits a Riemannian metric from X (TauCeti.Geometry.Manifold.Riemannian.SMulGroupoid.Basic).

The structure is defined for a topological space M, up to homeomorphism. For 3-manifolds this agrees with the smooth notion, since by Moise's theorem every topological 3-manifold has a smooth structure, unique up to diffeomorphism.

As a first family of examples, every three-dimensional lens space L(m; ℓ₀, ℓ₁) is a spherical manifold: its lens group acts on the unit sphere of ℂ² by unitary rotations, which a real linear isometry ℂ² ≃ ℝ⁴ turns into isometries of the round three-sphere.

Main definitions

• TauCeti.HasGeometricStructure M G: M is homeomorphic to G.Space / Γ for a subgroup Γ of Isom G.Space acting freely and properly discontinuously.

Main results

• TauCeti.hasGeometricStructure_iff_exists_isQuotientMap: a geometric structure is a quotient map G.Space → M whose fibres are the orbits of such a subgroup.
• TauCeti.hasGeometricStructure_quotient and TauCeti.hasGeometricStructure_space: every such orbit space, and in particular the model space itself, has a geometric structure.
• Homeomorph.hasGeometricStructure_iff: having a geometric structure is invariant under homeomorphism.
• TauCeti.HasGeometricStructure.exists_hasGroupoid: a space with a geometric structure is an (Isom X, X)-manifold.
• TauCeti.LensSpace.hasGeometricStructure_spherical: three-dimensional lens spaces are spherical manifolds.

References

• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983), 401–487, Sections 1 and 4.
• W. P. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Princeton University Press (1997), Sections 3.4 (complete (G, X)-structures and the developing map) and 3.8 (model geometries and geometric manifolds).

def TauCeti.HasGeometricStructure (M : Type u_3) [TopologicalSpace M] (G : ModelGeometry) : Prop

A topological space M has a geometric structure modelled on the Thurston geometry G if it is homeomorphic to the orbit space X / Γ of a subgroup Γ of the isometry group of the model space X = G.Space acting freely and properly discontinuously on X.

theorem TauCeti.hasGeometricStructure_quotient {G : ModelGeometry} (Γ : Subgroup (Isom G.model G.Space)) [ProperlyDiscontinuousSMul (↥Γ) G.Space] [IsCancelSMul (↥Γ) G.Space] : HasGeometricStructure (MulAction.orbitRel.Quotient (↥Γ) G.Space) G

The orbit space of a free, properly discontinuous action of a group of isometries of a model space has a geometric structure modelled on that geometry.

theorem Homeomorph.hasGeometricStructure_iff {M : Type u_1} {N : Type u_2} [TopologicalSpace M] [TopologicalSpace N] {G : TauCeti.ModelGeometry} (e : M ≃ₜ N) : TauCeti.HasGeometricStructure M G ↔ TauCeti.HasGeometricStructure N G

Having a geometric structure modelled on G is invariant under homeomorphism.

theorem TauCeti.hasGeometricStructure_of_isQuotientMap {M : Type u_1} [TopologicalSpace M] {G : ModelGeometry} (Γ : Subgroup (Isom G.model G.Space)) [ProperlyDiscontinuousSMul (↥Γ) G.Space] [IsCancelSMul (↥Γ) G.Space] {f : G.Space → M} (hf : Topology.IsQuotientMap f) (hfib : ∀ (x y : G.Space), f x = f y ↔ (MulAction.orbitRel (↥Γ) G.Space) x y) : HasGeometricStructure M G

If a quotient map from the model space G.Space onto M identifies exactly the points in the same orbit of a group of isometries acting freely and properly discontinuously, then M has a geometric structure modelled on G.

theorem TauCeti.hasGeometricStructure_iff_exists_isQuotientMap {M : Type u_1} [TopologicalSpace M] {G : ModelGeometry} : HasGeometricStructure M G ↔ ∃ (Γ : Subgroup (Isom G.model G.Space)), ProperlyDiscontinuousSMul (↥Γ) G.Space ∧ IsCancelSMul (↥Γ) G.Space ∧ ∃ (f : G.Space → M), Topology.IsQuotientMap f ∧ ∀ (x y : G.Space), f x = f y ↔ (MulAction.orbitRel (↥Γ) G.Space) x y

A space has a geometric structure modelled on G exactly when it is the target of a quotient map from the model space G.Space whose fibres are the orbits of a group of isometries acting freely and properly discontinuously.

theorem TauCeti.hasGeometricStructure_space (G : ModelGeometry) : HasGeometricStructure G.Space G

Each model space has a geometric structure modelled on its own geometry.

theorem TauCeti.HasGeometricStructure.exists_hasGroupoid {M : Type u_1} [TopologicalSpace M] {G : ModelGeometry} (h : HasGeometricStructure M G) : ∃ (x : ChartedSpace G.Space M), HasGroupoid M (smulGroupoid (Isom G.model G.Space) G.Space)

A space with a geometric structure modelled on G is an (Isom X, X)-manifold for the model space X = G.Space: it has an X-valued atlas whose transition maps are locally restrictions of isometries of X.

theorem TauCeti.LensSpace.hasGeometricStructure_spherical (m : ℕ) [NeZero m] (ℓ : Fin 2 → (ZMod m)ˣ) : HasGeometricStructure (LensSpace m ℓ) ModelGeometry.spherical

Three-dimensional lens spaces are spherical manifolds. A real linear isometry ℂ² ≃ ℝ⁴ carries the lens group, acting on the unit sphere of ℂ², to a finite group of isometries of the round three-sphere acting freely, and the lens space is its orbit space.