A holomorphic automorphism of the unit disc fixing the origin is a rotation

This file records the Schwarz-lemma rigidity for the complex unit disc: a holomorphic self-map f of Metric.ball (0 : ℂ) 1 that admits a holomorphic left inverse which is itself a self-map of the disc, and that fixes the origin, is a rotation z ↦ c * z for a constant c of modulus one. Equivalently, the rotation factor is deriv f 0, and such a map with derivative 1 at the origin is the identity. (The left inverse gives injectivity; that f is in fact a genuine automorphism is part of the conclusion, since a rotation is bijective.)

The proof is the classical two-sided Schwarz argument. Applying Mathlib's Schwarz lemma (Complex.norm_le_norm_of_mapsTo_ball) to f and to its inverse gives ‖f z‖ = ‖z‖ on the whole disc; the equality case of the Schwarz lemma (Complex.affine_of_mapsTo_ball_of_norm_dslope_eq_div) then forces f to be linear.

This advances the conformal-mapping roadmap's L2 disc-automorphism target (TauCetiRoadmap/ConformalMapping/README.md, layer L2: "the disc automorphism group Aut(𝔻) = {e^{iθ}(z−a)/(1−āz)}"); it is the rotation rigidity that pins down the automorphisms fixing the origin, and is the step Mathlib's Analysis/Complex/Schwarz.lean lists as an open TODO ("Prove that any diffeomorphism of the unit disk to itself is a Möbius map"). It reuses Mathlib's Schwarz lemma throughout and adds no new complex-analytic input. As with the rest of the L0--L3 conformal-mapping material, it is coordinated with the upstream Mathlib RMT effort leanprover-community/mathlib4#33505 and should be refactored to upstream API if that work lands a human-curated disc-automorphism classification.

theorem TauCeti.norm_map_of_leftInvOn_ball_of_map_zero {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hg : DifferentiableOn ℂ g (Metric.ball 0 1)) (hfmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hgmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hgf : ∀ z ∈ Metric.ball 0 1, g (f z) = z) (hf0 : f 0 = 0) {z : ℂ} (hz : z ∈ Metric.ball 0 1) : ‖f z‖ = ‖z‖

A holomorphic self-map of the open unit disc fixing the origin and admitting a holomorphic left inverse that is itself a self-map of the disc preserves the modulus: ‖f z‖ = ‖z‖ for every z in the disc.

This is the w = 0 case of the Schwarz--Pick equality pseudoHyperbolicExpr_map_eq, where the pseudo-hyperbolic expression to the origin is just the norm.

theorem TauCeti.exists_eqOn_const_mul_of_leftInvOn_ball_of_map_zero {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hg : DifferentiableOn ℂ g (Metric.ball 0 1)) (hfmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hgmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hgf : ∀ z ∈ Metric.ball 0 1, g (f z) = z) (hf0 : f 0 = 0) : ∃ (c : ℂ), ‖c‖ = 1 ∧ Set.EqOn f (fun (z : ℂ) => c * z) (Metric.ball 0 1)

Rotation rigidity for the unit disc. A holomorphic self-map f of the open unit disc with a holomorphic left inverse g that is also a self-map of the disc, fixing the origin, is a rotation: there is a constant c of modulus one with f z = c * z throughout the disc.

theorem TauCeti.eqOn_deriv_zero_mul_of_leftInvOn_ball_of_map_zero {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hg : DifferentiableOn ℂ g (Metric.ball 0 1)) (hfmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hgmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hgf : ∀ z ∈ Metric.ball 0 1, g (f z) = z) (hf0 : f 0 = 0) : ‖deriv f 0‖ = 1 ∧ Set.EqOn f (fun (z : ℂ) => deriv f 0 * z) (Metric.ball 0 1)

The rotation factor of an origin-fixing self-map of the disc with a holomorphic self-map left inverse is its derivative at the origin: with the hypotheses of exists_eqOn_const_mul_of_leftInvOn_ball_of_map_zero, the map equals z ↦ deriv f 0 * z on the disc, and ‖deriv f 0‖ = 1.

theorem TauCeti.eqOn_id_of_leftInvOn_ball_of_map_zero_of_deriv_zero_eq_one {f g : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hg : DifferentiableOn ℂ g (Metric.ball 0 1)) (hfmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hgmaps : Set.MapsTo g (Metric.ball 0 1) (Metric.ball 0 1)) (hgf : ∀ z ∈ Metric.ball 0 1, g (f z) = z) (hf0 : f 0 = 0) (hderiv : deriv f 0 = 1) : Set.EqOn f id (Metric.ball 0 1)

Uniqueness of the identity. An origin-fixing holomorphic self-map of the unit disc with a holomorphic self-map left inverse, whose derivative at the origin is 1, is the identity on the disc.