Unit-disc automorphisms as homeomorphisms

This file packages the standard unit-disc automorphisms from TauCeti.Analysis.Complex.Conformal.UnitDisc.Automorphism.Basic as homeomorphisms of Complex.UnitDisc. The underlying map is the existing equivalence unitDiscStandardAutomorphismEquiv; this file adds the continuity API needed before treating the disc automorphisms as a topological automorphism group in the Schwarz--Pick layer of the conformal-mapping roadmap.

This L2 material is coordinated with the upstream Mathlib RMT effort in leanprover-community/mathlib4#33505. Mathlib already contains the preceding human-curated work in Analysis/Complex/RiemannMapping.lean and Analysis/Complex/BranchLogRoot.lean; this file only packages Tau Ceti's existing unit-disc automorphism formulas topologically.

noncomputable def TauCeti.unitDiscStandardAutomorphismHomeomorph (u : Circle) (a : Complex.UnitDisc) : Complex.UnitDisc ≃ₜ Complex.UnitDisc

The standard automorphism of the complex unit disc, bundled as a homeomorphism.

It is the composition of the Moebius homeomorphism sending a to 0 with the fixed circle rotation by u.

Equations

• TauCeti.unitDiscStandardAutomorphismHomeomorph u a = (TauCeti.unitDiscMoebiusHomeomorph a).trans (Homeomorph.smul u)

@[simp]

theorem TauCeti.unitDiscStandardAutomorphismHomeomorph_apply (u : Circle) (a z : Complex.UnitDisc) : (unitDiscStandardAutomorphismHomeomorph u a) z = (unitDiscStandardAutomorphismEquiv u a) z

The standard automorphism homeomorphism applies by the existing equivalence formula.

@[simp]

theorem TauCeti.unitDiscStandardAutomorphismHomeomorph_toEquiv (u : Circle) (a : Complex.UnitDisc) : (unitDiscStandardAutomorphismHomeomorph u a).toEquiv = unitDiscStandardAutomorphismEquiv u a

The underlying equivalence of the standard automorphism homeomorphism is the existing one.

@[simp]

theorem TauCeti.unitDiscStandardAutomorphismHomeomorph_symm (u : Circle) (a : Complex.UnitDisc) : (unitDiscStandardAutomorphismHomeomorph u a).symm = (Homeomorph.smul u⁻¹).trans (unitDiscMoebiusHomeomorph (-a))

The inverse standard automorphism homeomorphism is inverse rotation followed by the inverse Moebius homeomorphism.

theorem TauCeti.coe_unitDiscStandardAutomorphismHomeomorph_apply (u : Circle) (a z : Complex.UnitDisc) : ↑((unitDiscStandardAutomorphismHomeomorph u a) z) = ↑u * ((↑z - ↑a) / (1 - (starRingEnd ℂ) ↑a * ↑z))

The scalar formula for the standard disc-automorphism homeomorphism.

@[simp]

theorem TauCeti.unitDiscStandardAutomorphismHomeomorph_zero (u : Circle) : unitDiscStandardAutomorphismHomeomorph u 0 = Homeomorph.smul u

With zero center, the standard automorphism homeomorphism is just rotation.

@[simp]

theorem TauCeti.unitDiscStandardAutomorphismHomeomorph_one (a : Complex.UnitDisc) : unitDiscStandardAutomorphismHomeomorph 1 a = unitDiscMoebiusHomeomorph a

With unit rotation factor, the standard automorphism homeomorphism is the Moebius one.