The model geometry Nil

Nil is ℝ³, with coordinates (x, y, z), carrying the Riemannian metric dx² + dy² + (dz - x dy)². It is one of Thurston's eight model geometries of three-manifolds, the geometry of the Seifert fibred spaces with Euclidean base orbifold and nonzero Euler number, such as the circle bundles of nonzero Euler number over the torus.

Nil is also the real Heisenberg group TauCeti.HeisenbergGroup ℝ of unipotent upper triangular 3 × 3 matrices, whose product in the coordinates of the strictly upper triangle is (a, b, c) * (x, y, z) = (a + x, b + y, c + z + a y); the coordinates give a group isomorphism Nil.toHeisenberg. The one-forms dx, dy and dz - x dy are left-invariant, so the metric is left-invariant and left multiplication by any element is a Riemannian isometry. This gives an injective group homomorphism from Nil into its isometry group, and already its image acts transitively, so Nil is a homogeneous Riemannian manifold.

The orthogonal group O(2) acts on Nil by group automorphisms fixing the identity. In the coordinates (x, y, z - x y / 2), in which the product is (a, b, c) * (x, y, z) = (a + x, b + y, c + z + (a y - b x) / 2), an orthogonal matrix g acts by g on the first two coordinates and by multiplication by det g = ± 1 on the third. These automorphisms preserve dx² + dy² and multiply the form dz - x dy by det g, so they are isometries. Together with left translations they give an injective homomorphism from the semidirect product Nil ⋊ O(2) into the isometry group of Nil. This is the whole isometry group of Nil (Scott, Section 4): every isometry is of this form by TauCeti.Nil.semidirectProductToIsom_surjective, in TauCeti.Geometry.Manifold.Riemannian.Nil.Stabilizer.

Main definitions

• TauCeti.Nil: the model geometry Nil, with the coordinate equivalence Nil.toProd to ℝ³ and the coordinates Nil.x, Nil.y, Nil.z.
• TauCeti.Nil.toProdDiffeomorph: the smooth global coordinates in real three-space.
• TauCeti.Nil.instGroup: the group structure of Nil, and TauCeti.Nil.toHeisenberg, the group isomorphism with the real Heisenberg group.
• TauCeti.Nil.riemannianMetric: the analytic metric dx² + dy² + (dz - x dy)², which is the RiemannianBundle instance of Nil.
• TauCeti.Nil.toIsom: left multiplication, as a homomorphism from Nil to its isometry group.
• TauCeti.Nil.orthogonalMulAut: the action of O(2) on Nil by group automorphisms.
• TauCeti.Nil.orthogonalToIsom: the same action, as a homomorphism from O(2) to the isometry group of Nil.
• TauCeti.Nil.semidirectProductToIsom: the homomorphism from Nil ⋊ O(2) to the isometry group of Nil, in which (n, g) acts by p ↦ n * g p.

Main results

• TauCeti.Nil.inner_def: the inner product of two tangent vectors at a point with first coordinate x is v₁ w₁ + v₂ w₂ + (v₃ - x v₂) (w₃ - x w₂).
• TauCeti.Nil.toIsom_injective: distinct elements of Nil give distinct isometries.
• TauCeti.Nil.isPretransitive_isom: the isometry group of Nil acts transitively on it.
• TauCeti.Nil.range_orthogonalToIsom_le_stabilizer: the orthogonal isometries fix the identity.
• TauCeti.Nil.semidirectProductToIsom_injective: distinct elements of Nil ⋊ O(2) act by distinct isometries.

Implementation notes

Nil is a type synonym for ℝ × ℝ × ℝ rather than for HeisenbergGroup ℝ, following TauCeti.Sol: its charts are then those of the model space ℝ × ℝ × ℝ itself, and the metric is a field of bilinear forms on that space (TauCeti.coerciveRiemannianMetric).

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 (the geometry Nil, its metric and its isometry group).

def TauCeti.Nil : Type

Thurston's model geometry Nil: the space ℝ³, with coordinates (x, y, z), carrying the left-invariant Riemannian metric dx² + dy² + (dz - x dy)² of the real Heisenberg group.

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

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

@[instance_reducible]

noncomputable instance TauCeti.Nil.instTopologicalSpace : TopologicalSpace Nil

instance TauCeti.Nil.instT2Space : T2Space Nil

instance TauCeti.Nil.instContractibleSpace : ContractibleSpace Nil

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

@[instance_reducible]

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

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

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

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

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

The first coordinate of a point of Nil.

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

The second coordinate of a point of Nil.

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

The third coordinate of a point of Nil.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

A point of Nil is determined by its coordinates.

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

The group structure

@[instance_reducible]

noncomputable instance TauCeti.Nil.instMul : Mul Nil

The product (a, b, c) * (x, y, z) = (a + x, b + y, c + z + a y) of the real Heisenberg group.

@[instance_reducible]

noncomputable instance TauCeti.Nil.instOne : One Nil

@[instance_reducible]

noncomputable instance TauCeti.Nil.instInv : Inv Nil

@[simp]

theorem TauCeti.Nil.x_mul (p q : Nil) : (p * q).x = p.x + q.x

@[simp]

theorem TauCeti.Nil.y_mul (p q : Nil) : (p * q).y = p.y + q.y

@[simp]

theorem TauCeti.Nil.z_mul (p q : Nil) : (p * q).z = p.z + q.z + p.x * q.y

@[simp]

theorem TauCeti.Nil.x_one : x 1 = 0

@[simp]

theorem TauCeti.Nil.y_one : y 1 = 0

@[simp]

theorem TauCeti.Nil.z_one : z 1 = 0

@[simp]

theorem TauCeti.Nil.x_inv (p : Nil) : p⁻¹.x = -p.x

@[simp]

theorem TauCeti.Nil.y_inv (p : Nil) : p⁻¹.y = -p.y

@[simp]

theorem TauCeti.Nil.z_inv (p : Nil) : p⁻¹.z = -p.z + p.x * p.y

@[instance_reducible]

noncomputable instance TauCeti.Nil.instGroup : Group Nil

Nil is a group: the real Heisenberg group, in the coordinates of toHeisenberg.

noncomputable def TauCeti.Nil.toHeisenberg : Nil ≃* HeisenbergGroup ℝ

The coordinates of Nil identify it with the real Heisenberg group of unipotent upper triangular 3 × 3 matrices, as a group.

@[simp]

theorem TauCeti.Nil.x_toHeisenberg (p : Nil) : (toHeisenberg p).x = p.x

@[simp]

theorem TauCeti.Nil.y_toHeisenberg (p : Nil) : (toHeisenberg p).y = p.y

@[simp]

theorem TauCeti.Nil.z_toHeisenberg (p : Nil) : (toHeisenberg p).z = p.z

The metric

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

The analytic Riemannian metric dx² + dy² + (dz - x dy)² of Nil: the metric coerciveRiemannianMetric of ℝ × ℝ × ℝ for this field of bilinear forms, read on the type synonym Nil.

@[simp]

theorem TauCeti.Nil.riemannianMetric_inner (p : Nil) (v w : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : ((riemannianMetric.inner p) v) w = ((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 - p.x * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).2.1) * (((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.2 - p.x * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.1)

The metric of Nil at p is v₁ w₁ + v₂ w₂ + (v₃ - x v₂) (w₃ - x w₂), where x is the first coordinate of p and the tangent vectors are read in the model space ℝ³.

@[instance_reducible]

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

Nil carries the metric dx² + dy² + (dz - x dy)².

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

The metric of Nil is analytic.

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

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

@[simp]

theorem TauCeti.Nil.inner_def (p : Nil) (v w : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) : inner ℝ v w = ((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 - p.x * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) v).2.1) * (((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.2 - p.x * ((tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) p) w).2.1)

The inner product of two tangent vectors v, w at a point p of Nil is v₁ w₁ + v₂ w₂ + (v₃ - x v₂) (w₃ - x w₂), where x is the first coordinate of p.

Left multiplication is an isometry

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

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

@[simp]

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

The isometry toIsom p is left multiplication by p.

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

Distinct elements of Nil act by distinct isometries.

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

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

The orthogonal group fixing the identity

noncomputable def TauCeti.Nil.orthogonalMulAut : ↥(Matrix.orthogonalGroup (Fin 2) ℝ) →* MulAut Nil

The orthogonal group O(2) acts on Nil by group automorphisms: g sends (x, y, z) to (x', y', det g * (z - x y / 2) + x' y' / 2), where (x', y') = g (x, y).

In the coordinates (x, y, z - x y / 2), in which the product of Nil is (a, b, c) * (x, y, z) = (a + x, b + y, c + z + (a y - b x) / 2), the automorphism orthogonalMulAut g is g on the first two coordinates and multiplication by det g = ± 1 on the third.

@[simp]

theorem TauCeti.Nil.x_orthogonalMulAut (g : ↥(Matrix.orthogonalGroup (Fin 2) ℝ)) (p : Nil) : ((orthogonalMulAut g) p).x = ↑g 0 0 * p.x + ↑g 0 1 * p.y

@[simp]

theorem TauCeti.Nil.y_orthogonalMulAut (g : ↥(Matrix.orthogonalGroup (Fin 2) ℝ)) (p : Nil) : ((orthogonalMulAut g) p).y = ↑g 1 0 * p.x + ↑g 1 1 * p.y

@[simp]

theorem TauCeti.Nil.z_orthogonalMulAut (g : ↥(Matrix.orthogonalGroup (Fin 2) ℝ)) (p : Nil) : ((orthogonalMulAut g) p).z = (↑g).det * (p.z - p.x * p.y / 2) + (↑g 0 0 * p.x + ↑g 0 1 * p.y) * (↑g 1 0 * p.x + ↑g 1 1 * p.y) / 2

theorem TauCeti.Nil.orthogonalMulAut_injective : Function.Injective ⇑orthogonalMulAut

Distinct orthogonal matrices act by distinct automorphisms of Nil.

noncomputable def TauCeti.Nil.orthogonalToIsom : ↥(Matrix.orthogonalGroup (Fin 2) ℝ) →* Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil

The orthogonal group O(2) acts on Nil by isometries fixing the identity (TauCeti.Nil.range_orthogonalToIsom_le_stabilizer): the automorphisms orthogonalMulAut g, which rotate or reflect the (x, y)-plane and preserve the form dz - x dy up to the sign det g.

@[simp]

theorem TauCeti.Nil.orthogonalToIsom_apply (g : ↥(Matrix.orthogonalGroup (Fin 2) ℝ)) (p : Nil) : (orthogonalToIsom g) p = (orthogonalMulAut g) p

The isometry orthogonalToIsom g is the automorphism orthogonalMulAut g.

@[simp]

theorem TauCeti.Nil.tangentSpaceCastModel_mfderiv_orthogonalToIsom_one (g : ↥(Matrix.orthogonalGroup (Fin 2) ℝ)) (v : TangentSpace (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) 1) : have u := (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) 1) v; (tangentSpaceCastModel (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) ((orthogonalToIsom g) 1)) ((mfderiv% ⇑(orthogonalToIsom g) 1) v) = (↑g 0 0 * u.1 + ↑g 0 1 * u.2.1, ↑g 1 0 * u.1 + ↑g 1 1 * u.2.1, (↑g).det * u.2.2)

At the identity, an orthogonal Nil automorphism has differential g on the horizontal plane and multiplication by det g on the central line.

theorem TauCeti.Nil.orthogonalToIsom_injective : Function.Injective ⇑orthogonalToIsom

Distinct orthogonal matrices act by distinct isometries of Nil.

theorem TauCeti.Nil.range_orthogonalToIsom_le_stabilizer : orthogonalToIsom.range ≤ MulAction.stabilizer (Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil) 1

The orthogonal isometries of Nil fix its identity element.

The semidirect product Nil ⋊ O(2)

noncomputable def TauCeti.Nil.semidirectProductToIsom : Nil ⋊[orthogonalMulAut] ↥(Matrix.orthogonalGroup (Fin 2) ℝ) →* Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil

Left translations and the orthogonal isometries together give an action of the semidirect product Nil ⋊ O(2) on Nil by isometries, in which (n, g) acts by p ↦ n * g p.

@[simp]

theorem TauCeti.Nil.semidirectProductToIsom_apply (a : Nil ⋊[orthogonalMulAut] ↥(Matrix.orthogonalGroup (Fin 2) ℝ)) (p : Nil) : (semidirectProductToIsom a) p = a.left * (orthogonalMulAut a.right) p

The element (n, g) of Nil ⋊ O(2) acts on Nil by p ↦ n * g p.

theorem TauCeti.Nil.semidirectProductToIsom_injective : Function.Injective ⇑semidirectProductToIsom

Distinct elements of Nil ⋊ O(2) act by distinct isometries of Nil.