Automorphisms of the Euclidean ball and the ball–polydisc distinction

The explicit involution exchanges an interior point with zero. Holomorphy, a nonvanishing denominator, the metric identity, preservation of the ball, and involutivity are proved. Packaging as a biholomorphism and transitivity are proved consequences, independent of Cartan uniqueness and circular-domain rigidity. The ball–polydisc inequivalence follows independently from Schwarz bounds on derivatives and the parallelogram identity in dimension at least two. The source uses the supremum norm and the target uses EuclideanSpace, explicitly. References: [Scheidemann][Scheidemann2005] (2005), Theorem 3.2.1 and Exercise 3.3.4.

Main definitions

• ballParallelComponent: Projection onto the complex line through a, with value zero when a = 0.
• ballMobius: The standard ball involution.
• ballMobiusOpenPartialHomeomorph: The standard involution as an equivalence of open unit balls, with an explicit formula.

Main results

• ballMobius_norm_identity: The metric identity for the standard ball map, expressed without division.
• mapsTo_ballMobius: The standard ball map preserves the unit ball, by its metric identity.
• ballMobius_ballMobius: The ball automorphism is an involution of the unit ball, using the parallel and perpendicular components.
• isBiholomorphic_ballMobius: Both directions of the explicit ball equivalence are holomorphic.
• exists_ball_automorphism: The unit ball is homogeneous under biholomorphic automorphisms: any interior point can be sent to any other, by composing two explicit ball involutions.
• not_exists_isBiholomorphic_polydisc_ball: The Euclidean unit ball and the unit polydisc are not biholomorphic in dimension at least two.

References

• [V. Scheidemann, Introduction to Complex Analysis in Several Variables][Scheidemann2005]

noncomputable def SeveralComplexVariables.ballParallelComponent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a z : E) : E

Projection onto the complex line through a, with value zero when a = 0.

Equations

• SeveralComplexVariables.ballParallelComponent a z = (inner ℂ a z / ↑‖a‖ ^ 2) • a

noncomputable def SeveralComplexVariables.ballMobius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a z : E) : E

The standard ball involution. Mathlib's inner product is linear in its second argument; the scalar in the perpendicular component is sqrt (1 - ‖a‖²).

Equations

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

theorem SeveralComplexVariables.ballMobius_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (z : E) : ballMobius 0 z = -z

At the origin, the standard involution is negation, including dimension zero.

theorem SeveralComplexVariables.ballMobius_apply_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a : E) : ballMobius a 0 = a

The ball involution exchanges zero with its parameter.

theorem SeveralComplexVariables.ballMobius_apply_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a : E) : ballMobius a a = 0

The ball involution sends its parameter to zero.

theorem SeveralComplexVariables.ballMobius_denominator_ne_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {a z : E} (ha : a ∈ Metric.ball 0 1) (hz : z ∈ Metric.ball 0 1) : 1 - inner ℂ a z ≠ 0

The denominator in the ball involution is nonzero on the unit ball.

theorem SeveralComplexVariables.differentiable_ballParallelComponent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a : E) : Differentiable ℂ (ballParallelComponent a)

The projection formula is complex differentiable even for the zero parameter.

theorem SeveralComplexVariables.differentiableOn_ballMobius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {a : E} (ha : a ∈ Metric.ball 0 1) : DifferentiableOn ℂ (ballMobius a) (Metric.ball 0 1)

The explicit ball involution is holomorphic on the unit ball.

theorem SeveralComplexVariables.inner_ballParallelComponent {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a z : E) : inner ℂ a (ballParallelComponent a z) = inner ℂ a z

Orthogonal projection onto the parameter line preserves its inner product with the parameter.

theorem SeveralComplexVariables.norm_ballParallelComponent_sq_mul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a z : E) : ‖ballParallelComponent a z‖ ^ 2 * ‖a‖ ^ 2 = ‖inner ℂ a z‖ ^ 2

The squared norm of the parallel component, in a form valid also for a zero parameter.

theorem SeveralComplexVariables.ballMobius_norm_identity {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {a z : E} (ha : a ∈ Metric.ball 0 1) (hz : z ∈ Metric.ball 0 1) : (1 - ‖ballMobius a z‖ ^ 2) * ‖1 - inner ℂ a z‖ ^ 2 = (1 - ‖a‖ ^ 2) * (1 - ‖z‖ ^ 2)

The metric identity for the standard ball map, expressed without division.

theorem SeveralComplexVariables.mapsTo_ballMobius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {a : E} (ha : a ∈ Metric.ball 0 1) : Set.MapsTo (ballMobius a) (Metric.ball 0 1) (Metric.ball 0 1)

The standard ball map preserves the unit ball, by its metric identity.

theorem SeveralComplexVariables.ballMobius_ballMobius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {a : E} (ha : a ∈ Metric.ball 0 1) (z : E) : z ∈ Metric.ball 0 1 → ballMobius a (ballMobius a z) = z

The ball automorphism is an involution of the unit ball, using the parallel and perpendicular components.

noncomputable def SeveralComplexVariables.ballMobiusOpenPartialHomeomorph {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a : E) (ha : a ∈ Metric.ball 0 1) : OpenPartialHomeomorph E E

The standard involution as an equivalence of open unit balls, with an explicit formula.

Equations

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

theorem SeveralComplexVariables.isBiholomorphic_ballMobius {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (a : E) (ha : a ∈ Metric.ball 0 1) : IsBiholomorphic (ballMobiusOpenPartialHomeomorph a ha)

Both directions of the explicit ball equivalence are holomorphic.

theorem SeveralComplexVariables.exists_ball_automorphism {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {a b : E} (ha : a ∈ Metric.ball 0 1) (hb : b ∈ Metric.ball 0 1) : ∃ (e : OpenPartialHomeomorph E E), IsBiholomorphic e ∧ e.source = Metric.ball 0 1 ∧ e.target = Metric.ball 0 1 ∧ ↑e a = b

The unit ball is homogeneous under biholomorphic automorphisms: any interior point can be sent to any other, by composing two explicit ball involutions.

theorem SeveralComplexVariables.IsBiholomorphic.norm_fderiv_apply_eq_of_unit_ball {A : Type u_2} {B : Type u_3} [NormedAddCommGroup A] [NormedSpace ℂ A] [NormedAddCommGroup B] [NormedSpace ℂ B] {e : OpenPartialHomeomorph A B} (he : IsBiholomorphic e) (hs : e.source = Metric.ball 0 1) (ht : e.target = Metric.ball 0 1) (hfix : ↑e 0 = 0) (x : A) : ‖(fderiv ℂ (↑e) 0) x‖ = ‖x‖

The derivative at zero of an origin-preserving biholomorphism between unit balls preserves norms. Schwarz bounds for the map and its inverse prove both inequalities, without Cartan uniqueness or finite-dimensional assumptions.

theorem SeveralComplexVariables.not_exists_isBiholomorphic_polydisc_ball {ι : Type u_2} [Fintype ι] (hdim : 2 ≤ Fintype.card ι) : ¬∃ (e : OpenPartialHomeomorph (ι → ℂ) (EuclideanSpace ℂ ι)), IsBiholomorphic e ∧ e.source = Metric.ball 0 1 ∧ e.target = Metric.ball 0 1

The Euclidean unit ball and the unit polydisc are not biholomorphic in dimension at least two. Normalize at zero using a ball automorphism; Schwarz's lemma makes the derivative norm-preserving, contradicting the parallelogram identity. This proof is independent of Cartan uniqueness. The dimension hypothesis excludes the singleton and one-variable cases.