Disc automorphisms as Poincaré isometric equivalences

This file bundles the standard automorphisms of the complex unit disc as isometric equivalences of PoincareDisc. The underlying distance-preservation results are proved in Poincare/MetricSpace.lean; the bundled form records both the isometry and the inverse and is therefore the natural API for the automorphism group acting on the Poincaré disc.

The main constructions are:

• PoincareDisc.isometryEquivOfHyperbolicDistEq, which transports any hyperbolic-distance-preserving equivalence of Complex.UnitDisc;
• PoincareDisc.unitDiscMoebiusIsometryEquiv, for the automorphism sending a to zero;
• PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv, for z ↦ u * (z - a) / (1 - conj a * z);
• PoincareDisc.starIsometryEquiv, for the conjugation z ↦ conj z, which is a Poincaré isometry without being a disc automorphism: it is the orientation-reversing symmetry.

This advances the conformal-mapping roadmap's L2 targets for the Poincaré metric and the disc automorphism group. It reuses Tau Ceti's disc-automorphism and hyperbolic-distance invariance API. 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 and should be refactored to upstream API if that work lands a human-curated Poincaré-disc isometry API.

noncomputable def TauCeti.PoincareDisc.isometryEquivOfHyperbolicDistEq (e : Complex.UnitDisc ≃ Complex.UnitDisc) (he : ∀ (z w : Complex.UnitDisc), hyperbolicDist ↑(e z) ↑(e w) = hyperbolicDist ↑z ↑w) : PoincareDisc ≃ᵢ PoincareDisc

A hyperbolic-distance-preserving equivalence of the unit disc induces an isometric equivalence of the Poincaré disc.

Equations

• TauCeti.PoincareDisc.isometryEquivOfHyperbolicDistEq e he = { toEquiv := TauCeti.PoincareDisc.toUnitDisc.trans (e.trans Complex.UnitDisc.toPoincare), isometry_toFun := ⋯ }

@[simp]

theorem TauCeti.PoincareDisc.isometryEquivOfHyperbolicDistEq_apply (e : Complex.UnitDisc ≃ Complex.UnitDisc) (he : ∀ (z w : Complex.UnitDisc), hyperbolicDist ↑(e z) ↑(e w) = hyperbolicDist ↑z ↑w) (z : PoincareDisc) : (isometryEquivOfHyperbolicDistEq e he) z = Complex.UnitDisc.toPoincare (e (toUnitDisc z))

The underlying function of the transported isometric equivalence is the original unit-disc equivalence, conjugated by the identity reinterpretation maps.

theorem TauCeti.PoincareDisc.isometryEquivOfHyperbolicDistEq_symm (e : Complex.UnitDisc ≃ Complex.UnitDisc) (he : ∀ (z w : Complex.UnitDisc), hyperbolicDist ↑(e z) ↑(e w) = hyperbolicDist ↑z ↑w) : (isometryEquivOfHyperbolicDistEq e he).symm = isometryEquivOfHyperbolicDistEq e.symm ⋯

Taking the inverse commutes with transporting a hyperbolic-distance-preserving equivalence to the Poincaré disc.

noncomputable def TauCeti.PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv (u : Circle) (a : Complex.UnitDisc) : PoincareDisc ≃ᵢ PoincareDisc

The standard disc automorphism with rotation u and center a as an isometric equivalence of the Poincaré disc.

Equations

• TauCeti.PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv u a = TauCeti.PoincareDisc.isometryEquivOfHyperbolicDistEq (TauCeti.unitDiscStandardAutomorphismEquiv u a) ⋯

@[simp]

theorem TauCeti.PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv_apply (u : Circle) (a : Complex.UnitDisc) (z : PoincareDisc) : (unitDiscStandardAutomorphismIsometryEquiv u a) z = Complex.UnitDisc.toPoincare ((unitDiscStandardAutomorphismEquiv u a) (toUnitDisc z))

The standard Poincaré isometry acts by the standard unit-disc automorphism.

@[simp]

theorem TauCeti.PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv_symm_apply (u : Circle) (a : Complex.UnitDisc) (z : PoincareDisc) : (unitDiscStandardAutomorphismIsometryEquiv u a).symm z = Complex.UnitDisc.toPoincare ((unitDiscMoebiusEquiv (-a)) (u⁻¹ • toUnitDisc z))

The inverse of the standard Poincaré isometry applies the inverse rotation followed by the inverse Moebius factor.

noncomputable def TauCeti.PoincareDisc.starIsometryEquiv : PoincareDisc ≃ᵢ PoincareDisc

Complex conjugation as an isometric equivalence of the Poincaré disc. It is not a disc automorphism, being orientation-reversing rather than holomorphic, but it does preserve the hyperbolic distance (TauCeti.hyperbolicDist_conj); together with the standard automorphisms it exhausts the Poincaré isometries.

Equations

• TauCeti.PoincareDisc.starIsometryEquiv = TauCeti.PoincareDisc.isometryEquivOfHyperbolicDistEq (Function.Involutive.toPerm star ⋯) TauCeti.PoincareDisc.starIsometryEquiv._proof_1✝

@[simp]

theorem TauCeti.PoincareDisc.starIsometryEquiv_apply (z : PoincareDisc) : starIsometryEquiv z = Complex.UnitDisc.toPoincare (star (toUnitDisc z))

The conjugation isometry of the Poincaré disc acts by star on the underlying disc.

@[simp]

theorem TauCeti.PoincareDisc.starIsometryEquiv_symm : starIsometryEquiv.symm = starIsometryEquiv

Conjugation is an involution of the Poincaré disc, so it is its own inverse.

noncomputable def TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv (a : Complex.UnitDisc) : PoincareDisc ≃ᵢ PoincareDisc

The disc Moebius automorphism centred at a as an isometric equivalence of the Poincaré disc.

Equations

• TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv a = TauCeti.PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv 1 a

@[simp]

theorem TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv_apply (a : Complex.UnitDisc) (z : PoincareDisc) : (unitDiscMoebiusIsometryEquiv a) z = Complex.UnitDisc.toPoincare (unitDiscMoebius a (toUnitDisc z))

The Moebius Poincaré isometry acts by the usual unit-disc Moebius automorphism.

@[simp]

theorem TauCeti.PoincareDisc.unitDiscMoebiusIsometryEquiv_symm (a : Complex.UnitDisc) : (unitDiscMoebiusIsometryEquiv a).symm = unitDiscMoebiusIsometryEquiv (-a)

The inverse of the Moebius Poincaré isometry centred at a is the one centred at -a.

@[simp]

theorem TauCeti.PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv_one (a : Complex.UnitDisc) : unitDiscStandardAutomorphismIsometryEquiv 1 a = unitDiscMoebiusIsometryEquiv a

With unit rotation factor, the standard Poincaré isometry is the Moebius isometry.

theorem TauCeti.PoincareDisc.unitDiscStandardAutomorphismIsometryEquiv_self (u : Circle) (a : Complex.UnitDisc) : (unitDiscStandardAutomorphismIsometryEquiv u a) (Complex.UnitDisc.toPoincare a) = Complex.UnitDisc.toPoincare 0

The standard Poincaré isometry sends its center to the origin.