The isometry group of a Riemannian manifold

The smooth Riemannian self-isometries of M form a group Isom(M) under composition. This file defines TauCeti.Isom I M as RiemannianIsometry I I M M and equips it with that group structure, using the convention of Equiv.Perm and of the self-diffeomorphism group: Φ * Ψ = Ψ.trans Φ acts as Φ ∘ Ψ. Forgetting the metric condition is an injective group homomorphism to the diffeomorphism group. The action of Isom(M) on M is in TauCeti.Geometry.Manifold.Riemannian.Isometry.Action.

Main definitions

• TauCeti.Isom I M: the isometry group of the Riemannian manifold M.
• TauCeti.RiemannianIsometry.instGroup: the group of Riemannian self-isometries.
• TauCeti.RiemannianIsometry.toDiff: the injective homomorphism to the diffeomorphism group.

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).

@[reducible, inline]

abbrev TauCeti.Isom {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] : Type u_3

Isom I M is the isometry group Isom(M) of the Riemannian manifold M modelled on I: its smooth Riemannian self-isometries under composition.

@[instance_reducible]

noncomputable instance TauCeti.RiemannianIsometry.instOne {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] : One (Isom I M)

The identity isometry is the unit of the isometry group.

@[instance_reducible]

noncomputable instance TauCeti.RiemannianIsometry.instMul {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] : Mul (Isom I M)

Multiplication of isometries is composition: Φ * Ψ follows Ψ then Φ, so that it acts as Φ ∘ Ψ, matching the Equiv.Perm convention.

@[instance_reducible]

noncomputable instance TauCeti.RiemannianIsometry.instInv {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] : Inv (Isom I M)

The inverse in the isometry group is the inverse isometry.

@[instance_reducible]

noncomputable instance TauCeti.RiemannianIsometry.instGroup {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] : Group (Isom I M)

The smooth Riemannian self-isometries of M form a group under composition, with multiplication acting as function composition.

theorem TauCeti.RiemannianIsometry.one_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] : 1 = RiemannianIsometry.refl I M

The unit of the isometry group is the identity isometry.

theorem TauCeti.RiemannianIsometry.mul_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) : Φ * Ψ = RiemannianIsometry.trans Ψ Φ

Multiplication in the isometry group is RiemannianIsometry.trans in composition order.

theorem TauCeti.RiemannianIsometry.inv_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) : Φ⁻¹ = RiemannianIsometry.symm Φ

Inversion in the isometry group is the inverse isometry.

@[simp]

theorem TauCeti.RiemannianIsometry.coe_one {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] : ⇑1 = id

The unit isometry coerces to the identity function.

@[simp]

theorem TauCeti.RiemannianIsometry.coe_mul {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) : ⇑(Φ * Ψ) = ⇑Φ ∘ ⇑Ψ

Multiplication of isometries coerces to function composition.

@[simp]

theorem TauCeti.RiemannianIsometry.coe_inv {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) : ⇑Φ⁻¹ = ⇑(RiemannianIsometry.symm Φ)

The inverse in the isometry group coerces to the inverse isometry.

@[simp]

theorem TauCeti.RiemannianIsometry.mul_apply {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)

Multiplication of isometries applies the right factor, then the left.

@[simp]

theorem TauCeti.RiemannianIsometry.one_apply {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] (x : M) : 1 x = x

The unit isometry fixes every point.

@[simp]

theorem TauCeti.RiemannianIsometry.inv_apply {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 = (RiemannianIsometry.symm Φ) x

The inverse in the isometry group acts as the inverse isometry.

@[simp]

theorem TauCeti.RiemannianIsometry.toDiffeomorph_one {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] : toDiffeomorph 1 = 1

The underlying diffeomorphism of the unit isometry is the unit diffeomorphism.

@[simp]

theorem TauCeti.RiemannianIsometry.toDiffeomorph_mul {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) : (Φ * Ψ).toDiffeomorph = Φ.toDiffeomorph * Ψ.toDiffeomorph

The underlying diffeomorphism preserves multiplication of isometries.

@[simp]

theorem TauCeti.RiemannianIsometry.toDiffeomorph_inv {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) : Φ⁻¹.toDiffeomorph = Φ.toDiffeomorph⁻¹

The underlying diffeomorphism preserves inversion of isometries.

def TauCeti.RiemannianIsometry.toDiff {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 →* Diff I M ↑⊤

The forgetful group homomorphism from the isometry group to the diffeomorphism group, sending an isometry to its underlying smooth diffeomorphism.

@[simp]

theorem TauCeti.RiemannianIsometry.toDiff_apply {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) : toDiff Φ = Φ.toDiffeomorph

The forgetful homomorphism to the diffeomorphism group forgets the metric condition.

theorem TauCeti.RiemannianIsometry.toDiff_injective {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] : Function.Injective ⇑toDiff

The forgetful homomorphism to the diffeomorphism group is injective, so the isometry group is a subgroup of the diffeomorphism group.