The isometry group of Euclidean space #
A real inner product space F is a Riemannian manifold for the flat metric given by the inner
product on each tangent space, and its Riemannian distance is the norm distance. This file
identifies its Riemannian isometries with its affine isometries:
- an affine isometry
F ≃ᵃⁱ[ℝ] Gis smooth, and its differential at every point is its linear part, which preserves inner products, so it is a Riemannian isometry; - conversely, a Riemannian isometry preserves the Riemannian distance, which is the norm
distance, so it is affine by the Mazur–Ulam theorem
(
IsometryEquiv.toRealAffineIsometryEquiv).
For self-maps this is an isomorphism between the Riemannian isometry group Isom 𝓘(ℝ, F) F and
the affine isometry group F ≃ᵃⁱ[ℝ] F of rigid motions. Translations act transitively, so
Euclidean space is a homogeneous Riemannian manifold, and the isotropy group of the origin is the
orthogonal group F ≃ₗᵢ[ℝ] F. With F = EuclideanSpace ℝ (Fin 3) this is the Euclidean model
geometry (𝔼³, Isom(𝔼³)), one of Thurston's eight three-dimensional geometries.
Main definitions #
AffineIsometryEquiv.toRiemannianIsometry: an affine isometry as a Riemannian isometry.TauCeti.RiemannianIsometry.toAffineIsometryEquiv: a Riemannian isometry of real inner product spaces as an affine isometry.TauCeti.RiemannianIsometry.affineIsometryMulEquiv: the isomorphism between the Riemannian isometry group of a real inner product space and its affine isometry group.TauCeti.RiemannianIsometry.stabilizerZeroMulEquiv: the isomorphism between the isotropy group of the origin and the linear isometry group.TauCeti.RiemannianIsometry.semidirectProductMulEquiv: the Euclidean group as the semidirect product of translations and orthogonal transformations.
Main results #
TauCeti.RiemannianIsometry.isPretransitive_innerProductSpace: the isometry group of a real inner product space acts transitively on it.
References #
- J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176, Chapters 2 and 3 (homogeneous Riemannian manifolds, and Euclidean space with its group of rigid motions).
- W. P. Thurston, Three-Dimensional Geometry and Topology, Vol. 1, Princeton (1997), §3.8 (the eight model geometries).
An affine isometry between real inner product spaces is a smooth Riemannian isometry for their flat metrics: its differential at every point is its linear part, a linear isometry.
Instances For
The Riemannian isometry of an affine isometry has the same underlying function.
A Riemannian isometry between real inner product spaces is an affine isometry: it preserves the Riemannian distance, which is the norm distance, so it is affine by the Mazur–Ulam theorem.
Instances For
The affine isometry of a Riemannian isometry has the same underlying function.
Viewing an affine isometry as a Riemannian isometry and back gives the original map.
A Riemannian isometry of real inner product spaces is determined by its affine isometry.
The Riemannian isometry group of a real inner product space is its affine isometry group, the group of rigid motions.
Instances For
The isomorphism of isometry groups sends a Riemannian isometry to its affine isometry.
The inverse isomorphism of isometry groups views an affine isometry as a Riemannian one.
The full Riemannian isometry group of a real inner product space is the semidirect
product of its translations and its orthogonal group. For F = EuclideanSpace ℝ (Fin n)
this is the Euclidean group decomposition E(n) = ℝⁿ ⋊ O(n).
Instances For
The translation coordinate of a Euclidean Riemannian isometry is its image of zero.
The orthogonal coordinate is the linear part of the canonical affine isometry.
The Riemannian isometry corresponding to (v, L) acts as x ↦ v + L x.
The isotropy group of the origin in the isometry group of a real inner product space is its
linear isometry group, the orthogonal group O(F): an isometry fixing the origin is linear by the
Mazur–Ulam theorem.
Instances For
The linear isometry of an isometry fixing the origin has the same underlying function.
A linear isometry, viewed as an isometry fixing the origin, has the same underlying function.
Euclidean space is a homogeneous Riemannian manifold: translations are isometries, so the isometry group of a real inner product space acts transitively on it.