The automorphism group of the complex unit disc

Conformal/UnitDisc/Automorphism/Classification.lean shows that a holomorphic self-map of the open unit disc with a holomorphic two-sided inverse has the standard form z ↦ u * (z - a) / (1 - conj a * z). That is a statement about individual maps. This file turns the family into the group Aut(𝔻) that the conformal-mapping roadmap's L2 layer asks for, and identifies it with the standard family.

The group is unitDiscAut, a Subgroup (Equiv.Perm Complex.UnitDisc): a permutation of the bundled disc belongs to it exactly when both it and its inverse are restrictions of functions ℂ → ℂ that are holomorphic on Metric.ball 0 1 (the predicate IsHolomorphicUnitDiscPerm). Stated this way the subgroup axioms are elementary — a composite of holomorphic maps is holomorphic — while the classification supplies the description of the underlying set.

Main results

• TauCeti.unitDiscAut — the group of holomorphic automorphisms of the unit disc.
• TauCeti.mem_unitDiscAut_iff — Aut(𝔻) = {z ↦ u * (z - a) / (1 - conj a * z)}: a permutation of the disc is a holomorphic automorphism iff it is a standard automorphism.
• TauCeti.unitDiscStandardAutomorphismEquiv_symm_eq — the standard family is closed under inversion, with the explicit parameters (u, a) ↦ (u⁻¹, u • (-a)).
• TauCeti.exists_mul_eq_unitDiscStandardAutomorphismEquiv — it is closed under composition; the parameters of the composite are supplied abstractly by the group structure rather than by a direct computation.
• TauCeti.unitDiscAut.isPretransitive — Aut(𝔻) acts transitively on the disc, as the standard MulAction.IsPretransitive instance (with TauCeti.exists_mem_unitDiscAut_apply_eq the corresponding statement about the ambient permutations).
• TauCeti.stabilizer_zero_eq_unitDiscRotation_subgroupOf — the stabiliser of the origin is the rotation subgroup unitDiscRotation, the image of Circle under its action on the disc (with TauCeti.mem_unitDiscRotation_iff the ambient membership criterion).

Transitivity together with the stabiliser description is how Aut(𝔻) gets used downstream: normalise a map at a chosen base point (transitivity), then read off the freedom that is left over (a rotation).

This discharges the group half of the conformal-mapping roadmap's L2 description of the disc automorphism group Aut(𝔻) = {e^{iθ}(z−a)/(1−āz)} (see ConformalMapping/README.md). 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 human-curated predecessors are Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; should a disc automorphism group 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.

def TauCeti.IsHolomorphicUnitDiscPerm (e : Equiv.Perm Complex.UnitDisc) : Prop

A permutation of the complex unit disc is holomorphic when it is the restriction of a function ℂ → ℂ that is holomorphic on the open unit ball.

Holomorphy of a map of the bundled disc is phrased through a scalar representative, matching the generality bar of the conformal-mapping roadmap (everything is stated for f : ℂ → ℂ) and the hypotheses of exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv.

Equations

• TauCeti.IsHolomorphicUnitDiscPerm e = ∃ (f : ℂ → ℂ), DifferentiableOn ℂ f (Metric.ball 0 1) ∧ ∀ (z : Complex.UnitDisc), ↑(e z) = f ↑z

def TauCeti.unitDiscAut : Subgroup (Equiv.Perm Complex.UnitDisc)

The automorphism group of the unit disc. A permutation of Complex.UnitDisc is a holomorphic automorphism when both it and its inverse extend to functions that are holomorphic on the open unit ball.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.mem_unitDiscAut {e : Equiv.Perm Complex.UnitDisc} : e ∈ unitDiscAut ↔ IsHolomorphicUnitDiscPerm e ∧ IsHolomorphicUnitDiscPerm (Equiv.symm e)

theorem TauCeti.unitDiscStandardAutomorphismEquiv_symm_eq (u : Circle) (a : Complex.UnitDisc) : (unitDiscStandardAutomorphismEquiv u a).symm = unitDiscStandardAutomorphismEquiv u⁻¹ (u • -a)

The inverse of a standard disc automorphism is again one: inverting z ↦ u * (z - a) / (1 - conj a * z) replaces the rotation u by u⁻¹ and the centre a by u • (-a), the image of the origin under the original automorphism. (The inverse itself sends 0 to a, since the original sends a to 0.)

theorem TauCeti.isHolomorphicUnitDiscPerm_unitDiscStandardAutomorphismEquiv (u : Circle) (a : Complex.UnitDisc) : IsHolomorphicUnitDiscPerm (unitDiscStandardAutomorphismEquiv u a)

A standard disc automorphism is holomorphic.

theorem TauCeti.unitDiscStandardAutomorphismEquiv_mem_unitDiscAut (u : Circle) (a : Complex.UnitDisc) : unitDiscStandardAutomorphismEquiv u a ∈ unitDiscAut

Every standard disc automorphism is a holomorphic automorphism of the disc.

@[simp]

theorem TauCeti.mem_unitDiscAut_iff {e : Equiv.Perm Complex.UnitDisc} : e ∈ unitDiscAut ↔ ∃ (u : Circle) (a : Complex.UnitDisc), e = unitDiscStandardAutomorphismEquiv u a

Aut(𝔻) = {e^{iθ}(z − a)/(1 − āz)}. A permutation of the complex unit disc is a holomorphic automorphism exactly when it is a standard automorphism.

The forward direction is the classification theorem exists_forall_unitDisc_eq_unitDiscStandardAutomorphismEquiv, which rests on the Schwarz lemma; the converse is the holomorphy of the standard formula and of its inverse.

theorem TauCeti.coe_unitDiscAut : ↑unitDiscAut = Set.range fun (p : Circle × Complex.UnitDisc) => unitDiscStandardAutomorphismEquiv p.1 p.2

The underlying set of Aut(𝔻) is the range of the standard parametrisation by a rotation and a centre.

theorem TauCeti.exists_mul_eq_unitDiscStandardAutomorphismEquiv (u₁ u₂ : Circle) (a₁ a₂ : Complex.UnitDisc) : ∃ (u : Circle) (a : Complex.UnitDisc), unitDiscStandardAutomorphismEquiv u₁ a₁ * unitDiscStandardAutomorphismEquiv u₂ a₂ = unitDiscStandardAutomorphismEquiv u a

The standard disc automorphisms are closed under composition.

This is a corollary of the group structure and the classification: no computation with the composite of two Moebius factors is needed.

instance TauCeti.unitDiscAut.isPretransitive : MulAction.IsPretransitive (↥unitDiscAut) Complex.UnitDisc

Aut(𝔻) acts transitively on the disc. Any point of the disc can be moved to any other by a holomorphic automorphism, namely the composite of the Moebius factor centred at the source with the inverse of the one centred at the target.

theorem TauCeti.exists_mem_unitDiscAut_apply_eq (z w : Complex.UnitDisc) : ∃ e ∈ unitDiscAut, e z = w

Transitivity of Aut(𝔻) on the disc, phrased for the ambient permutations.

noncomputable def TauCeti.unitDiscRotation : Subgroup (Equiv.Perm Complex.UnitDisc)

The rotations z ↦ u * z, as a subgroup of the permutations of the unit disc. It is the image of Circle under its multiplicative action on the disc.

Equations

• TauCeti.unitDiscRotation = (MulAction.toPermHom Circle Complex.UnitDisc).range

theorem TauCeti.unitDiscRotation_eq_range : unitDiscRotation = (MulAction.toPermHom Circle Complex.UnitDisc).range

The rotation subgroup is the range of the circle action, in the form that transfers general constructions about MonoidHom.range — such as Mathlib's Cayley-theorem construction Equiv.Perm.subgroupOfMulAction — to TauCeti.unitDiscRotation.

theorem TauCeti.unitDiscStandardAutomorphismEquiv_zero_mem_unitDiscRotation (u : Circle) : unitDiscStandardAutomorphismEquiv u 0 ∈ unitDiscRotation

@[simp]

theorem TauCeti.mem_unitDiscRotation_iff {e : Equiv.Perm Complex.UnitDisc} : e ∈ unitDiscRotation ↔ e ∈ unitDiscAut ∧ e 0 = 0

The stabiliser of the origin in Aut(𝔻) is the rotation group. A permutation of the disc is a rotation exactly when it is a holomorphic automorphism fixing the origin.

The forward implication is immediate; the converse is the classification, which forces the centre of a standard automorphism fixing 0 to be 0. This is the group-theoretic form of the rigidity statement behind the Schwarz lemma.

theorem TauCeti.unitDiscRotation_le_unitDiscAut : unitDiscRotation ≤ unitDiscAut

The rotations are holomorphic automorphisms of the disc.

theorem TauCeti.stabilizer_zero_eq_unitDiscRotation_subgroupOf : MulAction.stabilizer (↥unitDiscAut) 0 = unitDiscRotation.subgroupOf unitDiscAut

The stabiliser of the origin in Aut(𝔻) is the rotation group, as subgroups of Aut(𝔻) itself: the rotations sit inside Aut(𝔻) as unitDiscRotation.subgroupOf unitDiscAut, and that subgroup is exactly MulAction.stabilizer unitDiscAut 0.