The isometries of the Poincaré disc are the disc automorphisms and their conjugates

The two objects layer L2 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md) asks for — "the hyperbolic / Poincaré metric on 𝔻" and "the disc automorphism group Aut(𝔻) = {e^{iθ}(z−a)/(1−āz)}" — are already on main, and Conformal/Poincare/MetricSpace.lean records the one implication relating them: every standard automorphism is a Poincaré isometry. This file proves the converse, which is what makes Aut(𝔻) the right group for that metric:

a map of the open unit disc into itself that preserves the hyperbolic distance is z ↦ u * (z - b) / (1 - conj b * z) or z ↦ u * (conj z - b) / (1 - conj b * conj z), for a single u on the unit circle and a single b in the disc.

So the isometry group of the Poincaré disc is Aut(𝔻) together with its coset under conjugation, the second alternative being the orientation-reversing half. Two hypotheses one might expect are absent, and their absence is part of the statement: no holomorphy, and no surjectivity. Dropping holomorphy is what separates this from the Schwarz--Pick rigidity of Conformal/SchwarzPick/Rigidity.lean, whose exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv_of_hyperbolicDist_map_eq assumes DifferentiableOn ℂ and so can only ever reach the holomorphic half of the group; here conj is admitted, and it is genuinely reached, conjugation being a hyperbolic isometry. Dropping surjectivity is a conclusion rather than an omission: an isometric self-embedding of the Poincaré disc is automatically onto (TauCeti.bijOn_ball_of_hyperbolicDist_map_eq, TauCeti.PoincareDisc.bijective_of_isometry), the hyperbolic plane admitting no proper isometric copy of itself.

The proof

Everything is elementary once the problem is moved to the origin. Post-composing with the Moebius factor that sends g 0 to 0 — a hyperbolic isometry by TauCeti.pseudoHyperbolicExpr_unitDiscMoebiusFormula_of_norm_lt_one — reduces to an isometry h fixing 0, and there the hyperbolic metric collapses to the Euclidean one:

• ‖h z‖ = ‖z‖, because pseudoHyperbolicExpr z 0 is ‖z‖;
• ‖h z - h w‖ = ‖z - w‖ (TauCeti.norm_sub_eq_of_pseudoHyperbolicExpr_eq). This is the one computation with content. Writing A = ‖z - w‖ ^ 2 and B = ‖1 - conj w * z‖ ^ 2, the Poincaré defect identity TauCeti.norm_sq_one_sub_conj_mul_sub_norm_sq_sub says B = A + c with c = (1 - ‖z‖ ^ 2) * (1 - ‖w‖ ^ 2); since c depends only on the two norms, which h preserves, equality of the quotients A / B forces equality of the numerators.

That leaves a Euclidean isometry of the disc fixing 0, and nothing hyperbolic remains in the problem: TauCeti/Analysis/Complex/Isometry.lean classifies those maps as the rotations and the rotated conjugations, so h z = u * z or h z = u * conj z for a single unit u — with the alternative fixed once and for all, not chosen per point. Undoing the Moebius factor turns u into the rotation and g 0 into the centre b, by an explicit algebraic identity rather than by an appeal to the group law. The polarisation step of that Euclidean classification is also recorded here in hyperbolic language, as TauCeti.real_inner_map_map_of_pseudoHyperbolicExpr_map_eq; the inner product in question is Mathlib's own, ℂ carrying the InnerProductSpace ℝ ℂ instance with ⟪w, z⟫_ℝ = (z * conj w).re (Complex.inner), so nothing about the Euclidean plane is re-encoded here.

Main results

• TauCeti.real_inner_map_map_of_pseudoHyperbolicExpr_map_eq — an isometry fixing the origin preserves the real inner product.
• TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj — the classification for an isometry fixing the origin: it is a rotation or a rotated conjugation.
• TauCeti.exists_eqOn_ball_unitDiscStandardAutomorphismFormula_or_conj_of_hyperbolicDist_map_eq and its pseudo-hyperbolic companion — the classification.
• TauCeti.PoincareDisc.exists_eq_unitDiscStandardAutomorphismIsometryEquiv_or_comp_star — the same statement for the bundled metric space PoincareDisc and the bundled automorphisms PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv; its Isometry-iff form PoincareDisc.isometry_iff_exists_eq_unitDiscStandardAutomorphismIsometryEquiv_or_comp_star describes the isometry group itself, the conjugation entering its second alternative being bundled as PoincareDisc.starIsometryEquiv in Isometry/Equiv.lean.
• TauCeti.bijOn_ball_of_forall_pseudoHyperbolicExpr_map_eq, TauCeti.bijOn_ball_of_hyperbolicDist_map_eq and TauCeti.PoincareDisc.bijective_of_isometry — an isometric self-embedding of the Poincaré disc is a bijection.

Coordination with upstream Mathlib

Mathlib has no Poincaré metric on the disc at all — its hyperbolic material lives on UpperHalfPlane — so it has no classification of the isometries of one, and this file is new Lean formalization rather than a temporary shim. The in-progress human-curated Riemann-mapping effort mathlib4#33505, together with the preceding Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean, stops at the mapping theorem and contains nothing of this; should a human-curated Poincaré metric and its isometry group land upstream, this file is to be refactored onto it.

References

• L. V. Ahlfors, Conformal Invariants: Topics in Geometric Function Theory, Ch. 1.
• A. F. Beardon, The Geometry of Discrete Groups, §7.4 (the isometries of the hyperbolic plane).

Isometries of the Poincaré disc that fix the origin

theorem TauCeti.norm_map_of_pseudoHyperbolicExpr_map_eq {g : ℂ → ℂ} (hg : ∀ z ∈ Metric.ball 0 1, ∀ w ∈ Metric.ball 0 1, pseudoHyperbolicExpr (g z) (g w) = pseudoHyperbolicExpr z w) (h0 : g 0 = 0) {z : ℂ} (hz : z ∈ Metric.ball 0 1) : ‖g z‖ = ‖z‖

An isometry fixing the origin preserves norms. A self-map of the open unit disc that preserves the pseudo-hyperbolic expression and fixes 0 preserves the norm.

theorem TauCeti.norm_sub_map_of_pseudoHyperbolicExpr_map_eq {g : ℂ → ℂ} (hg : ∀ z ∈ Metric.ball 0 1, ∀ w ∈ Metric.ball 0 1, pseudoHyperbolicExpr (g z) (g w) = pseudoHyperbolicExpr z w) (h0 : g 0 = 0) {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : ‖g z - g w‖ = ‖z - w‖

An isometry fixing the origin is a Euclidean isometry. It preserves the Euclidean distance between any two points of the open unit disc.

theorem TauCeti.real_inner_map_map_of_pseudoHyperbolicExpr_map_eq {g : ℂ → ℂ} (hg : ∀ z ∈ Metric.ball 0 1, ∀ w ∈ Metric.ball 0 1, pseudoHyperbolicExpr (g z) (g w) = pseudoHyperbolicExpr z w) (h0 : g 0 = 0) {z w : ℂ} (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) : inner ℝ (g z) (g w) = inner ℝ z w

An isometry fixing the origin preserves the real inner product.

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

Isometries fixing the origin are rotations and rotated conjugations. A self-map of the open unit disc that preserves the pseudo-hyperbolic expression and fixes 0 is z ↦ u * z or z ↦ u * conj z for a single unit u.

The hyperbolic hypothesis has already done its work at TauCeti.norm_sub_map_of_pseudoHyperbolicExpr_map_eq: what is left is a Euclidean isometry of the disc fixing its centre, which TauCeti.exists_norm_eq_one_eqOn_ball_const_mul_or_const_mul_conj_of_dist_map_eq classifies.

The classification

theorem TauCeti.exists_eqOn_ball_unitDiscStandardAutomorphismFormula_or_conj_of_pseudoHyperbolicExpr_map_eq {g : ℂ → ℂ} (hmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hg : ∀ z ∈ Metric.ball 0 1, ∀ w ∈ Metric.ball 0 1, pseudoHyperbolicExpr (g z) (g w) = pseudoHyperbolicExpr z w) : ∃ (u : ℂ) (b : ℂ), ‖u‖ = 1 ∧ ‖b‖ < 1 ∧ (Set.EqOn g (fun (z : ℂ) => u * ((z - b) / (1 - (starRingEnd ℂ) b * z))) (Metric.ball 0 1) ∨ Set.EqOn g (fun (z : ℂ) => u * (((starRingEnd ℂ) z - b) / (1 - (starRingEnd ℂ) b * (starRingEnd ℂ) z))) (Metric.ball 0 1))

The isometries of the Poincaré disc, pseudo-hyperbolic form. A self-map of the open unit disc preserving the pseudo-hyperbolic expression is a standard disc automorphism z ↦ u * (z - b) / (1 - conj b * z) or the conjugate of one. Neither holomorphy nor surjectivity is assumed.

theorem TauCeti.exists_eqOn_ball_unitDiscStandardAutomorphismFormula_or_conj_of_hyperbolicDist_map_eq {g : ℂ → ℂ} (hmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hg : ∀ z ∈ Metric.ball 0 1, ∀ w ∈ Metric.ball 0 1, hyperbolicDist (g z) (g w) = hyperbolicDist z w) : ∃ (u : ℂ) (b : ℂ), ‖u‖ = 1 ∧ ‖b‖ < 1 ∧ (Set.EqOn g (fun (z : ℂ) => u * ((z - b) / (1 - (starRingEnd ℂ) b * z))) (Metric.ball 0 1) ∨ Set.EqOn g (fun (z : ℂ) => u * (((starRingEnd ℂ) z - b) / (1 - (starRingEnd ℂ) b * (starRingEnd ℂ) z))) (Metric.ball 0 1))

The isometries of the Poincaré disc. A self-map of the open unit disc preserving the hyperbolic distance is a standard disc automorphism z ↦ u * (z - b) / (1 - conj b * z) or the conjugate of one: the isometry group of the Poincaré metric is Aut(𝔻) together with its orientation-reversing coset.

Isometric self-embeddings are onto

theorem TauCeti.bijOn_ball_of_forall_pseudoHyperbolicExpr_map_eq {g : ℂ → ℂ} (hmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hg : ∀ z ∈ Metric.ball 0 1, ∀ w ∈ Metric.ball 0 1, pseudoHyperbolicExpr (g z) (g w) = pseudoHyperbolicExpr z w) : Set.BijOn g (Metric.ball 0 1) (Metric.ball 0 1)

An isometric self-embedding of the Poincaré disc is onto, pseudo-hyperbolic form. A self-map of the open unit disc preserving the pseudo-hyperbolic expression is a bijection of the disc onto itself: the hyperbolic plane contains no proper isometric copy of itself. The companion statement for a holomorphic self-map of the disc preserving it at a single pair of distinct points is TauCeti.bijOn_ball_of_pseudoHyperbolicExpr_map_eq, from Schwarz--Pick rigidity.

theorem TauCeti.bijOn_ball_of_hyperbolicDist_map_eq {g : ℂ → ℂ} (hmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hg : ∀ z ∈ Metric.ball 0 1, ∀ w ∈ Metric.ball 0 1, hyperbolicDist (g z) (g w) = hyperbolicDist z w) : Set.BijOn g (Metric.ball 0 1) (Metric.ball 0 1)

An isometric self-embedding of the Poincaré disc is onto. A self-map of the open unit disc preserving the hyperbolic distance is a bijection of the disc onto itself.

theorem TauCeti.PoincareDisc.exists_eq_unitDiscStandardAutomorphismIsometryEquiv_or_comp_star {f : PoincareDisc → PoincareDisc} (hf : Isometry f) : ∃ (u : Circle) (a : Complex.UnitDisc), (∀ (z : PoincareDisc), f z = (unitDiscStandardAutomorphismIsometryEquiv u a) z) ∨ ∀ (z : PoincareDisc), f z = (unitDiscStandardAutomorphismIsometryEquiv u a) (starIsometryEquiv z)

The isometries of the Poincaré disc, bundled form. Every isometry of the metric space PoincareDisc is a standard disc automorphism unitDiscStandardAutomorphismIsometryEquiv u a, or that automorphism precomposed with the conjugation starIsometryEquiv: the isometry group of PoincareDisc is Aut(𝔻) together with its orientation-reversing coset. The converse is PoincareDisc.isometry_iff_exists_eq_unitDiscStandardAutomorphismIsometryEquiv_or_comp_star.

theorem TauCeti.PoincareDisc.isometry_iff_exists_eq_unitDiscStandardAutomorphismIsometryEquiv_or_comp_star {f : PoincareDisc → PoincareDisc} : Isometry f ↔ ∃ (u : Circle) (a : Complex.UnitDisc), (∀ (z : PoincareDisc), f z = (unitDiscStandardAutomorphismIsometryEquiv u a) z) ∨ ∀ (z : PoincareDisc), f z = (unitDiscStandardAutomorphismIsometryEquiv u a) (starIsometryEquiv z)

The isometry group of the Poincaré disc. A self-map of PoincareDisc is an isometry if and only if it is a standard disc automorphism unitDiscStandardAutomorphismIsometryEquiv u a or that automorphism precomposed with the conjugation starIsometryEquiv. The forward direction is the classification exists_eq_unitDiscStandardAutomorphismIsometryEquiv_or_comp_star; the converse holds because both factors are isometric equivalences.

theorem TauCeti.PoincareDisc.bijective_of_isometry {f : PoincareDisc → PoincareDisc} (hf : Isometry f) : Function.Bijective f

Every isometry of the Poincaré disc is a bijection. Injectivity comes with any Isometry; surjectivity is the content, and it is read off the classification: both a standard automorphism and the conjugation are bijections.