Rigidity in the Schwarz--Pick theorem

The Schwarz--Pick theorem (TauCeti.pseudoHyperbolicExpr_map_le) says a holomorphic self-map f of the open unit disc contracts the pseudo-hyperbolic expression pseudoHyperbolicExpr z w = ‖(z - w) / (1 - conj w * z)‖. This file proves the equality case: if the contraction is an equality at a single pair of distinct points, then f is a disc automorphism, and in particular the contraction is an equality everywhere.

The proof runs on the shared TauCeti.schwarzPickConjugate construction, which conjugates f by the Moebius factors that send w to 0 on the source and f w to 0 on the target, exactly as the contraction estimate does. The conjugate g = schwarzPickConjugate f w is a holomorphic self-map of the disc fixing the origin, and the hypothesis says ‖g ξ‖ = ‖ξ‖ at the nonzero point ξ = (z - w) / (1 - conj w * z). Mathlib's equality case of the Schwarz lemma in its existence form, Complex.affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div', consumes exactly that one equality point, supplied as an existential, and forces g to be the rotation ζ ↦ C * ζ for a unimodular constant C. Unwinding the conjugation gives the identity (f ζ - f w) / (1 - conj (f w) * f ζ) = C * ((ζ - w) / (1 - conj w * ζ)) on the whole disc, from which the inverse map is read off explicitly as a Moebius factor, an inverse rotation and a Moebius factor.

Main results

• TauCeti.exists_norm_eq_one_forall_eq_of_pseudoHyperbolicExpr_map_eq — the unwound identity above: f is the Moebius conjugate of a rotation;
• TauCeti.exists_differentiableOn_mapsTo_invOn_of_pseudoHyperbolicExpr_map_eq — the explicit holomorphic two-sided inverse of f on the disc;
• TauCeti.bijOn_ball_of_pseudoHyperbolicExpr_map_eq — f is a bijection of the disc;
• TauCeti.forall_pseudoHyperbolicExpr_map_eq_of_pseudoHyperbolicExpr_map_eq — one equality propagates to every pair of points, so f is a pseudo-hyperbolic isometry;
• exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv_of_pseudoHyperbolicExpr_map_eq — f has the standard form u * (ζ - a) / (1 - conj a * ζ);
• TauCeti.forall_hyperbolicDist_map_eq_of_hyperbolicDist_map_eq and exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv_of_hyperbolicDist_map_eq — the same rigidity stated for the hyperbolic (Poincaré) distance.

Together with TauCeti.pseudoHyperbolicExpr_unitDiscStandardAutomorphismEquiv, which says the standard automorphisms are pseudo-hyperbolic isometries, these results identify the isometry group of the pseudo-hyperbolic expression among the holomorphic self-maps of the disc.

This advances the conformal-mapping roadmap's L2 target (Schwarz lemma extensions: Schwarz--Pick and the disc automorphism group Aut(𝔻) = {e^{iθ}(z−a)/(1−āz)}; see ConformalMapping/README.md). It reuses Mathlib's Schwarz-lemma equality case and Tau Ceti's unit-disc Moebius and disc-automorphism API rather than re-deriving either. As with the rest of the L0--L3 conformal-mapping material, it is coordinated with the upstream Mathlib RMT effort leanprover-community/mathlib4#33505. Mathlib already contains the preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; none of it is duplicated here, and should a human-curated Schwarz--Pick rigidity statement land upstream this file should be refactored onto it, or deleted with its consumers refactored.

theorem TauCeti.exists_norm_eq_one_forall_eq_of_pseudoHyperbolicExpr_map_eq {f : ℂ → ℂ} {z w : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hne : z ≠ w) (heq : pseudoHyperbolicExpr (f z) (f w) = pseudoHyperbolicExpr z w) : ∃ (C : ℂ), ‖C‖ = 1 ∧ ∀ ζ ∈ Metric.ball 0 1, (f ζ - f w) / (1 - (starRingEnd ℂ) (f w) * f ζ) = C * ((ζ - w) / (1 - (starRingEnd ℂ) w * ζ))

Rigidity in the Schwarz--Pick theorem. If a holomorphic self-map f of the open unit disc preserves the pseudo-hyperbolic expression at one pair of distinct points z ≠ w, then on the whole disc f is the Moebius conjugate of a rotation: there is a unimodular C with

(f ζ - f w) / (1 - conj (f w) * f ζ) = C * ((ζ - w) / (1 - conj w * ζ)).

theorem TauCeti.exists_differentiableOn_mapsTo_invOn_of_pseudoHyperbolicExpr_map_eq {f : ℂ → ℂ} {z w : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hne : z ≠ w) (heq : pseudoHyperbolicExpr (f z) (f w) = pseudoHyperbolicExpr z w) : ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g (Metric.ball 0 1) ∧ Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1) ∧ Set.LeftInvOn g f (Metric.ball 0 1) ∧ Set.RightInvOn g f (Metric.ball 0 1)

The inverse map produced by Schwarz--Pick rigidity. Under the hypotheses of TauCeti.exists_norm_eq_one_forall_eq_of_pseudoHyperbolicExpr_map_eq, the map f has an explicit holomorphic two-sided inverse on the open unit disc, namely the composite of the Moebius factor centred at f w, the inverse rotation, and the Moebius factor centred at -w.

theorem TauCeti.bijOn_ball_of_pseudoHyperbolicExpr_map_eq {f : ℂ → ℂ} {z w : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hne : z ≠ w) (heq : pseudoHyperbolicExpr (f z) (f w) = pseudoHyperbolicExpr z w) : Set.BijOn f (Metric.ball 0 1) (Metric.ball 0 1)

Schwarz--Pick rigidity, bijectivity form. A holomorphic self-map of the open unit disc that preserves the pseudo-hyperbolic expression at one pair of distinct points is a bijection of the disc, hence a conformal automorphism.

theorem TauCeti.forall_pseudoHyperbolicExpr_map_eq_of_pseudoHyperbolicExpr_map_eq {f : ℂ → ℂ} {z w : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hne : z ≠ w) (heq : pseudoHyperbolicExpr (f z) (f w) = pseudoHyperbolicExpr z w) (p : ℂ) : p ∈ Metric.ball 0 1 → ∀ q ∈ Metric.ball 0 1, pseudoHyperbolicExpr (f p) (f q) = pseudoHyperbolicExpr p q

Schwarz--Pick rigidity, isometry form. One equality in the Schwarz--Pick estimate propagates to every pair of points: the map preserves the pseudo-hyperbolic expression on the whole disc.

theorem TauCeti.exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv_of_pseudoHyperbolicExpr_map_eq {f : ℂ → ℂ} {z w : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hne : z ≠ w) (heq : pseudoHyperbolicExpr (f z) (f w) = pseudoHyperbolicExpr z w) : ∃ (u : Circle) (a : Complex.UnitDisc), ∀ (ζ : Complex.UnitDisc), f ↑ζ = ↑((unitDiscStandardAutomorphismEquiv u a) ζ)

Schwarz--Pick rigidity, classification form. A holomorphic self-map of the open unit disc that preserves the pseudo-hyperbolic expression at one pair of distinct points is one of the standard disc automorphisms ζ ↦ u * (ζ - a) / (1 - conj a * ζ).

theorem TauCeti.forall_hyperbolicDist_map_eq_of_hyperbolicDist_map_eq {f : ℂ → ℂ} {z w : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hne : z ≠ w) (heq : hyperbolicDist (f z) (f w) = hyperbolicDist z w) (p : ℂ) : p ∈ Metric.ball 0 1 → ∀ q ∈ Metric.ball 0 1, hyperbolicDist (f p) (f q) = hyperbolicDist p q

Schwarz--Pick rigidity, hyperbolic-distance form. A holomorphic self-map of the open unit disc that preserves the hyperbolic (Poincaré) distance between one pair of distinct points is a hyperbolic isometry of the disc.

theorem TauCeti.exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv_of_hyperbolicDist_map_eq {f : ℂ → ℂ} {z w : ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hz : z ∈ Metric.ball 0 1) (hw : w ∈ Metric.ball 0 1) (hne : z ≠ w) (heq : hyperbolicDist (f z) (f w) = hyperbolicDist z w) : ∃ (u : Circle) (a : Complex.UnitDisc), ∀ (ζ : Complex.UnitDisc), f ↑ζ = ↑((unitDiscStandardAutomorphismEquiv u a) ζ)

Schwarz--Pick rigidity, hyperbolic-distance classification form. A holomorphic self-map of the open unit disc that preserves the hyperbolic distance between one pair of distinct points is one of the standard disc automorphisms.