Linear isometries act on the round sphere by Riemannian isometries

A linear isometry e : E ≃ₗᵢ[ℝ] F restricts to a diffeomorphism between the unit spheres, and since the round metric is induced by the inclusion into the ambient space, whose differential e intertwines, this restriction is a Riemannian isometry for the round metrics. For F = E this gives an injective homomorphism from the linear isometry group O(E) to the isometry group of the round sphere.

The linear isometries already act transitively on the unit sphere (LinearIsometryEquiv.isPretransitive_unitSphere), so the round sphere is a homogeneous Riemannian manifold. With E = EuclideanSpace ℝ (Fin 4) this is the spherical model geometry (S³, Isom(S³)), one of Thurston's eight three-dimensional geometries.

Main definitions

• LinearIsometryEquiv.unitSphereRiemannianIsometry: the restriction of a linear isometry to the unit spheres, as a Riemannian isometry for the round metrics.
• LinearIsometryEquiv.unitSphereIsomHom: the injective homomorphism O(E) →* Isom(S(E)).

Main statements

• LinearIsometryEquiv.mvfderiv_coe_sphere_unitSphereEquiv: the differential of the restriction to the spheres, read in the ambient space, is the linear isometry itself. Use LinearIsometryEquiv.coe_unitSphereRiemannianIsometry to apply it to the Riemannian isometry.
• LinearIsometryEquiv.unitSphereIsomHom_injective: the homomorphism O(E) →* Isom(S(E)) is injective.
• TauCeti.isPretransitive_isom_sphere: the isometry group of the round sphere acts transitively on it.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapters 2 and 3 (the round sphere as a homogeneous Riemannian manifold, with isometries from O(n + 1)).
• W. P. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Princeton (1997), §3.8 (the eight model geometries).

def LinearIsometryEquiv.unitSphereRiemannianIsometry {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n k : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [Fact (Module.finrank ℝ F = k + 1)] (e : E ≃ₗᵢ[ℝ] F) : TauCeti.RiemannianIsometry (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin k))) ↑(Metric.sphere 0 1) ↑(Metric.sphere 0 1)

The restriction of a linear isometry to the unit spheres is a Riemannian isometry for the round metrics.

@[simp]

theorem LinearIsometryEquiv.unitSphereRiemannianIsometry_toDiffeomorph {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n k : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [Fact (Module.finrank ℝ F = k + 1)] (e : E ≃ₗᵢ[ℝ] F) : e.unitSphereRiemannianIsometry.toDiffeomorph = e.unitSphereDiffeomorph ↑⊤

The underlying diffeomorphism is the restriction unitSphereDiffeomorph e ∞.

@[simp]

theorem LinearIsometryEquiv.coe_unitSphereRiemannianIsometry_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n k : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [Fact (Module.finrank ℝ F = k + 1)] (e : E ≃ₗᵢ[ℝ] F) (x : ↑(Metric.sphere 0 1)) : ↑(e.unitSphereRiemannianIsometry x) = e ↑x

The isometry sends a point of the sphere to its image under the linear isometry.

theorem LinearIsometryEquiv.coe_unitSphereRiemannianIsometry {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n k : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [Fact (Module.finrank ℝ F = k + 1)] (e : E ≃ₗᵢ[ℝ] F) : ⇑e.unitSphereRiemannianIsometry = ⇑e.unitSphereEquiv

The isometry induced by e has the underlying function unitSphereEquiv e. This is not a simp lemma: the simp normal form of unitSphereRiemannianIsometry e x for F = E is e • x (unitSphereRiemannianIsometry_apply).

@[simp]

theorem LinearIsometryEquiv.unitSphereRiemannianIsometry_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (e : E ≃ₗᵢ[ℝ] E) (x : ↑(Metric.sphere 0 1)) : e.unitSphereRiemannianIsometry x = e • x

For F = E, the isometry induced by e acts on the sphere as e does.

@[simp]

theorem LinearIsometryEquiv.unitSphereRiemannianIsometry_symm {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n k : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [Fact (Module.finrank ℝ F = k + 1)] (e : E ≃ₗᵢ[ℝ] F) : e.unitSphereRiemannianIsometry.symm = e.symm.unitSphereRiemannianIsometry

The inverse of the isometry induced by e is the isometry induced by e.symm.

@[simp]

theorem LinearIsometryEquiv.unitSphereRiemannianIsometry_trans {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n k : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [Fact (Module.finrank ℝ F = k + 1)] {G : Type u_3} [NormedAddCommGroup G] [InnerProductSpace ℝ G] {l : ℕ} [Fact (Module.finrank ℝ G = l + 1)] (e : E ≃ₗᵢ[ℝ] F) (e' : F ≃ₗᵢ[ℝ] G) : e.unitSphereRiemannianIsometry.trans e'.unitSphereRiemannianIsometry = (e.trans e').unitSphereRiemannianIsometry

The composite of the isometries induced by e and e' is the isometry induced by e.trans e'.

theorem LinearIsometryEquiv.unitSphereRiemannianIsometry_injective {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup F] [InnerProductSpace ℝ F] {n k : ℕ} [Fact (Module.finrank ℝ E = n + 1)] [Fact (Module.finrank ℝ F = k + 1)] : Function.Injective unitSphereRiemannianIsometry

An ambient linear isometry is determined by its restriction as a round-sphere isometry.

def LinearIsometryEquiv.unitSphereIsomHom {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : (E ≃ₗᵢ[ℝ] E) →* TauCeti.Isom (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)

The homomorphism from the linear isometry group O(E) to the isometry group of the round unit sphere of E, restricting a linear isometry to the sphere.

@[simp]

theorem LinearIsometryEquiv.unitSphereIsomHom_apply {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (e : E ≃ₗᵢ[ℝ] E) : unitSphereIsomHom e = e.unitSphereRiemannianIsometry

The homomorphism O(E) →* Isom(S(E)) sends e to its restriction to the sphere.

theorem LinearIsometryEquiv.unitSphereIsomHom_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] (e : E ≃ₗᵢ[ℝ] E) (x : ↑(Metric.sphere 0 1)) : unitSphereIsomHom e • x = e • x

The isometry of the round sphere induced by a linear isometry acts on the sphere as the linear isometry does.

theorem LinearIsometryEquiv.toDiff_comp_unitSphereIsomHom {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : TauCeti.RiemannianIsometry.toDiff.comp unitSphereIsomHom = unitSphereDiffHom ↑⊤

Forgetting the metric, the restriction of linear isometries to the round sphere is the inclusion O(E) →* Diff(S(E)) of LinearIsometryEquiv.unitSphereDiffHom.

theorem LinearIsometryEquiv.unitSphereIsomHom_injective {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : Function.Injective ⇑unitSphereIsomHom

The homomorphism O(E) →* Isom(S(E)) is injective: a linear isometry is determined by its values on the unit sphere.

instance TauCeti.isPretransitive_isom_sphere {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} [Fact (Module.finrank ℝ E = n + 1)] : MulAction.IsPretransitive (Isom (modelWithCornersSelf ℝ (EuclideanSpace ℝ (Fin n))) ↑(Metric.sphere 0 1)) ↑(Metric.sphere 0 1)

The round sphere is a homogeneous Riemannian manifold: its isometry group acts transitively, since already the linear isometries of E do.