Transformation geometry and the Erlangen programme

Lens

MotivationH

What stays the same?

Walk along a beach and look back at your footprints: left, right, left, right. No single rotation or reflection carries the whole trail onto itself, yet the trail clearly has a symmetry — reflect in the line you walked along, then slide forward one step. That motion is a glide reflection, and it is one of exactly four kinds of rigid motion of the plane.

Now photograph a straight railway line. In the photo the rails meet at the horizon and the equally spaced sleepers crowd together. Lengths, angles and even parallelism are destroyed. And yet something survives: a certain combination of four distances along a line, the cross-ratio, is exactly the same in the photo as on the ground. With it you can predict where the next sleeper will appear in the picture.

Which properties of a figure are "geometric"? In 1872 the 23-year-old Felix Klein gave an answer that reorganised the subject: choose a group of transformations; the geometry is the study of whatever that group leaves unchanged. Rigid motions give Euclidean geometry; the projections of a camera give projective geometry; in between lie similarity and affine geometry; and the non-Euclidean geometries fit into the same scheme. This lesson proves the classification of rigid motions, works out the invariants of the larger groups, and explains Klein's programme. It builds on Euclidean geometry and rigid motions and similarity from school, on matrices from linear algebra, and on the notion of a group from algebraic structures.

IntuitionH

Mirrors make everything

A single mirror reflects the plane. Two mirrors, one after the other, do something that is not a reflection at all: if the mirrors cross at an angle $\theta$ , the result is a rotation about the crossing point by $2\theta$ ; if they are parallel at distance $d$ , it is a translation by $2d$ perpendicular to them. A kaleidoscope works this way.

Rigid motions come in two orientations. A rotation or translation keeps a left hand a left hand (it is direct); a reflection turns it into a right hand (it is opposite). Each mirror flips orientation, so an even number of reflections is direct and an odd number is opposite. Three mirrors in general position give a glide reflection — the footprint symmetry.

Footprints: the trail is carried onto itself by a glide reflection — reflect in the dashed line, then translate along it by one step. The motion has no fixed point, and doing it twice is a translation by two steps.

The best coordinate system for all of this is the complex plane. A point is a complex number $z$ , distance is $|z - w|$ , a rotation about $0$ by $\theta$ is $z \mapsto e^{i\theta} z$ , a translation is $z \mapsto z + b$ , and complex conjugation $z \mapsto \bar z$ is the reflection in the real axis.

DefinitionsH

Definitions

Definition— isometry

An isometry of the plane is a map $f : \R^2 \to \R^2$ that preserves distances: $|f(z) - f(w)| = |z - w|$ for all $z, w$ . We identify $\R^2$ with $\C$ .

Definition— the four types

A translation by $b$ : $z \mapsto z + b$ .
A rotation about $c$ by the angle $\theta$ : $z \mapsto c + e^{i\theta}(z - c)$ .
A reflection in a line $\ell$ : each point goes to its mirror image across $\ell$ . In the line through $c$ in direction $e^{i\theta}$ , it is $z \mapsto c + e^{2i\theta}\,\overline{(z - c)}$ .
A glide reflection: a reflection in a line $\ell$ followed by a non-zero translation parallel to $\ell$ .

An isometry is direct if it preserves orientation (translations, rotations) and opposite if it reverses it (reflections, glide reflections).

Definition— similarity, affine map

A similarity multiplies all distances by a fixed $k > 0$ ; in complex form, $z \mapsto az + b$ or $z \mapsto a\bar z + b$ with $a \ne 0$ . An affine map of $\R^n$ is a map $x \mapsto Ax + b$ with $A$ an invertible $n \times n$ matrix. In homogeneous coordinates, writing the point $x$ as the column $(x, 1)$ , it is the $(n+1) \times (n+1)$ matrix $\begin{pmatrix} A & b \\ 0 & 1 \end{pmatrix}$ , and composition of affine maps is matrix multiplication.

Definition— projective line, projective plane, projective transformation

The real projective line is $\R \cup \{\infty\}$ ; its projective transformations are the maps $x \mapsto \dfrac{px + q}{rx + s}$ with $ps - qr \ne 0$ (with the conventions $-s/r \mapsto \infty$ and $\infty \mapsto p/r$ ). The real projective plane $\R P^2$ is the set of lines through the origin in $\R^3$ ; the line through $(x, y, z) \ne 0$ is written $[x : y : z]$ . Ordinary points $(x, y)$ are $[x : y : 1]$ , and the points $[x : y : 0]$ form the line at infinity, where parallel lines meet. A projective transformation of $\R P^2$ is $[v] \mapsto [Mv]$ for an invertible $3 \times 3$ matrix $M$ ; $M$ and $cM$ ( $c \ne 0$ ) give the same transformation.

Definition— cross-ratio

The cross-ratio of four distinct points $a, b, c, d$ on a line (given by coordinates) is

(a, b;\, c, d) = \frac{(c - a)(d - b)}{(c - b)(d - a)} .

Definition— geometry in the sense of Klein

A group action of a group $G$ on a set $X$ assigns to each $g \in G$ a bijection $X \to X$ , compatibly with composition. A property or quantity is an invariant of the action if it is unchanged by every $g \in G$ . In Klein's sense, a geometry is a pair $(X, G)$ ; its theorems are the statements about invariants, and two figures are equivalent (congruent, similar, …) if some $g \in G$ carries one to the other.

Worked examplesH

Examples

Example— Recognising the type from the formula

$z \mapsto -z + 4$ : a direct isometry with $a = -1 \ne 1$ . Its fixed point solves $c = -c + 4$ , so $c = 2$ ; it is the half-turn about $2$ .
$z \mapsto iz$ : the rotation about $0$ by $90^\circ$ .
$z \mapsto \bar z + 2i$ : opposite. It fixes every point of the line $\operatorname{Im} z = 1$ (if $z = x + i$ then $\bar z + 2i = x + i$ ): the reflection in that line.
$z \mapsto \bar z + 1$ : opposite with no fixed point ( $\operatorname{Re}$ would give $0 = 1$ ): the footprint glide reflection along the real axis.

Example— Two mirrors

Reflection in the real axis is $z \mapsto \bar z$ ; reflection in the line $y = x$ (direction $e^{i\pi/4}$ ) is $z \mapsto e^{i\pi/2}\bar z = i\bar z$ . First the real axis, then $y = x$ : $z \mapsto i\,\overline{\bar z} = iz$ , the rotation by $90^\circ = 2 \times 45^\circ$ . In the other order: $z \mapsto \overline{i\bar z} = -iz$ , the rotation by $-90^\circ$ . Reflections do not commute.

Example— An affine map that is not a similarity

The shear $(x, y) \mapsto (x + y, y)$ has matrix $\begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}$ . It sends the perpendicular vectors $(1, 0)$ and $(0, 1)$ to $(1, 0)$ and $(1, 1)$ , at $45^\circ$ ; it sends the unit circle to an ellipse; but it maps lines to lines, keeps parallel lines parallel, and keeps midpoints midpoints. It preserves area ( $\det = 1$ ).

Example— Perspective

A camera at the origin of $\R^3$ photographs the ground plane $z = -1$ onto the picture plane $y = 1$ : the point $(x, t, -1)$ of the ground, at distance $t$ ahead, appears at $(x/t, 1, -1/t)$ . A ground line receding at constant spacing $t = 1, 2, 3, \dots$ appears at heights $-1, -\tfrac12, -\tfrac13, \dots$ — crowding towards the horizon, which is the image of the points at infinity. In homogeneous coordinates the map is linear, so it is a projective transformation.

ProofH

The classification of plane isometries

Theorem— Lemma (three distances determine a point)

If $|w| = |z|$ , $|w - 1| = |z - 1|$ and $|w - i| = |z - i|$ , then $w = z$ .

Proof

For any $c$ , $|w - c|^2 = |w|^2 - 2\operatorname{Re}(w \bar c) + |c|^2$ . Comparing the first two hypotheses (with $c = 1$ ) gives $\operatorname{Re} w = \operatorname{Re} z$ ; comparing the first and third (with $c = i$ , so $\operatorname{Re}(w\,\bar\imath) = \operatorname{Im} w$ ) gives $\operatorname{Im} w = \operatorname{Im} z$ .

∎

Theorem— Theorem (normal form)

Every isometry $f$ of the plane has the form

f(z) = az + b \quad\text{for all } z, \qquad\text{or}\qquad f(z) = a\bar z + b \quad\text{for all } z,

with $|a| = 1$ . In particular every isometry is a bijection, and the isometries form a group.

Proof

Put $b = f(0)$ and $a = f(1) - f(0)$ ; then $|a| = |1 - 0| = 1$ . The map $g(z) = (f(z) - b)/a$ is again an isometry (dividing by $a$ does not change lengths) and fixes $0$ and $1$ . The point $g(i)$ has distance $1$ from $g(0) = 0$ and $\sqrt2$ from $g(1) = 1$ ; writing $g(i) = x + iy$ , this says $x^2 + y^2 = 1$ and $(x - 1)^2 + y^2 = 2$ , so $x = 0$ and $y = \pm1$ : $g(i) = \pm i$ .

If $g(i) = i$ , then for every $z$ the point $g(z)$ has the same distances from $0, 1, i$ as $z$ (because $g$ preserves distances and fixes these three points), so $g(z) = z$ by the lemma, and $f(z) = az + b$ . If $g(i) = -i$ , then $h(z) = \overline{g(z)}$ is an isometry fixing $0$ , $1$ and $i$ , so $h(z) = z$ , i.e. $g(z) = \bar z$ , and $f(z) = a\bar z + b$ .

Both forms are bijections, with inverses $z \mapsto \bar a(z - b)$ and $z \mapsto a\,\overline{(z - b)}$ (using $a\bar a = 1$ ), which are isometries; composites of isometries are isometries.

∎

Theorem— Theorem (the four types)

Every isometry of the plane other than the identity is exactly one of: a translation, a rotation, a reflection, a glide reflection.

Proof

Direct, $f(z) = az + b$ . If $a = 1$ , $f$ is a translation. If $a \neq 1$ , let $c = b/(1 - a)$ ; then $c = ac + b$ , so $f(z) - c = a(z - c)$ : $f$ is the rotation about $c$ by $\arg a$ .

Opposite, $g(z) = a\bar z + b$ . Since $a\bar a = 1$ ,

g(g(z)) = a\,\overline{(a\bar z + b)} + b = a\bar a z + a\bar b + b = z + s, \qquad s = a\bar b + b,

so $g \circ g$ is the translation by $s$ .

If $s = 0$ : the point $c = b/2$ is fixed, since $g(c) = \tfrac12 a\bar b + b = \tfrac12(s + b) = c$ . Then $b = c - a\bar c$ , so $g(z) = c + a\,\overline{(z - c)}$ . Writing $a = e^{2i\theta}$ , the map $w \mapsto a\bar w$ sends $re^{i\varphi}$ to $re^{i(2\theta - \varphi)}$ , the mirror image of $re^{i\varphi}$ in the line at angle $\theta$ ; so $g$ is the reflection in the line through $c$ at angle $\theta$ .

If $s \neq 0$ : $g$ has no fixed point (a fixed point $c$ would give $c = g(g(c)) = c + s$ ). Let $w = s/2$ . Then $a\bar w = \tfrac12 a(\bar a b + \bar b) = \tfrac12(b + a\bar b) = w$ , so $w$ is fixed by $u \mapsto a\bar u$ , which means $w$ is a real multiple of $e^{i\theta}$ : it points along the mirror direction. The map $h(z) = g(z) - w = a\bar z + (b - w)$ has $a\overline{(b - w)} + (b - w) = s - (a\bar w + w) = s - 2w = 0$ , so by the previous case $h$ is a reflection, in a line of direction $e^{i\theta}$ . Hence $g = (\text{translation by } w) \circ h$ is a glide reflection.

The types are distinct: translations and glide reflections have no fixed points, a rotation has exactly one, a reflection fixes a line; and a direct isometry is never opposite (if $az + b = a'\bar z + b'$ for all $z$ , then $z = 0, 1, i$ give $b = b'$ , $a = a'$ and $a = -a'$ , so $a = 0$ ).

∎

Theorem— Corollary (three mirrors suffice)

The composite of reflections in two lines meeting at angle $\theta$ is the rotation by $2\theta$ about their intersection; in two parallel lines at distance $d$ , it is a translation by $2d$ perpendicular to them. Consequently every isometry of the plane is a product of at most three reflections.

Proof

For lines through $0$ at angles $\beta$ and then $\alpha$ : $z \mapsto e^{2i\alpha}\,\overline{e^{2i\beta}\bar z} = e^{2i\alpha}e^{-2i\beta}z = e^{2i(\alpha - \beta)}z$ ; moving the intersection point to $c$ conjugates by a translation. For the vertical lines $\operatorname{Re} z = b$ , then $\operatorname{Re} z = a$ : $z \mapsto 2a - \overline{(2b - \bar z)} = z + 2(a - b)$ . Conversely, a rotation about $c$ by $\varphi$ is the product of reflections in two lines through $c$ at angle $\varphi/2$ , a translation by $t$ is the product of reflections in two lines perpendicular to $t$ at distance $|t|/2$ , and a glide reflection is a reflection followed by a translation, i.e. three reflections.

∎

The direct isometries form a subgroup of index $2$ (the kernel of "orientation", a homomorphism to $\{\pm1\}$ ). The translations form a normal subgroup: if $f(z) = az + b$ , then $f \circ (z \mapsto z + t) \circ f^{-1}$ is the translation by $at$ . In words: every observer, however they are placed and turned, agrees on which motions are translations — though not on their direction.

ProofH

Affine geometry

Theorem— Theorem (what affine maps preserve)

Let $f(x) = Ax + b$ with $A$ an invertible $n \times n$ matrix. Then

$f\big((1 - t)x + ty\big) = (1 - t)f(x) + tf(y)$ for all $x, y$ and $t \in \R$ : $f$ preserves ratios along lines, and in particular midpoints;
$f$ maps lines to lines and parallel lines to parallel lines;
$f$ multiplies all areas ( $n = 2$ ) or volumes ( $n = 3$ ) by the same factor $|\det A|$ , so it preserves ratios of areas;
for any two triangles $pqr$ and $p'q'r'$ in the plane there is exactly one affine map with $p \mapsto p'$ , $q \mapsto q'$ , $r \mapsto r'$ .

Proof

(1) $A\big((1 - t)x + ty\big) + b = (1 - t)(Ax + b) + t(Ay + b)$ by linearity of $A$ (and $(1 - t) + t = 1$ ). (2) The line $\{p + tv\}$ goes to $\{f(p) + tAv\}$ , a line since $Av \neq 0$ ; parallel lines have a common direction $v$ , and their images the common direction $Av$ . (3) This is the geometric meaning of the determinant (see linear algebra). (4) The vectors $q - p$ , $r - p$ form a basis of $\R^2$ , as do $q' - p'$ , $r' - p'$ ; so there is exactly one linear $A$ with $A(q - p) = q' - p'$ and $A(r - p) = r' - p'$ , and it is invertible. Then $b = p' - Ap$ is forced.

∎

Affine maps do not preserve lengths or angles: the shear above turns a right angle into $45^\circ$ and a circle into an ellipse. Part 4 says something striking: in affine geometry all triangles are alike. So any theorem about triangles that only mentions affine notions — lines, midpoints, parallels, ratios along lines, ratios of areas — need only be checked for one triangle.

Example— An Erlangen-style proof: the medians are concurrent

The three medians of a triangle (each joining a vertex to the midpoint of the opposite side) meet in a point that divides each of them in the ratio $2 : 1$ . Proof. Medians and the ratio $2:1$ are affine notions, so by part 4 we may assume the triangle is equilateral, with vertices $1$ , $\omega$ , $\omega^2$ where $\omega = e^{2\pi i/3}$ . The midpoint of the side opposite $1$ is $(\omega + \omega^2)/2 = -\tfrac12$ , and the point $0$ lies on the segment from $1$ to $-\tfrac12$ , dividing it as $1 : \tfrac12 = 2 : 1$ . By the rotational symmetry $z \mapsto \omega z$ , the same holds for the other two medians. Mapping back by an affine map, which preserves lines, midpoints and ratios along lines, proves the theorem for every triangle.

ProofH

Projective geometry and the cross-ratio

A projective transformation of $\R P^2$ maps lines to lines (planes through $0$ in $\R^3$ to planes through $0$ ) and preserves incidence: if three points are collinear, so are their images. Affine maps are exactly the projective transformations that map the line at infinity to itself (those whose matrix has last row $(0, 0, c)$ ). A general one can move the line at infinity into view — that is the horizon in a photograph — so parallel lines can become lines that meet, and ratios along a line are not preserved. What survives is the cross-ratio.

Theorem— Lemma (the key identity)

If $m(x) = \dfrac{px + q}{rx + s}$ and $rx + s \neq 0 \neq ry + s$ , then

m(x) - m(y) = \frac{(ps - qr)(x - y)}{(rx + s)(ry + s)} .

Proof

$m(x) - m(y) = \dfrac{(px + q)(ry + s) - (py + q)(rx + s)}{(rx + s)(ry + s)}$ , and the numerator expands to $psx + qry - qrx - psy = (ps - qr)(x - y)$ .

∎

Theorem— Theorem (invariance of the cross-ratio)

Projective transformations of the line preserve the cross-ratio: if $ps - qr \neq 0$ and $a, b, c, d$ are distinct points none of which is sent to $\infty$ , then $\big(m(a), m(b);\, m(c), m(d)\big) = (a, b;\, c, d)$ .

Proof

Substitute the key identity into each of the four differences:

\frac{(m(c) - m(a))(m(d) - m(b))}{(m(c) - m(b))(m(d) - m(a))} = \frac{(ps - qr)^2 (c - a)(d - b) \big/ \big[(rc + s)(ra + s)(rd + s)(rb + s)\big]}{(ps - qr)^2 (c - b)(d - a) \big/ \big[(rc + s)(rb + s)(rd + s)(ra + s)\big]} .

The factor $(ps - qr)^2 \neq 0$ and the four factors $(rx + s)$ appear in numerator and denominator alike, and cancel, leaving $(a, b; c, d)$ .

∎

A projective transformation of the plane restricted to a line $\ell$ is a projective transformation from $\ell$ to its image line (in a parameter $t$ along $\ell$ , the homogeneous coordinates of the image depend linearly on $t$ , so the image parameter is a ratio of two linear functions of $t$ ). So every projective transformation of the plane — every photograph of a flat scene — preserves cross-ratios of collinear points. The cross-ratio has a neat interpretation: the unique projective map with $a \mapsto 0$ , $b \mapsto \infty$ , $d \mapsto 1$ is $x \mapsto \frac{(x - a)(d - b)}{(x - b)(d - a)}$ , and it sends $c$ to $(a, b; c, d)$ . The cross-ratio is the coordinate of the fourth point in the frame made by the other three.

Example— Where is the next sleeper?

Sleepers lie on the ground at distances $0, 1, 2, 3$ along a rail; their cross-ratio is $(0, 1; 2, 3) = \frac{2 \cdot 2}{1 \cdot 3} = \frac43$ . In a photo, measured up the image of the rail, the first three appear at $0$ , $10$ and $15$ mm. Where is the fourth? Solve $(0, 10; 15, x) = \frac{15(x - 10)}{5x} = \frac43$ : $45(x - 10) = 20x$ , so $x = 18$ mm. The gaps $10, 5, 3, \dots$ shrink towards the horizon, which is at $m(\infty)$ : here the map is $m(t) = \frac{30t}{t + 2}$ , so the horizon is at $30$ mm.

Equally spaced sleepers in perspective. Their images are not equally spaced, and the rails meet at the horizon, but the cross-ratio of any four sleepers is the same on the ground and in the picture.

ExplanationH

Klein's Erlangen programme

In his inaugural programme at the University of Erlangen (1872), Klein proposed to classify geometries by their groups. The bigger the group, the fewer invariants, and the more figures count as "the same":

Geometry	Group of transformations	Typical invariants	Figures that are all equivalent
Euclidean	isometries $z \mapsto az + b$ , $a\bar z + b$ , $\lvert a\rvert = 1$	distance, angle, area	congruent figures only
Similarity	$z \mapsto az + b$ , $a\bar z + b$ , $a \ne 0$	angle, ratios of lengths	all circles; all squares; all equilateral triangles
Affine	$x \mapsto Ax + b$	parallelism, ratios along a line, ratios of areas	all triangles; all parallelograms; all ellipses
Projective	$[v] \mapsto [Mv]$	incidence (collinearity, concurrence), cross-ratio	all quadrilaterals (four points, no three collinear); all non-degenerate conics with real points

Each group contains the one above it, so each geometry's invariants include the invariants of the geometries below it: the cross-ratio is also a Euclidean invariant, and so is parallelism. A theorem of projective geometry (such as Pappus's or Desargues's theorem, which speak only of points lying on lines) is automatically a theorem of Euclidean geometry, and can be proved by first moving the figure, by a projective transformation, to a convenient position — exactly as we proved the median theorem by making the triangle equilateral.

The programme reaches further. The non-Euclidean geometries are $(X, G)$ pairs too: spherical geometry is the sphere with its rotation group $SO(3)$ , and the hyperbolic plane is the unit disc with the Möbius transformations that map the disc to itself (together with the reflections), whose invariant is the hyperbolic distance (itself built from a cross-ratio). Topology appears as the geometry of the very large group of homeomorphisms, with invariants such as connectedness and the Euler characteristic (see surfaces). An honest caveat: a general curved space has very few symmetries, so Riemannian geometry does not fit Klein's scheme directly; Élie Cartan's generalisation (Cartan geometries) models such spaces infinitesimally on Klein geometries.

Formal mathematicsF

The classification in Lean

Mathlib represents the Euclidean plane by ℂ with its norm, and has the group ℂ ≃ᵢ ℂ of isometries. The lesson's module proves the normal form from scratch, following the human proof: first the lemma that three distances determine a point, then that an isometry fixing $0$ , $1$ , $i$ is the identity, then the theorem itself, including the computation $g(i) = \pm i$ .

eq_of_three_distsLean 4Proved here from basic factsFormally verified

/-- **Three distances determine a point.** If `w` has the same distances as `z` from the three
non-collinear points `0`, `1` and `i`, then `w = z`. Squaring the distances, the differences of
the three equations are linear: they give `Re w = Re z` and `Im w = Im z`. -/
theorem eq_of_three_dists {z w : ℂ} (h0 : ‖w‖ = ‖z‖) (h1 : ‖w - 1‖ = ‖z - 1‖)
    (hI : ‖w - I‖ = ‖z - I‖) : w = z := by
  have e0 : normSq w = normSq z := by rw [← Complex.sq_norm, ← Complex.sq_norm, h0]
  have e1 : normSq (w - 1) = normSq (z - 1) := by
    rw [← Complex.sq_norm, ← Complex.sq_norm, h1]
  have eI : normSq (w - I) = normSq (z - I) := by
    rw [← Complex.sq_norm, ← Complex.sq_norm, hI]
  simp only [normSq_apply, sub_re, sub_im, one_re, one_im, I_re, I_im] at e0 e1 eI
  apply Complex.ext <;> nlinarith

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

fix_three_eq_idLean 4Proved here from basic factsFormally verified

/-- **An isometry fixing `0`, `1` and `i` is the identity.** Apply `eq_of_three_dists` to
`w = g z`: its distances from `0 = g 0`, `1 = g 1`, `i = g i` equal those of `z`. -/
theorem fix_three_eq_id (g : ℂ → ℂ) (hg : ∀ z w, ‖g z - g w‖ = ‖z - w‖) (h0 : g 0 = 0)
    (h1 : g 1 = 1) (hI : g I = I) (z : ℂ) : g z = z := by
  apply eq_of_three_dists
  · simpa [h0] using hg z 0
  · simpa [h1] using hg z 1
  · simpa [hI] using hg z I

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

isometry_normal_formLean 4Proved here from basic factsFormally verified

/-- **The normal form of a plane isometry.** Every distance-preserving map `f : ℂ → ℂ` is
`z ↦ a z + b` or `z ↦ a z̄ + b` with `|a| = 1`. Proof as in the lesson: put `b = f 0` and
`a = f 1 - f 0`; then `g z = (f z - b) / a` preserves distances and fixes `0` and `1`, so `g i`
is at distance `1` from `0` and `√2` from `1`, i.e. `g i = ± i`. If `g i = i` then `g` is the
identity; if `g i = -i` then `z ↦ conj (g z)` fixes `0`, `1`, `i` and is the identity. -/
theorem isometry_normal_form (f : ℂ → ℂ) (hf : Isometry f) :
    ∃ a b : ℂ, ‖a‖ = 1 ∧ ((∀ z, f z = a * z + b) ∨ (∀ z, f z = a * conj z + b)) := by
  have hd : ∀ z w, ‖f z - f w‖ = ‖z - w‖ := fun z w => by
    rw [← Complex.dist_eq, ← Complex.dist_eq, hf.dist_eq]
  set a := f 1 - f 0 with ha_def
  set b := f 0 with hb_def
  have ha : ‖a‖ = 1 := by simpa using hd 1 0
  have ha0 : a ≠ 0 := by
    intro h; rw [h, norm_zero] at ha; exact zero_ne_one ha
  set g : ℂ → ℂ := fun z => (f z - b) / a with hg_def
  have hfg : ∀ z, f z = a * g z + b := fun z => by
    simp only [hg_def]; field_simp; ring
  have hgd : ∀ z w, ‖g z - g w‖ = ‖z - w‖ := fun z w => by
    have : g z - g w = (f z - f w) / a := by simp only [hg_def]; field_simp; ring
    rw [this, norm_div, ha, div_one, hd]
  have hg0 : g 0 = 0 := by simp [hg_def, hb_def]
  have hg1 : g 1 = 1 := by simp only [hg_def]; rw [← ha_def]; exact div_self ha0
  -- `g i` is `i` or `-i`.
  have hgI : g I = I ∨ g I = -I := by
    have e0 : normSq (g I) = 1 := by
      have := hgd I 0; rw [hg0, sub_zero, sub_zero, norm_I] at this
      rw [← Complex.sq_norm, this, one_pow]
    have e1 : normSq (g I - 1) = 2 := by
      have := hgd I 1; rw [hg1] at this
      rw [← Complex.sq_norm, this, Complex.sq_norm]; simp [normSq_apply]; norm_num
    simp only [normSq_apply, sub_re, sub_im, one_re, one_im] at e0 e1
    have hre : (g I).re = 0 := by nlinarith
    have him : (g I).im = 1 ∨ (g I).im = -1 := by
      have : (g I).im * (g I).im = 1 := by rw [hre] at e0; linarith
      rcases mul_self_eq_one_iff.mp this with h | h
      · exact Or.inl h
      · exact Or.inr h
    rcases him with h | h
    · left; apply Complex.ext <;> simp [hre, h]
    · right; apply Complex.ext <;> simp [hre, h]
  refine ⟨a, b, ha, ?_⟩
  rcases hgI with hI | hI
  · -- `g` is the identity: a direct isometry.
    left; intro z
    rw [hfg z, fix_three_eq_id g hgd hg0 hg1 hI z]
  · -- `conj ∘ g` is the identity: an opposite isometry.
    right; intro z
    have hc := fix_three_eq_id (fun z => conj (g z))
      (fun z w => by rw [← map_sub, Complex.norm_conj, hgd]) (by simp [hg0])
      (by simp [hg1]) (by simp [hI]) z
    have : g z = conj z := by rw [← Complex.conj_conj (g z), hc]
    rw [hfg z, this]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

Mathlib reaches the same normal form by a more general route: the Mazur–Ulam theorem (a surjective isometry between real normed spaces is affine) and a description of the linear isometries of ℂ. Our proof is specific to the plane but elementary; Mathlib's works in every normed space and needs surjectivity as a hypothesis — which, as our proof shows, is automatic in the plane.

isometry_normal_form_mathlibLean 4Applies a library theoremFormally verified

/-- **The normal form, Mathlib's way.** For a surjective isometry (`ℂ ≃ᵢ ℂ`), Mathlib's
Mazur–Ulam theorem (`IsometryEquiv.toRealLinearIsometryEquiv`) makes `z ↦ f z - f 0` a real
linear isometry, and `linear_isometry_complex` says such a map is a rotation, possibly
preceded by conjugation. -/
theorem isometry_normal_form_mathlib (f : ℂ ≃ᵢ ℂ) :
    ∃ a b : ℂ, ‖a‖ = 1 ∧ ((∀ z, f z = a * z + b) ∨ (∀ z, f z = a * conj z + b)) := by
  obtain ⟨u, hu⟩ := linear_isometry_complex f.toRealLinearIsometryEquiv
  refine ⟨u, f 0, by simp, ?_⟩
  rcases hu with h | h
  · left; intro z
    have := congrArg (fun e : ℂ ≃ₗᵢ[ℝ] ℂ => e z) h
    simp only [IsometryEquiv.toRealLinearIsometryEquiv_apply, rotation_apply] at this
    rw [← this]; ring
  · right; intro z
    have := congrArg (fun e : ℂ ≃ₗᵢ[ℝ] ℂ => e z) h
    simp only [IsometryEquiv.toRealLinearIsometryEquiv_apply, LinearIsometryEquiv.trans_apply,
      rotation_apply, conjLIE_apply] at this
    rw [← this]; ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

Sorting the normal forms into the four types, step by step as in the proof:

direct_is_rotationLean 4Proved here from basic factsFormally verified

/-- **A direct isometry with `a ≠ 1` is a rotation.** The point `c = b / (1 - a)` is fixed,
and `a z + b = a (z - c) + c`: turn about `c` through the angle `arg a`. (If `a = 1` the map
is the translation `z ↦ z + b`.) -/
theorem direct_is_rotation {a b : ℂ} (ha : a ≠ 1) :
    ∃ c : ℂ, ∀ z, a * z + b = a * (z - c) + c := by
  have h : (1 : ℂ) - a ≠ 0 := sub_ne_zero.mpr (Ne.symm ha)
  refine ⟨b / (1 - a), fun z => ?_⟩
  field_simp
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

opposite_squareLean 4Proved here from basic factsFormally verified

/-- **The square of an opposite isometry is a translation.** If `g z = a z̄ + b` with
`|a| = 1`, then `g (g z) = z + (a b̄ + b)`, because `a ā = |a|² = 1`. -/
theorem opposite_square {a b : ℂ} (ha : ‖a‖ = 1) (z : ℂ) :
    a * conj (a * conj z + b) + b = z + (a * conj b + b) := by
  have h : a * conj a = 1 := by
    rw [Complex.mul_conj, Complex.normSq_eq_norm_sq, ha]; norm_num
  simp only [map_add, map_mul, Complex.conj_conj]
  linear_combination z * h

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

opposite_fixed_iffLean 4Proved here from basic factsFormally verified

/-- **When does an opposite isometry fix a point?** `g z = a z̄ + b` (with `|a| = 1`) has a
fixed point exactly when its square is the identity, i.e. `a b̄ + b = 0`. If `g c = c` then
`c = g (g c) = c + (a b̄ + b)`; conversely, if `a b̄ + b = 0` then `b / 2` is fixed. -/
theorem opposite_fixed_iff {a b : ℂ} (ha : ‖a‖ = 1) :
    (∃ c, a * conj c + b = c) ↔ a * conj b + b = 0 := by
  constructor
  · rintro ⟨c, hc⟩
    have h2 := opposite_square (b := b) ha c
    rw [hc, hc] at h2
    linear_combination -h2
  · intro h
    refine ⟨b / 2, ?_⟩
    rw [map_div₀, map_ofNat]
    linear_combination h / 2

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

opposite_with_fixed_pointLean 4Proved here from basic factsFormally verified

/-- **An opposite isometry with a fixed point `c` is a reflection** in a line through `c`:
`g z = a · conj (z - c) + c`, which is the reflection `w ↦ a w̄` in a line through `0`,
conjugated by the translation taking `0` to `c`. -/
theorem opposite_with_fixed_point {a b c : ℂ} (hc : a * conj c + b = c) (z : ℂ) :
    a * conj z + b = a * conj (z - c) + c := by
  rw [map_sub]
  linear_combination hc

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

glide_decompositionLean 4Proved here from basic factsFormally verified

/-- **Every opposite isometry is a glide reflection** (possibly with zero glide). Let
`w = (a b̄ + b) / 2`, half the translation `g ∘ g`. Then `a w̄ = w`, so `w` points along the
mirror direction, and `z ↦ a z̄ + (b - w)` has a fixed point (by `opposite_fixed_iff`), so it
is a reflection. Hence `g` = (reflection) followed by (translation by `w` parallel to the
mirror). -/
theorem glide_decomposition {a b : ℂ} (ha : ‖a‖ = 1) :
    let w := (a * conj b + b) / 2
    a * conj w = w ∧ a * conj (b - w) + (b - w) = 0 := by
  intro w
  have h : a * conj a = 1 := by
    rw [Complex.mul_conj, Complex.normSq_eq_norm_sq, ha]; norm_num
  have hw : a * conj w = w := by
    simp only [w, map_div₀, map_add, map_mul, Complex.conj_conj, map_ofNat]
    linear_combination b * h / 2
  refine ⟨hw, ?_⟩
  rw [map_sub, mul_sub, hw]
  simp only [w]
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

glide_no_fixed_pointLean 4Proved here from basic factsFormally verified

/-- **A glide reflection moves every point.** For real `t ≠ 0`, the glide reflection
`z ↦ z̄ + t` (reflect in the real axis, then slide along it) has no fixed point: comparing
real parts would give `t = 0`. -/
theorem glide_no_fixed_point {t : ℝ} (ht : t ≠ 0) (z : ℂ) : conj z + t ≠ z := by
  intro h
  have := congrArg Complex.re h
  simp at this
  exact ht this

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

Products of reflections, and the normality of translations:

reflect_reflectLean 4Proved here from basic factsFormally verified

/-- **Two reflections make a rotation.** The reflection in the line through `0` in direction
`e^{iα}` is `z ↦ e^{2iα} z̄`. Composing the reflections for `β` and then `α` gives multiplication
by `e^{2iα} · conj(e^{2iβ}) = e^{2i(α - β)}`: a rotation by twice the angle between the
mirrors. -/
theorem reflect_reflect (α β : ℝ) (z : ℂ) :
    exp (2 * α * I) * conj (exp (2 * β * I) * conj z) = exp (2 * (α - β) * I) * z := by
  have hconj : conj (exp (2 * β * I)) = exp (-(2 * β * I)) := by
    rw [← Complex.exp_conj]; congr 1; simp [Complex.conj_ofReal, map_ofNat]
  rw [map_mul, Complex.conj_conj, hconj, ← mul_assoc, ← Complex.exp_add]
  congr 2
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

parallel_reflectionsLean 4Proved here from basic factsFormally verified

/-- **Two reflections in parallel mirrors make a translation.** The reflection in the vertical
line `Re z = a` is `z ↦ 2a - z̄`. Reflecting in `Re z = b` and then in `Re z = a` translates by
`2(a - b)`, twice the distance between the mirrors. -/
theorem parallel_reflections (a b : ℝ) (z : ℂ) :
    2 * (a : ℂ) - conj (2 * (b : ℂ) - conj z) = z + 2 * ((a : ℂ) - b) := by
  simp only [map_sub, map_mul, Complex.conj_ofReal, Complex.conj_conj, map_ofNat]
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

conj_translationLean 4Proved here from basic factsFormally verified

/-- **Translations form a normal subgroup.** Conjugating the translation by `t` by a direct
similarity `f z = a z + b` (`a ≠ 0`) gives the translation by `a t`:
`f (f⁻¹ z + t) = z + a t`. So "being a translation" is a notion every observer agrees on —
in Klein's language, it is invariant. -/
theorem conj_translation {a b : ℂ} (ha : a ≠ 0) (t z : ℂ) :
    a * ((z - b) / a + t) + b = z + a * t := by
  field_simp
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

Affine maps preserve ratios along lines in any real vector space; the shear destroys a right angle:

affine_preserves_ratioLean 4Proved here from basic factsFormally verified

/-- **Affine maps preserve ratios along lines.** If `f x = A x + c` with `A` linear, then
`f` sends the point dividing the segment from `x` to `y` in the ratio `t : (1 - t)` to the point
dividing the image segment in the same ratio. (Midpoints go to midpoints; parallel lines go to
parallel lines.) -/
theorem affine_preserves_ratio {V : Type*} [AddCommGroup V] [Module ℝ V] (A : V →ₗ[ℝ] V)
    (c x y : V) (t : ℝ) :
    A ((1 - t) • x + t • y) + c = (1 - t) • (A x + c) + t • (A y + c) := by
  rw [map_add, map_smul, map_smul, smul_add, smul_add]
  module

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

shear_breaks_right_angleLean 4Proved here from basic factsFormally verified

/-- **Affine maps need not preserve angles.** The shear `(x, y) ↦ (x + y, y)` sends the
perpendicular vectors `e₁ = (1, 0)` and `e₂ = (0, 1)` to `(1, 0)` and `(1, 1)`, whose dot product
is `1 ≠ 0`. -/
theorem shear_breaks_right_angle :
    (![1, 0] : Fin 2 → ℝ) ⬝ᵥ ![0, 1] = 0 ∧
      (!![1, 1; 0, 1] *ᵥ ![1, 0] : Fin 2 → ℝ) ⬝ᵥ (!![1, 1; 0, 1] *ᵥ ![0, 1]) = 1 := by
  constructor <;> simp [dotProduct, Matrix.mulVec, Fin.sum_univ_two]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

Finally the cross-ratio, over an arbitrary field. Lean's division satisfies $x/0 = 0$ , so the theorem needs exactly the hypotheses of the human statement — $ps - qr \ne 0$ and no point sent to $\infty$ — and the proof handles the degenerate case where $(c - b)(d - a) = 0$ separately.

crossRatioLean 4Formally verified

/-- The **cross-ratio** of four points `a, b, c, d` of a line (coordinates in a field `K`):
`(a, b; c, d) = ((c - a)(d - b)) / ((c - b)(d - a))`. -/
def crossRatio {K : Type*} [Field K] (a b c d : K) : K :=
  ((c - a) * (d - b)) / ((c - b) * (d - a))

Axioms used: propext, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

mobiusLean 4Formally verified

/-- A **projective (Möbius) transformation of the line**, `x ↦ (p x + q) / (r x + s)`, given by
the matrix `!![p, q; r, s]` (invertible when `p s - q r ≠ 0`). -/
def mobius {K : Type*} [Field K] (p q r s x : K) : K := (p * x + q) / (r * x + s)

Axioms used: propext, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

mobius_subLean 4Proved here from basic factsFormally verified

/-- The key identity: `m(x) - m(y) = (p s - q r)(x - y) / ((r x + s)(r y + s))`. Differences
are multiplied by a factor that depends on each point separately, so in the cross-ratio all
the factors cancel. -/
theorem mobius_sub {K : Type*} [Field K] {p q r s x y : K} (hx : r * x + s ≠ 0)
    (hy : r * y + s ≠ 0) :
    mobius p q r s x - mobius p q r s y =
      (p * s - q * r) * (x - y) / ((r * x + s) * (r * y + s)) := by
  unfold mobius
  rw [div_sub_div _ _ hx hy]
  congr 1
  ring

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

crossRatio_mobiusLean 4Proved here from basic factsFormally verified

/-- **Projective transformations preserve the cross-ratio.** Substitute `mobius_sub` into each
of the four differences: the factor `(p s - q r)²` and the four factors `(r x + s)` appear in
numerator and denominator alike, and cancel. -/
theorem crossRatio_mobius {K : Type*} [Field K] {p q r s a b c d : K} (hdet : p * s - q * r ≠ 0)
    (ha : r * a + s ≠ 0) (hb : r * b + s ≠ 0) (hc : r * c + s ≠ 0) (hd : r * d + s ≠ 0) :
    crossRatio (mobius p q r s a) (mobius p q r s b) (mobius p q r s c) (mobius p q r s d) =
      crossRatio a b c d := by
  unfold crossRatio
  rw [mobius_sub hc ha, mobius_sub hd hb, mobius_sub hc hb, mobius_sub hd ha]
  rw [div_mul_div_comm, div_mul_div_comm, div_div_div_eq]
  by_cases h : (c - b) * (d - a) = 0
  · have h' : (p * s - q * r) * (c - b) * ((p * s - q * r) * (d - a)) = 0 := by
      rcases mul_eq_zero.mp h with h | h <;> simp [h]
    simp [h, h']
  · field_simp

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/TransformationGeometry.leanTry it in the Lean web editor

Not formalised here: the projective plane itself (Mathlib has Projectivization, which this module does not use), the restriction of a planar projective map to a line, and the Erlangen programme as such — which is a point of view rather than a theorem.

ComputationC

Composing mirrors, and Klein's table by machine

The first experiment stores isometries in the normal form of the lesson, with complex numbers made of exact fractions, and composes reflections in random lines. It classifies each product with the criteria from the proof and double-checks the answer against fixed points.

Products of reflections: the four types of plane isometryPythonExact computationExperimental evidenceComputationally tested

"""Compose reflections and watch the four types of plane isometry appear.

Plane isometries are stored in the normal form of the lesson: z -> a z + b
(direct) or z -> a conj(z) + b (opposite), with |a| = 1 and complex numbers
held as pairs of exact fractions. Reflections in random lines (rational
directions and points) are composed k at a time, for k = 1, 2, 3, 4, and every
product is classified by the lesson's criteria: a = 1 (translation or
identity), a != 1 (rotation about b / (1 - a)), and for opposite maps the
vector a conj(b) + b (zero: reflection; non-zero: glide reflection). Each
classification is double-checked against fixed points. Exact arithmetic on
random samples: evidence for the theorem, which the lesson proves.
"""

import random
from fractions import Fraction

ZERO = (Fraction(0), Fraction(0))
ONE = (Fraction(1), Fraction(0))

def cadd(z, w):
    """Sum of two complex numbers given as (re, im) pairs."""
    return (z[0] + w[0], z[1] + w[1])

def csub(z, w):
    """Difference z - w."""
    return (z[0] - w[0], z[1] - w[1])

def cmul(z, w):
    """Product z w."""
    return (z[0] * w[0] - z[1] * w[1], z[0] * w[1] + z[1] * w[0])

def cdiv(z, w):
    """Quotient z / w (w non-zero)."""
    n = w[0] * w[0] + w[1] * w[1]
    return ((z[0] * w[0] + z[1] * w[1]) / n, (z[1] * w[0] - z[0] * w[1]) / n)

def conj(z):
    """Complex conjugate."""
    return (z[0], -z[1])

def unit_from_slope(t):
    """The rational point ((1 - t^2), 2t) / (1 + t^2) on the unit circle."""
    t = Fraction(t)
    d = 1 + t * t
    return ((1 - t * t) / d, 2 * t / d)

def apply(iso, z):
    """Apply an isometry (a, b, opposite) to the point z."""
    a, b, opp = iso
    return cadd(cmul(a, conj(z) if opp else z), b)

def compose(f, g):
    """The isometry 'first g, then f' in normal form."""
    a1, b1, o1 = f
    a2, b2, o2 = g
    if not o1:
        return (cmul(a1, a2), cadd(cmul(a1, b2), b1), o2)
    return (cmul(a1, conj(a2)), cadd(cmul(a1, conj(b2)), b1), not o2)

def reflection(p, e):
    """Reflection in the line through p whose doubled direction is e = u^2.

    z -> e conj(z - p) + p, i.e. a = e and b = p - e conj(p).
    """
    return (e, csub(p, cmul(e, conj(p))), True)

def classify(iso):
    """Return 'identity', 'translation', 'rotation', 'reflection' or 'glide'."""
    a, b, opp = iso
    if not opp:
        if a == ONE:
            return "identity" if b == ZERO else "translation"
        return "rotation"
    return "reflection" if cadd(cmul(a, conj(b)), b) == ZERO else "glide"

def fixed_point_check(iso):
    """Verify the classification using fixed points; True if consistent."""
    kind = classify(iso)
    a, b, opp = iso
    if kind == "rotation":
        c = cdiv(b, csub(ONE, a))
        return apply(iso, c) == c
    if kind == "reflection":
        mid = (b[0] / 2, b[1] / 2)
        return apply(iso, mid) == mid
    if kind in ("translation", "glide"):
        z = (Fraction(3), Fraction(-7))
        shift = csub(apply(iso, apply(iso, z)), z)
        return shift != ZERO and apply(iso, z) != z
    return apply(iso, (Fraction(2), Fraction(5))) == (2, 5)

def fmt(z):
    """Format a complex number x + y i with exact fractions."""
    sign = "-" if z[1] < 0 else "+"
    return f"{z[0]} {sign} {abs(z[1])}i"

def random_reflection(rng):
    """A reflection in a line with one of a few slopes through a random point."""
    slope = rng.choice([0, 1, 2, Fraction(1, 2), -1, Fraction(-1, 3)])
    p = (Fraction(rng.randint(-5, 5)), Fraction(rng.randint(-5, 5)))
    return reflection(p, unit_from_slope(slope))

def census(rng, k, trials):
    """Classify `trials` products of k random reflections."""
    counts = {}
    consistent = True
    for _ in range(trials):
        iso = random_reflection(rng)
        for _ in range(k - 1):
            iso = compose(random_reflection(rng), iso)
        kind = classify(iso)
        counts[kind] = counts.get(kind, 0) + 1
        consistent = consistent and fixed_point_check(iso)
    return counts, consistent

def main():
    rng = random.Random(1872)
    print("Products of k random reflections (400 samples each, exact):")
    for k in range(1, 5):
        counts, ok = census(rng, k, 400)
        parts = ", ".join(f"{name} {n}" for name, n in sorted(counts.items()))
        print(f"  k = {k}: {parts}")
        print(f"         fixed-point checks consistent: {ok}")
    print()
    s1 = reflection(ZERO, ONE)
    s2 = reflection(ZERO, unit_from_slope(Fraction(1, 2)))
    rot = compose(s2, s1)
    print(f"Mirrors y = 0, then y = x/2: z -> ({fmt(rot[0])}) z")
    print("  = rotation by twice the angle between them (cos 2t = 3/5,")
    print("    sin 2t = 4/5 for tan t = 1/2)")
    v = reflection((Fraction(0), Fraction(0)), unit_from_slope(Fraction(0)))
    w = reflection((Fraction(0), Fraction(1)), unit_from_slope(Fraction(0)))
    vw = compose(w, v)
    print(f"Mirrors y = 0, then y = 1: {classify(vw)} by {fmt(vw[1])}")
    print("Footprints z -> conj(z) + 1:", classify((ONE, ONE, True)))
    print()
    print("Epistemic status: exact rational arithmetic, so every product is")
    print("classified without rounding; but these are random samples, not all")
    print("isometries. The classification theorem is proved in the lesson and")
    print("in Lean.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Even products are always direct and odd products opposite — the orientation homomorphism at work. Notice also how often each type occurs: two random mirrors almost always meet (a rotation), and three random mirrors almost always give a glide reflection, because a reflection requires the special condition $a\bar b + b = 0$ .

The second experiment builds Klein's table experimentally. For each of the four groups it applies random transformations (exact rational rotations, scalings, integer matrices) to random configurations and records which quantities survive.

Invariants of the Euclidean, similarity, affine and projective groupsPythonExact computationExperimental evidenceCounterexampleComputationally tested

"""Klein's Erlangen programme as a table: which quantities does each group keep?

Four groups of plane transformations, from small to large: Euclidean motions,
similarities, affine maps and projective maps (in homogeneous coordinates).
For random configurations of rational points the experiment applies random
members of each group, in exact fraction arithmetic, and tests whether a
quantity is unchanged: distance, angle, ratio of two lengths, parallelism,
ratio along a line, collinearity and the cross-ratio of four collinear points.
The larger the group, the fewer invariants survive. These are exact checks on
random samples: a "kept in 100 of 100" is evidence, the lesson has the proofs.
"""

import random
from fractions import Fraction

def rational_rotation(rng):
    """(c, s) with c^2 + s^2 = 1, from a random rational slope."""
    t = Fraction(rng.randint(-6, 6), rng.randint(1, 6))
    d = 1 + t * t
    return (1 - t * t) / d, 2 * t / d

def random_map(rng, group):
    """A random 3 x 3 matrix (homogeneous coordinates) from the group."""
    tx, ty = Fraction(rng.randint(-5, 5)), Fraction(rng.randint(-5, 5))
    if group in ("euclidean", "similarity"):
        c, s = rational_rotation(rng)
        k = 1 if group == "euclidean" else Fraction(rng.choice([1, 3, 4, 6]), 2)
        flip = rng.choice([1, -1])
        return [[k * c, -k * s * flip, tx], [k * s, k * c * flip, ty], [0, 0, 1]]
    while True:
        m = [[Fraction(rng.randint(-4, 4)) for _ in range(3)] for _ in range(3)]
        if group == "affine":
            m[2] = [Fraction(0), Fraction(0), Fraction(1)]
            m[0][2], m[1][2] = tx, ty
        if det3(m) != 0:
            return m

def det3(m):
    """Determinant of a 3 x 3 matrix."""
    return (m[0][0] * (m[1][1] * m[2][2] - m[1][2] * m[2][1])
            - m[0][1] * (m[1][0] * m[2][2] - m[1][2] * m[2][0])
            + m[0][2] * (m[1][0] * m[2][1] - m[1][1] * m[2][0]))

def act(m, p):
    """Image of the point p, or None if it is sent to infinity."""
    x, y = p
    u = [m[i][0] * x + m[i][1] * y + m[i][2] for i in range(3)]
    return None if u[2] == 0 else (u[0] / u[2], u[1] / u[2])

def sub(p, q):
    """The vector from q to p."""
    return (p[0] - q[0], p[1] - q[1])

def dot(u, v):
    """Dot product."""
    return u[0] * v[0] + u[1] * v[1]

def cross(u, v):
    """2D cross product; zero exactly when u and v are parallel."""
    return u[0] * v[1] - u[1] * v[0]

def param(a, b, c):
    """t with c = a + t (b - a), for collinear points a != b."""
    d = sub(b, a)
    k = 0 if d[0] != 0 else 1
    return sub(c, a)[k] / d[k]

def cross_ratio(a, b, c, d):
    """(a, b; c, d) = (c - a)(d - b) / ((c - b)(d - a)) for numbers."""
    return (c - a) * (d - b) / ((c - b) * (d - a))

def angle_key(a, o, b):
    """(sign of cos, cos^2) of the angle aob: equal keys = equal angles."""
    u, v = sub(a, o), sub(b, o)
    d = dot(u, v)
    return (d > 0) - (d < 0), d * d / (dot(u, u) * dot(v, v))

def quantities(pts):
    """The seven quantities for a configuration (a, b, c, d, e, f, g, h).

    a, b, c, d are collinear (on a line), e, f, g are a triangle, and h is
    chosen so that e h is parallel to f g.
    """
    a, b, c, d, e, f, g, h = pts
    return {
        "distance": dot(sub(e, f), sub(e, f)),
        "angle": angle_key(f, e, g),
        "length ratio": dot(sub(e, f), sub(e, f)) / dot(sub(f, g), sub(f, g)),
        "parallelism": cross(sub(h, e), sub(g, f)) == 0,
        "ratio on a line": param(a, b, c),
        "collinearity": cross(sub(b, a), sub(c, a)) == 0,
        "cross-ratio": cross_ratio(*(param(a, b, x) for x in (a, b, c, d))),
    }

def random_configuration(rng):
    """Eight rational points with the incidences described in quantities()."""
    def pt():
        return (Fraction(rng.randint(-6, 6)), Fraction(rng.randint(-6, 6)))
    a = pt()
    b = (a[0] + rng.randint(1, 3), a[1] + rng.randint(-3, 3))
    c, d = (tuple(a[i] + t * (b[i] - a[i]) for i in range(2))
            for t in (Fraction(3), Fraction(-2, 3)))
    e, f = pt(), pt()
    while f == e:
        f = pt()
    g = pt()
    while cross(sub(f, e), sub(g, e)) == 0:
        g = pt()
    h = (e[0] + 2 * (g[0] - f[0]), e[1] + 2 * (g[1] - f[1]))
    return (a, b, c, d, e, f, g, h)

def survival(rng, group, trials):
    """For each quantity, in how many trials it was preserved."""
    kept = {}
    done = 0
    while done < trials:
        pts = random_configuration(rng)
        m = random_map(rng, group)
        image = [act(m, p) for p in pts]
        if None in image or len(set(image[:4])) < 4:
            continue
        before, after = quantities(pts), quantities(image)
        for name in before:
            kept[name] = kept.get(name, 0) + (before[name] == after[name])
        done += 1
    return kept

def main():
    rng = random.Random(1872)
    groups = ["euclidean", "similarity", "affine", "projective"]
    trials = 100
    table = {g: survival(rng, g, trials) for g in groups}
    print(f"Quantities kept in {trials} random trials (exact arithmetic)")
    print(f"{'':16}" + "".join(f"{g[:10]:>11}" for g in groups))
    for name in table["euclidean"]:
        row = "".join(f"{table[g][name]:>11}" for g in groups)
        print(f"{name:16}{row}")
    print()
    print("Each larger group keeps fewer invariants: Euclidean motions keep")
    print("distance; similarities keep angles and ratios of lengths; affine")
    print("maps keep parallelism and ratios along a line; projective maps keep")
    print("only incidence (collinearity) and the cross-ratio.")
    print()
    print("Epistemic status: exact computation on random samples. A count")
    print("below 100 exhibits genuine counterexamples (the quantity is not")
    print("invariant); a count of 100 is evidence, and the lesson proves it.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

A count below $100$ is a set of genuine counterexamples; a count of $100$ is only evidence — the proofs are in the sections above.

Explore

Explore: two mirrors make a rotation

Matrix $A$ is the reflection in the $x$ -axis and $B$ the reflection in the line at $30^\circ$ . "First $A$ , then $B$ " is the matrix $BA$ ; compare it with $AB$ . Both are rotations — by $+60^\circ$ and $-60^\circ$ — and the flag shows they are direct. Change $B$ to other reflections and predict the angle before you look.

Two reflections compose to a rotation

The mirrors meet at 30°; the composite turns by 60°.

A =

Set A to:

B =

Set B to:

First A, then B: the matrix BA

BA =

0.5−0.8660.8660.5

First B, then A: the matrix AB

AB =

0.50.866−0.8660.5

image of the grid
image of the unit square
image of the flag
before the transformation
after the first step

AB ≠ BA: the order matters.

BA means “apply A first, then B”: products of transformations are read from right to left.

det(AB) = det(BA) = det A · det B = −1 · −1 = 1 The area scale factor is the same in either order.

Over the complex numbers the formula $z \mapsto (pz + q)/(rz + s)$ acts on the Riemann sphere $\C \cup \{\infty\}$ . These Möbius transformations form the group of inversive geometry: they map circles and lines to circles and lines, preserve angles, and preserve the (complex) cross-ratio. Move the probe and watch the right angle survive.

A Möbius transformation: w = (z − 1)/(z + 1)

Lines and circles go to lines and circles; small right angles stay right angles.

Function

Grid

z-plane

w-plane · w = (z − 1)/(z + 1)

horizontal lines and their images
vertical lines and their images
small cross at z₀ and its image

Drag the points, or focus one with Tab and use the arrow keys (hold Shift for small steps).

z₀ =Re+Imi

z₀: 0.5 + 0.5i
w₀ = f(z₀): −0.2 + 0.4i
f′(z₀): 0.64 − 0.48i
Local scale factor |f′(z₀)|: 0.8
Local rotation arg f′(z₀): −36.9°
Angle between the image curves: 90°

Conformal at z₀: the little right angle is turned by −36.9° and scaled by 0.8, and it stays a right angle.

A Möbius map: lines and circles go to lines and circles; the imaginary axis becomes the unit circle and the right half-plane becomes the unit disc.

Exercises

1. Transformation geometry and the Erlangen programme

Warm-upHuman

What kind of isometry is $f(z) = -z + 4$ ?

Choose one

The rotation by

180^\circ

about the point

2

A translation by

4

A reflectionThe rotation by

180^\circ

about

0

2. Transformation geometry and the Erlangen programme

Warm-upHuman

Which of these isometries of the plane move every point? (Choose all that apply.)

Choose all that apply

A translation by a non-zero vectorA glide reflectionA rotation by

90^\circ

A reflection

3. Transformation geometry and the Erlangen programme

CoreHuman

Two mirror lines cross at the point $P$ at an angle of $40^\circ$ . What is the composite of the two reflections?

Choose one

A rotation about

P

80^\circ

(clockwise or anticlockwise, depending on the order)A rotation about

P

40^\circ

A reflection in the line bisecting the two mirrorsA translation

4. Transformation geometry and the Erlangen programme

CoreHuman

The points $0, 1, 3, -3$ have cross-ratio $(0, 1;\, 3, -3) = \dfrac{(3 - 0)(-3 - 1)}{(3 - 1)(-3 - 0)} = 2$ . The projective map $m(x) = \dfrac{2x + 1}{x + 1}$ sends them to $1, \tfrac32, \tfrac74, \tfrac52$ . What is the cross-ratio $(1, \tfrac32;\, \tfrac74, \tfrac52)$ ?

5. Transformation geometry and the Erlangen programme

CoreHuman

Four equally spaced fence posts stand along a straight road. In a photograph, measured along the image of the road, the first three appear at $0$ , $10$ and $15$ mm. At how many millimetres does the fourth appear? (Use the cross-ratio: equally spaced points $0, 1, 2, 3$ have $(0, 1; 2, 3) = \tfrac43$ .)

6. Transformation geometry and the Erlangen programme

CoreHuman

Which property is preserved by every affine map $x \mapsto Ax + b$ of the plane?

Choose one

Two lines are parallelTwo lines are perpendicularA curve is a circleTwo segments have equal length

7. Transformation geometry and the Erlangen programme

StretchHuman

Claim: an isometry of the plane is determined by the images of two distinct points $p$ and $q$ . The claim is false. Which counterexample shows it?

Choose one

The identity and the reflection in the line through

p

and

q

Two rotations about

p

by different anglesTwo different translationsA rotation about

p

and a non-zero translation

8. Transformation geometry and the Erlangen programme

CoreFormal

Which Lean statement correctly formalises the glide reflection $z \mapsto \bar z + t$ (with $t$ real and non-zero) has no fixed point?

Choose one

theorem _ {t : ℝ} (ht : t ≠ 0) (z : ℂ) : conj z + t ≠ ztheorem _ {t : ℝ} (ht : t ≠ 0) : ∃ z : ℂ, conj z + t ≠ ztheorem _ {t : ℝ} (z : ℂ) : conj z + t ≠ ztheorem _ {t : ℝ} (ht : t ≠ 0) (z : ℂ) : conj (conj z + t) + t = z + 2 * t

9. Transformation geometry and the Erlangen programme

StretchComputational

An isometry is stored as (a, b, opposite) meaning $z \mapsto az + b$ (if opposite is False) or $z \mapsto a\bar z + b$ (if True), with $|a| = 1$ . Write classify(a, b, opposite) returning 'identity', 'translation', 'rotation', 'reflection' or 'glide', using the criteria from the proof. The tests use Gaussian integers, so exact comparisons with == are safe.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Every isometry fixes some point." Translations and glide reflections move every point. The correct statement is the classification: rotations fix exactly one point, reflections fix a line, the identity fixes everything, and the other two types fix nothing. (In the proof, the absence of a fixed point for an opposite isometry is detected by $g \circ g$ being a non-zero translation.)

Misconception

"Affine maps preserve angles." Only the similarities among them do. A shear turns a right angle into $45^\circ$ , and a stretch $(x, y) \mapsto (2x, y)$ turns a circle into an ellipse. Affine maps preserve parallelism and ratios along a line — which is why "midpoint" and "centroid" are affine notions but "perpendicular" and "circle" are not.

Misconception

"Two reflections make a reflection." Two reflections make a direct isometry: a rotation (by twice the angle between the mirrors) or a translation (by twice the distance between parallel mirrors). Orientation is reversed twice.

Misconception

"Projective transformations keep parallel lines parallel." Only the affine ones do. A general projective transformation moves the line at infinity, so parallel lines (which meet at infinity) can become lines meeting at a visible point — the vanishing point of a photograph.

Misconception

"A glide reflection is just a reflection followed by any translation." Every reflection followed by a translation is indeed a reflection or a glide reflection — but its mirror is usually a different line. The definition uses a translation parallel to the mirror, and with that convention the decomposition is unique: the translation part is half of $g \circ g$ .

ViewpointsH

Many ways of seeing

Geometry— Symmetry groups of patterns: 7 friezes and 17 wallpapers

The symmetries of a figure form a subgroup of the isometry group, and Klein's view turns the study of patterns into the study of these subgroups. A frieze pattern, repeating along one direction, has one of exactly 7 symmetry groups; a wallpaper pattern, repeating in two independent directions, has one of exactly 17 (E. S. Fedorov, 1891; rediscovered by George Pólya, 1924). The proof uses the classification of this lesson: a discrete group of isometries containing two independent translations can only contain rotations of order $1, 2, 3, 4$ or $6$ (the crystallographic restriction — a rotation by $\theta$ must preserve a lattice, so $2\cos\theta$ is an integer), and the possible combinations with reflections and glide reflections can be listed. Patterns from many cultures — Islamic tilings such as those of the Alhambra, Kuba textiles from Central Africa, Chinese lattice windows — have been analysed in exactly these terms. See groups.

Algebra— The structure of the Euclidean group

Algebraically, the isometry group of the plane is a semidirect product $\R^2 \rtimes O(2)$ : every isometry is uniquely "an orthogonal map $x \mapsto Qx$ , then a translation", the translations form a normal subgroup $\R^2$ , and the quotient is $O(2)$ , the group of rotations and reflections about the origin. In homogeneous coordinates this is the block form $\begin{pmatrix} Q & b \\ 0 & 1 \end{pmatrix}$ . The four types are unions of conjugacy classes: conjugating a rotation gives a rotation by the same angle (or its negative, if we conjugate by an opposite isometry) about another centre, which is why "rotation by $90^\circ$ " is a geometric notion but "rotation about the origin" is not. In $n$ dimensions the Cartan–Dieudonné theorem says that every isometry of $\R^n$ fixing the origin is a product of at most $n$ reflections in hyperplanes, generalising our "three mirrors suffice". See algebraic structures.

Topology— The shape of the group, and surfaces as quotients

The isometry group of the plane is itself a space: the normal form identifies it with two copies of $S^1 \times \R^2$ (the choices of $a$ on the unit circle and $b \in \C$ ), one for direct and one for opposite isometries. So it is a 3-dimensional manifold with two connected components — one cannot continuously deform a reflection into a rotation through isometries, which is the topological content of orientation (see matrix groups).

Groups of isometries also build spaces. Quotienting the plane by the group generated by two independent translations gives a torus; quotienting by the group generated by a glide reflection along the $x$ -axis and a translation in the $y$ -direction gives a Klein bottle, a non-orientable surface — the glide reflection is what reverses orientation as you go around. Both have Euler characteristic $0$ , as they must, being tiled by copies of a flat square; this is developed in surfaces and the Euler characteristic.

Physics— Symmetry, conservation, and the geometry of spacetime

Physics takes Klein's programme literally. By Noether's theorem, each continuous symmetry of the laws of motion gives a conserved quantity: invariance under translations gives conservation of momentum, under rotations conservation of angular momentum, under time translations conservation of energy. Special relativity is an Erlangen geometry: spacetime $\R^4$ with the Poincaré group (translations and Lorentz transformations), whose basic invariant is the interval $c^2 t^2 - x^2 - y^2 - z^2$ rather than Euclidean distance; Newtonian mechanics is the geometry of the Galilean group. In crystallography, the classification of discrete isometry groups of space gives the 230 space groups (Fedorov and Schoenflies, 1891), the 3D analogue of the 17 wallpaper groups, which organise the X-ray diffraction patterns of crystals. See relativity.

Category theory— A group is a one-object category; a geometry is an action

A group $G$ is a category with one object in which every morphism is invertible, and an action of $G$ on $X$ is a functor from that category to $\cat{Set}$ sending the object to $X$ . Klein's invariants are then the functions on $X$ (or on configurations in $X$ ) that factor through the quotient $X/G$ , and "equivalent figures" are isomorphic objects of the action groupoid, whose objects are the points of $X$ and whose morphisms $x \to y$ are the $g$ with $gx = y$ . Changing geometry by enlarging $G$ adds morphisms, so more figures become isomorphic and fewer invariants survive — Klein's table read categorically. See categories.

History & global context

History and global context

Ornament before theory. Long before any classification, artisans explored symmetry systematically: Islamic geometric tiling in Spain, North Africa, Iran and Central Asia; textile and basketry traditions in Africa, the Americas and Oceania; lattice designs in China. Dorothy Washburn and Donald Crowe's Symmetries of Culture (1988) shows how the frieze and wallpaper classifications are used by anthropologists to compare such patterns.
Cross-ratio. A lemma in Book VII of the Collection of Pappus of Alexandria (4th century CE) amounts to the invariance of the cross-ratio under projection. Girard Desargues (1639) founded projective geometry in a study of conic sections inspired by perspective drawing; Jean-Victor Poncelet's Traité des propriétés projectives des figures (1822) developed it systematically. The cross-ratio was named in the 1820s–1830s by August Ferdinand Möbius (Doppelverhältnis) and Michel Chasles (rapport anharmonique).
Affine geometry. Leonhard Euler used the word affinitas for these maps in 1748, and Möbius's Der barycentrische Calcul (1827) studied affine and projective properties with coordinates.
Motions. The theorem that every rigid motion of space is a screw motion (a rotation about an axis combined with a translation along it) is due to Giulio Mozzi (1763) and Michel Chasles (1830); its planar case is the classification in this lesson.
Groups and Klein. Felix Klein and Sophus Lie met in Berlin and worked together in Paris in 1870, studying transformation groups. Klein's Vergleichende Betrachtungen über neuere geometrische Forschungen (1872), the "Erlangen programme", proposed the classification of geometries by groups; Lie went on to create the theory of continuous groups that now bears his name.
Patterns classified. Evgraf Fedorov (1891) proved that there are 17 wallpaper groups and 230 space groups (the latter independently found by Arthur Schoenflies); George Pólya (1924) rediscovered the planar classification, and his paper inspired the artist M. C. Escher.

What stays the same?

Mirrors make everything

Definitions

Examples

The classification of plane isometries

Affine geometry

Projective geometry and the cross-ratio

Klein's Erlangen programme

The classification in Lean

Composing mirrors, and Klein's table by machine

Explore: two mirrors make a rotation

Exercises

Common misconceptions

Many ways of seeing

History and global context

Further reading