Isometry

An isometry is a function between metric spaces that preserves the distance between every pair of points. It formalizes the idea of changing the position or representation of an object without altering its metric geometry. Terminology varies: some authors call any distance-preserving map an isometry, while others additionally require it to be surjective and call a nonsurjective distance-preserving map an isometric embedding. A bijective isometry identifies two spaces as geometrically identical with respect to their specified distances. (leanprover-community.github.io)

Definition and elementary properties

Let $(X,d_X)$ and $(Y,d_Y)$ be metric spaces. A map $f:X\to Y$ is distance-preserving if

This entry uses isometry in that sense, stating surjectivity separately when needed. Two spaces are isometric if there exists a bijective isometry between them. This is a stronger relationship than having the same topological structure. (leanprover-community.github.io)

Several consequences follow directly:

• Injectivity: if $f(x)=f(x')$, then $d_X(x,x')=0$, so $x=x'$. Thus every isometry is an injective function.
• Continuity: an isometry satisfies Lipschitz continuity with constant $1$.
• Invertibility on its image: the inverse $f^{-1}:f(X)\to X$ is also an isometry. Consequently, $f$ is a homeomorphism onto its image.
• Composition: a composition of isometries is an isometry.
• Metric invariants: distances, diameters, and the radii of balls relative to the image are preserved. (leanprover-community.github.io)

Isometries also preserve the Cauchy property of sequences. Hence a space and its isometric image are either both complete or both incomplete. If the domain is a complete metric space, its image under an isometry is a closed subset of the target metric space. (leanprover-community.github.io)

Surjectivity is not automatic. For example, the inclusion of a metric subspace into its containing space preserves distances but need not cover that space. (leanprover-community.github.io)

Isometries of Euclidean space

For Euclidean space $\mathbb R^n$, equipped with Euclidean distance, every isometry from the whole space to itself has the form

where $b\in\mathbb R^n$ and $Q$ is an orthogonal matrix:

Thus a Euclidean isometry consists of an orthogonal transformation followed by a translation. Conversely, every map of this form preserves distances. Such a map is an affine map, but it is a linear map only when $b=0$. (math.ucr.edu)

For a map fixing the origin, preservation of distances determines preservation of the inner product through

This identity explains the connection between distance preservation and orthogonal transformations. Euclidean isometries preserve angles, lines, and affine geometric relations, not merely lengths. (math.ucr.edu)

Classification in the plane

The isometries of the Euclidean plane are:

• Identity: every point remains fixed.
• Translation: every point moves by the same vector.
• Rotation: points rotate through a fixed angle about a center.
• Reflection: points are reflected across a line.
• Glide reflection: reflection across a line is combined with a nonzero translation parallel to that line.

The identity may be regarded as a translation by zero or a rotation through zero angle. These possibilities exhaust the plane’s isometries. (pi.math.cornell.edu)

Isometry groups and symmetry

The bijective isometries of a metric space $X$ form its isometry group, usually written $\operatorname{Isom}(X)$. The operation is composition; the identity map is the identity element, and every element has an isometric inverse. This brings metric geometry into group theory. (leanprover-community.github.io)

For a figure $S$ inside Euclidean space, its geometric symmetries are the ambient isometries that carry $S$ onto itself. A square, for example, has eight such plane symmetries: four rotations, including the identity, and four reflections. The distinction between an isometry of the surrounding space and a symmetry of a particular figure is essential: most plane isometries do not preserve a given square. (pi.math.cornell.edu)

Normed vector spaces and linear isometries

In a normed vector space, the distance is induced by a norm:

A linear map $T:V\to W$ is a linear isometry precisely when

Linearity then makes norm preservation equivalent to distance preservation. A general metric isometry, however, need not be linear. (leanprover-community.github.io)

The Mazur–Ulam theorem, originally proved in 1932, states that every surjective isometry between real normed vector spaces is affine. Equivalently, if $f:V\to W$ is such an isometry, then

is a real-linear isometry. In particular, a surjective isometry fixing zero is linear. Neither finite dimensionality nor completeness is required. This is a central rigidity result connecting metric geometry with the algebraic structure of normed spaces. (citeseerx.ist.psu.edu)

The theorem is specifically real-linear. For complex normed spaces, a surjective metric isometry is affine when the spaces are regarded as real spaces, but complex linearity does not follow from the theorem. (leanprover-community.github.io)

Riemannian isometries

In Riemannian geometry, a manifold carries a metric tensor assigning an inner product to each tangent space. A Riemannian isometry is a smooth diffeomorphism $f:M\to N$ satisfying

for every $p\in M$ and every $v,w\in T_pM$. In compact notation, $f^*g_N=g_M$. It preserves the lengths of curves and therefore the intrinsic distances defined by infima of curve lengths. (math.ucla.edu)

A local isometry satisfies this condition locally but need not be globally injective. Riemannian covering maps provide important examples: neighborhoods upstairs and downstairs are isometric even though distinct points upstairs may map to the same point downstairs. (math.ucla.edu)

An isometric immersion preserves the metric tensor without necessarily being a diffeomorphism or even globally injective. Its defining condition concerns tangent vectors and curve lengths; it does not assert preservation of every pairwise distance measured through the entire target manifold. Thus isometric embedding in differential geometry must be distinguished from a distance-preserving embedding of metric spaces. (math.ucla.edu)

Distinctions and mathematical uses

An isometry preserves exact distances, whereas a similarity preserves them up to a fixed positive factor:

An isometry is the special case $c=1$. In Euclidean geometry, similarities retain angles and proportions but can change size. (math.ucr.edu)

A homeomorphism preserves topological structure rather than metric values. Isometry is therefore a more restrictive form of equivalence: a bijective isometry is always a homeomorphism, but the converse requires additional conditions. (leanprover-community.github.io)

Isometries serve three closely related purposes: identifying spaces with the same metric structure, describing the symmetries of geometric objects, and constraining maps through rigidity theorems. In Euclidean geometry, distance-preserving correspondences between subsets can be extended to ambient isometries; in normed spaces, the Mazur–Ulam theorem recovers affine structure from a surjective distance-preserving map. (math.ucr.edu)

References

1. Distance Functions and Isometriespi.math.cornell.edu
2. topology.metric_space.isometry - mathlib3 docsleanprover-community.github.io
3. Isometries of figures in Euclidean spacesmath.ucr.edu
4. Symmetries and Isometriespi.math.cornell.edu
5. analysis.normed_space.mazur_ulam - mathlib3 docsleanprover-community.github.io
6. Riemannian Geometrymath.ucla.edu