The action of the isometry group

The isometry group Isom(M) of a Riemannian manifold acts on M by evaluation: Φ • x = Φ x. This file records that action, its faithfulness and the regularity of each element's action, mirroring the action of the self-diffeomorphism group in TauCeti.Geometry.Diffeomorphism.Action.

A Riemannian manifold is homogeneous when its isometry group acts transitively, which is MulAction.IsPretransitive (Isom I M) M for the action recorded here. The model spaces of Thurston's eight three-dimensional geometries are homogeneous in this sense, and the model geometry is the pair (X, Isom(X)).

Main definitions

• TauCeti.RiemannianIsometry.applyMulAction: the action of Isom I M on M by evaluation.
• TauCeti.RiemannianIsometry.applyFaithfulSMul: the action is faithful.
• TauCeti.RiemannianIsometry.applyContinuousConstSMul and TauCeti.RiemannianIsometry.applyContMDiffConstSMul: each isometry acts by a smooth homeomorphism, so Isom(M) generates a structure groupoid on M and (Isom M, M)-manifolds are smooth manifolds.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176, Chapter 2 (isometries and homogeneous Riemannian manifolds).
• P. Scott, The geometries of 3-manifolds, Bull. London Math. Soc. 15 (1983) 401–487 (model geometries as homogeneous spaces of their isometry groups).

@[instance_reducible]

noncomputable instance TauCeti.RiemannianIsometry.applyMulAction {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : MulAction (Isom I M) M

The isometry group acts on M by evaluation.

@[simp]

theorem TauCeti.RiemannianIsometry.smul_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (Φ : Isom I M) (x : M) : Φ • x = Φ x

The action of the isometry group on M is evaluation.

instance TauCeti.RiemannianIsometry.applyFaithfulSMul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : FaithfulSMul (Isom I M) M

The isometry group acts faithfully on M.

instance TauCeti.RiemannianIsometry.applyContinuousConstSMul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : ContinuousConstSMul (Isom I M) M

Each isometry acts on M by a homeomorphism.

instance TauCeti.RiemannianIsometry.applyContMDiffConstSMul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : ContMDiffConstSMul I (↑⊤) (Isom I M) M

Each isometry acts on M by a smooth map.