Distance-preserving maps of a disc about the origin

Mathlib's Mathlib/Analysis/Complex/Isometry.lean classifies the linear isometries of the plane: linear_isometry_complex says that every f : ℂ ≃ₗᵢ[ℝ] ℂ is rotation a or conjLIE.trans (rotation a). That statement asks for a map defined on all of ℂ, and asks it to be both ℝ-linear and surjective. This file drops all three hypotheses at once: for a map g defined on a disc ball 0 r about the origin, fixing the origin and merely preserving distances between points of that disc, the restriction of g to that disc is the restriction of z ↦ u * z, or of z ↦ u * conj z, for a single unit u. The alternative is not chosen point by point — that single choice is the content of the theorem.

Linearity and surjectivity are dropped as hypotheses; they are not put back as conclusions. Nothing is claimed about g off the disc, so g itself need be neither linear nor surjective, and the theorem says only that on ball 0 r it agrees with a map that is.

The proof is the classical orthonormal-frame argument. TauCeti/Analysis/InnerProductSpace/ Isometry.lean turns the distance hypothesis into preservation of the real inner product that ℂ carries (Complex.inner : ⟪w, z⟫_ℝ = (z * conj w).re). The two probe points r / 2 and I * r / 2 of the disc then have images whose doublings-by-2 / r are an orthonormal pair e, f, and ⟪e, g z⟫_ℝ, ⟪f, g z⟫_ℝ read off the real and imaginary parts of z. Orthogonality of two unit complex numbers means a quarter turn, f = e * I or f = -(e * I) (TauCeti.eq_mul_I_or_eq_neg_mul_I_of_real_inner_eq_zero, where Mathlib's two-dimensional orientation API enters, its quarter turn Complex.rightAngleRotation being multiplication by I), and pairing g z against e and against e * I recovers g z as e * z in the first case and as e * conj z in the second — the alternative being fixed once, by f, and not per point.

That argument is adapted from the proof of TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj and its private scaffolding (real_inner_eq, im_conj_mul, exists_orthonormal_pair_real_inner_map_eq, eq_mul_I_or_eq_neg_mul_I) in TauCeti/Analysis/Complex/Conformal/Poincare/Isometry/Classification.lean, as merged in TauCeti#1502; here the unit radius is relaxed to an arbitrary r > 0 and the hyperbolic hypothesis is replaced by the Euclidean one the argument actually used.

Main results

• TauCeti.eq_mul_I_or_eq_neg_mul_I_of_real_inner_eq_zero — two orthogonal unit vectors of the Euclidean plane ℂ differ by the quarter turn z ↦ z * I.
• TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj_of_dist_map_eq — the classification: a distance-preserving self-map of ball 0 r fixing 0 is a rotation or a rotated conjugation there, and TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj_iff — the converse packaged with it, the rotations and rotated conjugations being exactly the maps in question.

The consumer is TauCeti/Analysis/Complex/Conformal/Poincare/Isometry/Classification.lean, which classifies the isometries of the Poincaré disc: an isometry of the hyperbolic metric fixing the origin is a Euclidean isometry of the disc fixing the origin, so the hyperbolic classification is this Euclidean one together with the Moebius factor that moves the base point. This supports the hyperbolic-metric layer L2 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md) without adding to it.

Orthogonality in the Euclidean plane

theorem TauCeti.eq_mul_I_or_eq_neg_mul_I_of_real_inner_eq_zero {z w : ℂ} (hz : ‖z‖ = 1) (hw : ‖w‖ = 1) (h : inner ℝ z w = 0) : w = z * Complex.I ∨ w = -(z * Complex.I)

Two orthogonal unit vectors of the plane differ by a quarter turn. For unit complex numbers z and w with ⟪z, w⟫_ℝ = 0, either w = z * I or w = -(z * I).

The plane being two-dimensional, the orthogonal complement of a nonzero z is the real line through the quarter turn z * I; that is Mathlib's Submodule.mem_span_singleton_of_inner_eq_zero_of_inner_eq_zero, the quarter turn being Complex.orientation.rightAngleRotation (Complex.rightAngleRotation). Being a unit vector, the real multiple it produces is 1 or -1.

The classification

theorem TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj_of_dist_map_eq {r : ℝ} {g : ℂ → ℂ} (hr : 0 < r) (h0 : g 0 = 0) (hg : ∀ z ∈ Metric.ball 0 r, ∀ w ∈ Metric.ball 0 r, dist (g z) (g w) = dist z w) : ∃ (u : ℂ), ‖u‖ = 1 ∧ (Set.EqOn g (fun (z : ℂ) => u * z) (Metric.ball 0 r) ∨ Set.EqOn g (fun (z : ℂ) => u * (starRingEnd ℂ) z) (Metric.ball 0 r))

Distance-preserving self-maps of a disc fixing its centre are rotations and rotated conjugations. A map of ball 0 r that fixes 0 and preserves the distance between any two of its points agrees on that disc with z ↦ u * z, or with z ↦ u * conj z, for a single unit u.

No linearity and no surjectivity are assumed, and the map is only constrained on the disc; this is what separates the statement from Mathlib's linear_isometry_complex, which classifies the elements of ℂ ≃ₗᵢ[ℝ] ℂ. The single u, and the single choice between the two alternatives, are the content: a priori each point of the disc could be reflected or not independently.

theorem TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj_iff {r : ℝ} {g : ℂ → ℂ} (hr : 0 < r) : (g 0 = 0 ∧ ∀ z ∈ Metric.ball 0 r, ∀ w ∈ Metric.ball 0 r, dist (g z) (g w) = dist z w) ↔ ∃ (u : ℂ), ‖u‖ = 1 ∧ (Set.EqOn g (fun (z : ℂ) => u * z) (Metric.ball 0 r) ∨ Set.EqOn g (fun (z : ℂ) => u * (starRingEnd ℂ) z) (Metric.ball 0 r))

The distance-preserving self-maps of a disc fixing its centre are exactly the rotations and the rotated conjugations. The converse half is immediate — multiplication by a unit and conjugation are both isometries of ℂ, and both fix 0 — so TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj_of_dist_map_eq closes the description into an equivalence.