Fixed points of holomorphic self-maps of the unit disc

A holomorphic self-map of the open unit disc that fixes two distinct points of the disc is the identity (TauCeti.eqOn_id_of_isFixedPt_of_isFixedPt); equivalently, the fixed-point set in the open unit disc of any self-map other than the identity is a subsingleton (TauCeti.subsingleton_inter_fixedPoints_of_not_eqOn_id), which read hypothesis-free is the dichotomy that a self-map is either the identity or fixes at most one point of the disc (TauCeti.eqOn_id_or_subsingleton_inter_fixedPoints).

This generalises TauCeti.eq_one_of_mem_unitDiscAut_of_isFixedPt of UnitDisc/Automorphism/Parametrization.lean, which says the same for a member of Aut(𝔻), from automorphisms to arbitrary holomorphic self-maps.

The argument

The automorphism case is exactly what the proof runs on. Two fixed points make the Schwarz--Pick contraction estimate an equality at that pair of points for a trivial reason — both sides are the same pseudo-hyperbolic expression — so the classification form of Schwarz--Pick rigidity, exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv_of_pseudoHyperbolicExpr_map_eq of SchwarzPick/Rigidity.lean, turns f into a standard disc automorphism ζ ↦ u * (ζ - b) / (1 - conj b * ζ). Its two fixed points then force it to be the identity of Aut(𝔻) by the already-merged automorphism statement.

Generality

In accordance with the generality bar of ConformalMapping/README.md, which fixes scalar ℂ for every theorem added in layers L0--L6, everything below is stated for maps of ℂ, matching the rest of Conformal/SchwarzPick/. The hypothesis Function.IsFixedPt f a is Mathlib's spelling of f a = a, as in TauCeti.eq_one_of_mem_unitDiscAut_of_isFixedPt.

Coordination with upstream Mathlib

Per the Coordination with upstream Mathlib section of ConformalMapping/README.md, the L0--L3 material of this roadmap overlaps the in-progress human-curated Riemann-mapping effort mathlib4#33505, which proves its prerequisites internally as private lemmas; Mathlib's Analysis/Complex/Schwarz.lean and Analysis/Complex/BranchLogRoot.lean are the preceding human-curated work. This file is therefore a temporary shim in the same sense as the rest of Conformal/SchwarzPick/: should a human-curated fixed-point form of Schwarz--Pick land upstream, these statements are to be backed by it, or deleted and their consumers refactored onto it.

References

• L. Ahlfors, Complex Analysis, Ch. 6 §1.2.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. VI §2.

theorem TauCeti.eqOn_id_of_isFixedPt_of_isFixedPt {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) (hfz : Function.IsFixedPt f z) (hfw : Function.IsFixedPt f w) : Set.EqOn f id (Metric.ball 0 1)

A holomorphic self-map of the disc with two distinct fixed points is the identity.

If f is differentiable on the open unit ball ball (0 : ℂ) 1, maps that ball into itself and fixes two distinct points z ≠ w of it, then f agrees with the identity on the whole ball. This is TauCeti.eq_one_of_mem_unitDiscAut_of_isFixedPt with its hypothesis weakened from membership in Aut(𝔻) to an arbitrary holomorphic self-map.

theorem TauCeti.subsingleton_inter_fixedPoints_of_not_eqOn_id {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) (hid : ¬Set.EqOn f id (Metric.ball 0 1)) : (Metric.ball 0 1 ∩ Function.fixedPoints f).Subsingleton

The fixed-point set in the disc of a self-map other than the identity is a subsingleton.

The hypotheses constrain f only on ball (0 : ℂ) 1, so only the fixed points lying in that ball are controlled: fixed points of f outside the disc are arbitrary.

theorem TauCeti.eqOn_id_or_subsingleton_inter_fixedPoints {f : ℂ → ℂ} (hf : DifferentiableOn ℂ f (Metric.ball 0 1)) (hmaps : Set.MapsTo f (Metric.ball 0 1) (Metric.ball 0 1)) : Set.EqOn f id (Metric.ball 0 1) ∨ (Metric.ball 0 1 ∩ Function.fixedPoints f).Subsingleton

The fixed-point dichotomy for a holomorphic self-map of the disc. Either the map is the identity, or it fixes at most one point of the disc.