The model geometry Sol

Sol is ℝ³, with coordinates (x, y, z), carrying the Riemannian metric e^{2z} dx² + e^{-2z} dy² + dz². It is one of Thurston's eight model geometries of three-manifolds, the geometry of torus bundles over the circle with Anosov monodromy.

Sol is also the solvable Lie group ℝ² ⋊ ℝ in which ℝ acts on ℝ² by t • (x, y) = (e^{-t} x, e^{t} y): the product is (a, b, c) * (x, y, z) = (e^{-c} x + a, e^{c} y + b, c + z). The metric is left-invariant, so left multiplication by any element is a Riemannian isometry. This gives an injective group homomorphism from Sol into its isometry group, and already its image acts transitively, so Sol is a homogeneous Riemannian manifold.

Main definitions

• TauCeti.Sol: the model geometry Sol, with the coordinate equivalence Sol.toProd to ℝ³, its smooth version Sol.toProdDiffeomorph, and the coordinates Sol.x, Sol.y, Sol.z.
• TauCeti.Sol.instGroup: the group structure of Sol.
• TauCeti.Sol.riemannianMetric: the analytic metric e^{2z} dx² + e^{-2z} dy² + dz², which is the RiemannianBundle instance of Sol.
• TauCeti.Sol.toIsom: left multiplication, as a homomorphism from Sol to its isometry group.

Main results

• TauCeti.Sol.inner_def: the inner product of two tangent vectors at a point of height z is e^{2z} v₁ w₁ + e^{-2z} v₂ w₂ + v₃ w₃.
• TauCeti.Sol.toIsom_injective: distinct elements of Sol give distinct isometries.
• TauCeti.Sol.isPretransitive_isom: the isometry group of Sol 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, Section 4, pp. 470–472 (the geometry Sol and its metric).

def TauCeti.Sol : Type

Thurston's model geometry Sol: the space ℝ³, with coordinates (x, y, z), carrying the left-invariant Riemannian metric e^{2z} dx² + e^{-2z} dy² + dz² of the solvable Lie group ℝ² ⋊ ℝ.

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

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

@[instance_reducible]

noncomputable instance TauCeti.Sol.instTopologicalSpace : TopologicalSpace Sol

instance TauCeti.Sol.instT2Space : T2Space Sol

instance TauCeti.Sol.instContractibleSpace : ContractibleSpace Sol

Sol is contractible: its underlying topology is that of real three-space.

@[instance_reducible]

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

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

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

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

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

The first coordinate of a point of Sol.

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

The second coordinate of a point of Sol.

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

The third coordinate, or height, of a point of Sol.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A point of Sol is determined by its coordinates.

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

@[simp]

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

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

The global coordinate diffeomorphism of Sol with real three-space.

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

The differential of the inverse global coordinates retains the model vector.

theorem TauCeti.Sol.tangentSpaceCastModel_mfderiv_of_eq_linear (Ψ : Sol → Sol) (L : ℝ × ℝ × ℝ →L[ℝ] ℝ × ℝ × ℝ) (hΨ : ∀ (p : Sol), Ψ p = toProd.symm (L (toProd p))) (p : Sol) (u : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) (Ψ p)) ((mfderiv% Ψ p) u) = L ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u)

A map linear in Sol's global coordinates has that linear map as its differential, read in the canonical model-space tangent identifications.

The group structure

@[instance_reducible]

noncomputable instance TauCeti.Sol.instMul : Mul Sol

The product (a, b, c) * (x, y, z) = (e^{-c} x + a, e^{c} y + b, c + z) of the semidirect product ℝ² ⋊ ℝ.

@[instance_reducible]

noncomputable instance TauCeti.Sol.instOne : One Sol

@[instance_reducible]

noncomputable instance TauCeti.Sol.instInv : Inv Sol

@[simp]

theorem TauCeti.Sol.x_mul (p q : Sol) : (p * q).x = Real.exp (-p.z) * q.x + p.x

@[simp]

theorem TauCeti.Sol.y_mul (p q : Sol) : (p * q).y = Real.exp p.z * q.y + p.y

@[simp]

theorem TauCeti.Sol.z_mul (p q : Sol) : (p * q).z = p.z + q.z

@[simp]

theorem TauCeti.Sol.x_one : x 1 = 0

@[simp]

theorem TauCeti.Sol.y_one : y 1 = 0

@[simp]

theorem TauCeti.Sol.z_one : z 1 = 0

@[simp]

theorem TauCeti.Sol.x_inv (p : Sol) : p⁻¹.x = -(Real.exp p.z * p.x)

@[simp]

theorem TauCeti.Sol.y_inv (p : Sol) : p⁻¹.y = -(Real.exp (-p.z) * p.y)

@[simp]

theorem TauCeti.Sol.z_inv (p : Sol) : p⁻¹.z = -p.z

@[instance_reducible]

noncomputable instance TauCeti.Sol.instGroup : Group Sol

Sol is a group: the semidirect product ℝ² ⋊ ℝ in which t ∈ ℝ acts on ℝ² by (x, y) ↦ (e^{-t} x, e^{t} y).

The metric

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

The analytic Riemannian metric e^{2z} dx² + e^{-2z} dy² + dz² of Sol: the metric coerciveRiemannianMetric of ℝ × ℝ × ℝ for this field of bilinear forms, read on the type synonym Sol.

@[simp]

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

The metric of Sol at p is e^{2z} v₁ w₁ + e^{-2z} v₂ w₂ + v₃ w₃, where z is the height of p and the tangent vectors are read in the model space ℝ³.

@[instance_reducible]

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

Sol carries the metric e^{2z} dx² + e^{-2z} dy² + dz².

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

The metric of Sol is analytic.

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

The metric of Sol is continuous, as the Riemannian volume construction requires.

@[simp]

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

The inner product of two tangent vectors v, w at a point p of Sol is e^{2z} v₁ w₁ + e^{-2z} v₂ w₂ + v₃ w₃, where z is the height of p.

theorem TauCeti.Sol.contDiff_toProd_isometry (Φ : Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Sol) : ContDiff ℝ (↑⊤) ((⇑toProd ∘ ⇑Φ) ∘ ⇑toProd.symm)

A Sol isometry is smooth when expressed in global coordinates.

@[simp]

theorem TauCeti.Sol.fderiv_toProd_isometry_apply (Φ : Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Sol) (p : Sol) (u : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : (fderiv ℝ ((⇑toProd ∘ ⇑Φ) ∘ ⇑toProd.symm) (toProd p)) ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) u) = (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) (Φ p)) ((mfderiv% ⇑Φ p) u)

The ordinary derivative of a Sol isometry in global coordinates is its manifold derivative, read through the canonical tangent-space identifications.

Left multiplication is an isometry

noncomputable def TauCeti.Sol.toIsom : Sol →* Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Sol

Left multiplication, as a group homomorphism from Sol to its isometry group: the metric of Sol is left-invariant.

@[simp]

theorem TauCeti.Sol.toIsom_apply (p q : Sol) : (toIsom p) q = p * q

The isometry toIsom p is left multiplication by p.

theorem TauCeti.Sol.toIsom_injective : Function.Injective ⇑toIsom

Distinct elements of Sol act by distinct isometries.

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

The isometry group of Sol acts transitively: Sol is a homogeneous Riemannian manifold. This is transferred along toIsom from the transitive action of Sol on itself by left multiplication.