The standard parametrisation of `Aut(𝔻)` is a bijection #

Conformal/UnitDisc/Automorphism/Group.lean identifies the automorphism group of the open unit disc with the standard family: TauCeti.coe_unitDiscAut exhibits Aut(𝔻) as the range of

(u, a) ↦ (z ↦ u * (z - a) / (1 - conj a * z)),

a map Circle × 𝔻 → Equiv.Perm 𝔻. This file shows that map is injective, so that the description Aut(𝔻) = {e^{iθ}(z−a)/(1−āz)} is a genuine parametrisation: the rotation u and the centre a are uniquely determined by the automorphism, not merely available for it.

Why uniqueness is a separate matter #

Surjectivity onto Aut(𝔻) is the Schwarz-lemma classification and is already merged. Injectivity is elementary, but it is not formal: the family is indexed by two parameters and a priori nothing prevents different pairs from naming the same map — a family of Möbius maps of ℂ written in homogeneous coordinates is a genuine example of a parametrisation that is not injective. What makes this one injective is that the two parameters can be read off geometrically: the centre is a = e⁻¹ 0, and once the centre is known the rotation is recovered by the circle acting freely on the nonzero points of the disc. The second half is exactly the faithfulness of the Circle action on Complex.UnitDisc, which is TauCeti.instFaithfulSMulCircleUnitDisc in Analysis/Complex/UnitDisc/Basic.lean.

Main results #

TauCeti.unitDiscStandardAutomorphismEquiv_eq_iff and TauCeti.unitDiscStandardAutomorphismEquiv_injective — the parameters of a standard automorphism are unique, and TauCeti.existsUnique_eq_unitDiscStandardAutomorphismEquiv records the classification and this uniqueness together as an ∃!.
TauCeti.unitDiscAutEquivProd — the resulting bijection Aut(𝔻) ≃ Circle × 𝔻, with TauCeti.unitDiscAutEquivProd_apply_snd naming the centre coordinate as e⁻¹ 0.
TauCeti.eq_one_of_mem_unitDiscAut_of_isFixedPt — a holomorphic automorphism of the disc with two distinct fixed points is the identity. This is the rigidity statement uniqueness is usually wanted for: it is what forces a normalisation at two points to determine a conformal map.

The group-level half — the rotation subgroup of Aut(𝔻) is the circle group, not just a quotient of it — needs no declaration: with faithfulness of the circle action available, Mathlib's Cayley-theorem construction Equiv.Perm.subgroupOfMulAction Circle Complex.UnitDisc already is an isomorphism onto TauCeti.unitDiscRotation, as recorded by the example below.

Generality #

Everything here concerns Aut(𝔻) and is ℂ-scalar, as the conformal-mapping roadmap's generality bar fixes for layers L0--L6; the underlying facts about Complex.UnitDisc and its Circle action are stated at that generality in Analysis/Complex/UnitDisc/Basic.lean.

This completes the conformal-mapping roadmap's L2 description of the disc automorphism group Aut(𝔻) = {e^{iθ}(z−a)/(1−āz)} (see ConformalMapping/README.md), whose existence half is TauCeti.mem_unitDiscAut_iff. As with the rest of the L0--L3 conformal-mapping material it is coordinated with the upstream Mathlib Riemann-mapping effort leanprover-community/mathlib4#33505, whose preceding human-curated work is Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; neither contains a disc automorphism group, and should one land upstream these declarations are a temporary shim to be deleted and their consumers refactored onto it.

References #

L. Ahlfors, Complex Analysis, Ch. 6 §2.

The rotation subgroup is the circle group #

Uniqueness of the parameters #

source

theorem TauCeti.unitDiscStandardAutomorphismEquiv_symm_apply_zero (u : Circle) (a : Complex.UnitDisc) :

(unitDiscStandardAutomorphismEquiv u a).symm 0 = a

The centre of a standard automorphism is the preimage of the origin. This is the geometric description of the parameter a; it is the half of the uniqueness that needs no computation.

This is deliberately not a simp lemma: TauCeti.unitDiscStandardAutomorphismEquiv_symm already rewrites its left-hand side, and simp proves the result outright.

source

theorem TauCeti.unitDiscStandardAutomorphismEquiv_eq_iff {u v : Circle} {a b : Complex.UnitDisc} :

unitDiscStandardAutomorphismEquiv u a = unitDiscStandardAutomorphismEquiv v b ↔ u = v ∧ a = b

The parameters of a standard disc automorphism are unique. Two standard automorphisms coincide exactly when their rotations and their centres do.

source

theorem TauCeti.unitDiscStandardAutomorphismEquiv_injective :

Function.Injective fun (p : Circle × Complex.UnitDisc) => unitDiscStandardAutomorphismEquiv p.1 p.2

The standard parametrisation of Aut(𝔻) is injective: distinct pairs (u, a) name distinct automorphisms. With TauCeti.coe_unitDiscAut, which says the parametrisation has Aut(𝔻) as its range, this is the statement that Circle × 𝔻 parametrises the group.

source

@[simp]

theorem TauCeti.unitDiscStandardAutomorphismEquiv_eq_one_iff {u : Circle} {a : Complex.UnitDisc} :

unitDiscStandardAutomorphismEquiv u a = 1 ↔ u = 1 ∧ a = 0

A standard automorphism is the identity exactly at the trivial parameters.

source

theorem TauCeti.existsUnique_eq_unitDiscStandardAutomorphismEquiv {e : Equiv.Perm Complex.UnitDisc} (he : e ∈ unitDiscAut) :

∃! p : Circle × Complex.UnitDisc , e = unitDiscStandardAutomorphismEquiv p.1 p.2

The classification of disc automorphisms, with uniqueness. A holomorphic automorphism of the disc is a standard automorphism for exactly one rotation and one centre.

The bijection `Aut(𝔻) ≃ Circle × 𝔻` #

source

noncomputable def TauCeti.unitDiscAutEquivProd :

↥unitDiscAut ≃ Circle × Complex.UnitDisc

Aut(𝔻) ≃ Circle × 𝔻. The automorphism group of the unit disc is parametrised by a rotation and a centre, bijectively: the inverse map is (u, a) ↦ (z ↦ u * (z - a) / (1 - conj a * z)).

This is only a bijection of types, not a group isomorphism: the composition law on Aut(𝔻) does not become the product law on Circle × 𝔻, since already TauCeti.unitDiscStandardAutomorphismEquiv_symm_eq shows that inversion mixes the two coordinates.

Equations