The full isometry group of Nil

The stabilizer of the identity consists exactly of the orthogonal automorphisms. The Ricci tensor singles out the central line. Naturality of the Levi-Civita connection then forces the sign on that line to equal the determinant of the horizontal orthogonal map. First-order uniqueness identifies the isometry with that automorphism. Consequently the full isometry group is Nil ⋊ O(2).

References

• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983), 401–487, Section 4 (Nil).
• J. M. Lee, Introduction to Riemannian Manifolds, second edition, Propositions 5.13 and 5.22 (connection naturality and first-order uniqueness).

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

The full stabilizer of the identity in the Riemannian isometry group of Nil is exactly the image of its orthogonal automorphisms.

theorem TauCeti.Nil.semidirectProductToIsom_surjective : Function.Surjective ⇑semidirectProductToIsom

Every Riemannian isometry of Nil is an orthogonal automorphism followed by a left translation. Equivalently, the canonical semidirect-product action is surjective.

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

The full Riemannian isometry group of Nil is Nil ⋊ O(2), with its canonical translation and orthogonal actions. This is an isomorphism of groups.

@[simp]

theorem TauCeti.Nil.semidirectProductIsomMulEquiv_apply (a : Nil ⋊[orthogonalMulAut] ↥(Matrix.orthogonalGroup (Fin 2) ℝ)) : semidirectProductIsomMulEquiv a = semidirectProductToIsom a

The full-group identification acts by the existing semidirect-product action.

@[simp]

theorem TauCeti.Nil.semidirectProductIsomMulEquiv_symm_apply_left (Φ : Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil) : (semidirectProductIsomMulEquiv.symm Φ).left = Φ 1

The translation part recovered from an arbitrary isometry is its value at the identity.

@[simp]

theorem TauCeti.Nil.orthogonalToIsom_semidirectProductIsomMulEquiv_symm_apply_right (Φ : Isom (modelWithCornersSelf ℝ (ℝ × ℝ × ℝ)) Nil) : orthogonalToIsom (semidirectProductIsomMulEquiv.symm Φ).right = (toIsom (Φ 1))⁻¹ * Φ

The orthogonal part recovered from an arbitrary isometry is obtained by removing its translation by the image of the identity.