The model geometry SL₂ℝ~

The model geometry SL₂ℝ~ of Thurston's eight three-dimensional geometries is the universal cover of the unit tangent bundle of the hyperbolic plane, with its natural (Sasaki) metric. Its isometry group is four-dimensional and contains the universal cover of PSL₂ℝ, acting by left translations, whence the name.

This file models it on ℝ³ with coordinates (x, y, z). The pair (x, y) is the point x + i eʸ of the upper half-plane, so that e^{-2y} dx² + dy² is the hyperbolic metric in horocyclic coordinates, and z is an angle coordinate on the fibre, unwound to a real line. In the orthonormal frame e₁ = eʸ ∂ₓ, e₂ = ∂_y of the hyperbolic plane, with dual coframe θ₁ = e^{-y} dx, θ₂ = dy, one has dθ₁ = θ₁ ∧ θ₂ and dθ₂ = 0, so the Levi-Civita connection is ∇e₁ = θ₁ ⊗ e₂, ∇e₂ = -θ₁ ⊗ e₁. Along a curve γ, the covariant derivative of the unit vector cos z e₁ + sin z e₂ is therefore (z' + θ₁(γ')) times the unit vector -sin z e₁ + cos z e₂. The Sasaki metric of the unit tangent bundle, in which the horizontal part projects isometrically and the vertical part is measured by this covariant derivative, is thus θ₁² + θ₂² + (dz + θ₁)². So SL₂ℝ~ is ℝ³ with the Riemannian metric e^{-2y} dx² + dy² + (dz + e^{-y} dx)². The connection form has nonzero exterior derivative, d(e^{-y} dx) = e^{-y} dx ∧ dy, the area form of the hyperbolic plane, which is what distinguishes this twisted metric from the product metric of ℍ² × ℝ.

The orientation-preserving affine maps x ↦ eˢ x + a of the boundary line of the upper half-plane, together with the translations of the fibre, act by the isometries (x, y, z) ↦ (eˢ x + a, y + s, z + c). These form a three-dimensional group acting simply transitively, so SL₂ℝ~ is a homogeneous Riemannian manifold.

Main definitions

• TauCeti.SL2Tilde: the model geometry SL₂ℝ~, with the coordinate equivalence SL2Tilde.toProd to ℝ³ and the coordinates SL2Tilde.x, SL2Tilde.y, SL2Tilde.z.
• TauCeti.SL2Tilde.riemannianMetric: the analytic metric e^{-2y} dx² + dy² + (dz + e^{-y} dx)², which is the RiemannianBundle instance of SL2Tilde.
• TauCeti.SL2Tilde.translate a s c: the isometry (x, y, z) ↦ (eˢ x + a, y + s, z + c).

Main results

• TauCeti.SL2Tilde.inner_def: the inner product of two tangent vectors at a point with second coordinate y is e^{-2y} v₁ w₁ + v₂ w₂ + (v₃ + e^{-y} v₁) (w₃ + e^{-y} w₁).
• TauCeti.SL2Tilde.translate_mul_translate: the isometries translate a s c compose as the group Aff⁺(ℝ) × ℝ, and TauCeti.SL2Tilde.translate_inj says distinct parameters give distinct isometries.
• TauCeti.SL2Tilde.isPretransitive_isom: the isometry group of SL₂ℝ~ acts transitively on it.

References

• W. P. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Princeton (1997), §3.8 (the eight model geometries).
• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983) 401–487, §4 (the geometry SL₂ℝ~ as the unit tangent bundle of the hyperbolic plane).
• The formal structure of this file (the coordinate type synonym, its charts, the metric built with TauCeti.coerciveRiemannianMetric, the explicit isometries and the transitivity instance) follows TauCeti.Geometry.Manifold.Riemannian.Sol.Basic.

def TauCeti.SL2Tilde : Type

Thurston's model geometry SL₂ℝ~: the space ℝ³, with coordinates (x, y, z), carrying the Riemannian metric e^{-2y} dx² + dy² + (dz + e^{-y} dx)² of the universal cover of the unit tangent bundle of the hyperbolic plane.

noncomputable def TauCeti.SL2Tilde.toProd : SL2Tilde ≃ ℝ × ℝ × ℝ

The coordinates (x, y, z) of a point of SL2Tilde, as an equivalence with ℝ³.

@[instance_reducible]

noncomputable instance TauCeti.SL2Tilde.instTopologicalSpace : TopologicalSpace SL2Tilde

instance TauCeti.SL2Tilde.instT2Space : T2Space SL2Tilde

instance TauCeti.SL2Tilde.instContractibleSpace : ContractibleSpace SL2Tilde

The model SL₂ℝ~ is contractible, with its global real three-space coordinates.

@[instance_reducible]

noncomputable instance TauCeti.SL2Tilde.instChartedSpaceProdReal : ChartedSpace (ℝ × ℝ × ℝ) SL2Tilde

instance TauCeti.SL2Tilde.instIsManifoldRealProdModelWithCornersSelfTopWithTopENat : IsManifold (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) ⊤ SL2Tilde

noncomputable def TauCeti.SL2Tilde.mk (x y z : ℝ) : SL2Tilde

The point of SL2Tilde with coordinates (x, y, z).

noncomputable def TauCeti.SL2Tilde.x (p : SL2Tilde) : ℝ

The first coordinate of a point of SL2Tilde, the horizontal coordinate of its image in the upper half-plane.

noncomputable def TauCeti.SL2Tilde.y (p : SL2Tilde) : ℝ

The second coordinate of a point of SL2Tilde, the logarithm of the height of its image in the upper half-plane.

noncomputable def TauCeti.SL2Tilde.z (p : SL2Tilde) : ℝ

The third coordinate of a point of SL2Tilde, the fibre coordinate.

@[simp]

theorem TauCeti.SL2Tilde.x_mk (a b c : ℝ) : (mk a b c).x = a

@[simp]

theorem TauCeti.SL2Tilde.y_mk (a b c : ℝ) : (mk a b c).y = b

@[simp]

theorem TauCeti.SL2Tilde.z_mk (a b c : ℝ) : (mk a b c).z = c

@[simp]

theorem TauCeti.SL2Tilde.toProd_mk (a b c : ℝ) : toProd (mk a b c) = (a, b, c)

@[simp]

theorem TauCeti.SL2Tilde.x_toProd_symm (r : ℝ × ℝ × ℝ) : (toProd.symm r).x = r.1

@[simp]

theorem TauCeti.SL2Tilde.y_toProd_symm (r : ℝ × ℝ × ℝ) : (toProd.symm r).y = r.2.1

@[simp]

theorem TauCeti.SL2Tilde.z_toProd_symm (r : ℝ × ℝ × ℝ) : (toProd.symm r).z = r.2.2

@[simp]

theorem TauCeti.SL2Tilde.fst_toProd (p : SL2Tilde) : (toProd p).1 = p.x

@[simp]

theorem TauCeti.SL2Tilde.fst_snd_toProd (p : SL2Tilde) : (toProd p).2.1 = p.y

@[simp]

theorem TauCeti.SL2Tilde.snd_snd_toProd (p : SL2Tilde) : (toProd p).2.2 = p.z

theorem TauCeti.SL2Tilde.ext {p q : SL2Tilde} (hx : p.x = q.x) (hy : p.y = q.y) (hz : p.z = q.z) : p = q

A point of SL2Tilde is determined by its coordinates.

theorem TauCeti.SL2Tilde.ext_iff {p q : SL2Tilde} : p = q ↔ p.x = q.x ∧ p.y = q.y ∧ p.z = q.z

@[simp]

theorem TauCeti.SL2Tilde.mk_x_y_z (p : SL2Tilde) : mk p.x p.y p.z = p

noncomputable def TauCeti.SL2Tilde.toProdDiffeomorph : Diffeomorph (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) SL2Tilde (ℝ × ℝ × ℝ) ↑⊤

The global horocyclic coordinates as a smooth diffeomorphism.

@[simp]

theorem TauCeti.SL2Tilde.coe_toProdDiffeomorph : ⇑toProdDiffeomorph = ⇑toProd

The coordinate diffeomorphism has the existing coordinate map as its forward map.

@[simp]

theorem TauCeti.SL2Tilde.coe_toProdDiffeomorph_symm : ⇑toProdDiffeomorph.symm = ⇑toProd.symm

Inverse global coordinates agree with the inverse coordinate equivalence.

@[simp]

theorem TauCeti.SL2Tilde.mfderiv_toProd_apply (p : SL2Tilde) (v : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : (mfderiv% ⇑toProd p) v = (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v

The differential of global coordinates reads the tangent vector in the model space.

@[simp]

theorem TauCeti.SL2Tilde.tangentSpaceCastModel_mfderiv_toProd_symm (r : ℝ × ℝ × ℝ) (v : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) r) : (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) (toProd.symm r)) ((mfderiv% ⇑toProd.symm r) v) = v

The differential of inverse global coordinates retains the model vector.

The metric

noncomputable def TauCeti.SL2Tilde.riemannianMetric : Bundle.ContMDiffRiemannianMetric (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) ⊤ (ℝ × ℝ × ℝ) fun (p : SL2Tilde) => TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p

The analytic Riemannian metric e^{-2y} dx² + dy² + (dz + e^{-y} dx)² of SL₂ℝ~: the metric coerciveRiemannianMetric of ℝ × ℝ × ℝ for this field of bilinear forms, read on the type synonym SL2Tilde.

@[simp]

theorem TauCeti.SL2Tilde.riemannianMetric_inner (p : SL2Tilde) (v w : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : ((riemannianMetric.inner p) v) w = Real.exp (-2 * p.y) * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).1 * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).1 + ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).2.1 * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.1 + (((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).2.2 + Real.exp (-p.y) * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).1) * (((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.2 + Real.exp (-p.y) * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).1)

The metric of SL₂ℝ~ at p is e^{-2y} v₁ w₁ + v₂ w₂ + (v₃ + e^{-y} v₁) (w₃ + e^{-y} w₁), where y is the second coordinate of p and the tangent vectors are read in the model space ℝ³.

@[instance_reducible]

noncomputable instance TauCeti.SL2Tilde.instRiemannianBundleTangentSpaceRealProdModelWithCornersSelf : Bundle.RiemannianBundle fun (p : SL2Tilde) => TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p

SL2Tilde carries the metric e^{-2y} dx² + dy² + (dz + e^{-y} dx)².

instance TauCeti.SL2Tilde.instIsContMDiffRiemannianBundleProdRealModelWithCornersSelfTopWithTopENatTangentSpace : IsContMDiffRiemannianBundle (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) ⊤ (ℝ × ℝ × ℝ) fun (p : SL2Tilde) => TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p

The metric of SL₂ℝ~ is analytic.

instance TauCeti.SL2Tilde.instIsContinuousRiemannianBundleProdRealTangentSpaceModelWithCornersSelf : IsContinuousRiemannianBundle (ℝ × ℝ × ℝ) fun (p : SL2Tilde) => TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p

The metric of SL₂ℝ~ is continuous, as the Riemannian volume construction requires.

@[simp]

theorem TauCeti.SL2Tilde.inner_def (p : SL2Tilde) (v w : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : inner ℝ v w = Real.exp (-2 * p.y) * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).1 * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).1 + ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).2.1 * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.1 + (((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).2.2 + Real.exp (-p.y) * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).1) * (((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.2 + Real.exp (-p.y) * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).1)

The inner product of two tangent vectors v, w at a point p of SL₂ℝ~ is e^{-2y} v₁ w₁ + v₂ w₂ + (v₃ + e^{-y} v₁) (w₃ + e^{-y} w₁), where y is the second coordinate of p.

A transitive family of isometries

noncomputable def TauCeti.SL2Tilde.translate (a s c : ℝ) : Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) SL2Tilde

The isometry (x, y, z) ↦ (eˢ x + a, y + s, z + c) of SL₂ℝ~: the lift of the hyperbolic isometry w ↦ eˢ w + a of the upper half-plane, followed by the translation by c along the fibres.

@[simp]

theorem TauCeti.SL2Tilde.x_translate (a s c : ℝ) (p : SL2Tilde) : ((translate a s c) p).x = Real.exp s * p.x + a

@[simp]

theorem TauCeti.SL2Tilde.y_translate (a s c : ℝ) (p : SL2Tilde) : ((translate a s c) p).y = p.y + s

@[simp]

theorem TauCeti.SL2Tilde.z_translate (a s c : ℝ) (p : SL2Tilde) : ((translate a s c) p).z = p.z + c

@[simp]

theorem TauCeti.SL2Tilde.translate_zero : translate 0 0 0 = 1

The isometry translate 0 0 0 is the identity.

@[simp]

theorem TauCeti.SL2Tilde.translate_mul_translate (a s c a' s' c' : ℝ) : translate a s c * translate a' s' c' = translate (Real.exp s * a' + a) (s + s') (c + c')

The isometries translate a s c compose as the group Aff⁺(ℝ) × ℝ: the affine maps w ↦ eˢ w + a compose by (a, s) * (a', s') = (eˢ a' + a, s + s'), and the fibre translations add.

@[simp]

theorem TauCeti.SL2Tilde.translate_inv (a s c : ℝ) : (translate a s c)⁻¹ = translate (-(Real.exp (-s) * a)) (-s) (-c)

The inverse of translate a s c is translate (-(e^{-s} a)) (-s) (-c).

@[simp]

theorem TauCeti.SL2Tilde.translate_inj {a s c a' s' c' : ℝ} : translate a s c = translate a' s' c' ↔ a = a' ∧ s = s' ∧ c = c'

Distinct parameters give distinct isometries: translate a s c sends the point (0, 0, 0) to (a, s, c).

theorem TauCeti.SL2Tilde.translate_apply_eq (p q : SL2Tilde) : (translate (q.x - Real.exp (q.y - p.y) * p.x) (q.y - p.y) (q.z - p.z)) p = q

The isometry translate (q.x - e^{q.y - p.y} p.x) (q.y - p.y) (q.z - p.z) sends p to q.

instance TauCeti.SL2Tilde.isPretransitive_isom : MulAction.IsPretransitive (Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) SL2Tilde) SL2Tilde

The isometry group of SL₂ℝ~ acts transitively: SL₂ℝ~ is a homogeneous Riemannian manifold. Already the isometries translate a s c act transitively.