LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The determinant quotient $\det g_{Ω} / K_{Ω}$ is a biholomorphic invariant

Statement

Assume the Axiom of Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $Ω, Ω^{'} \subseteq C^{m}$ be bounded domains, let $F : Ω \to Ω^{'}$ be a biholomorphism with complex Jacobian $D F (z)$ , and let $g_{Ω} (z)$ be the matrix of the Bergman metric form in the one-based coordinate aliases of The Levi form and strict plurisubharmonicity. Then, for every $z \in Ω$ ,

$\det g_{Ω} (z) = ∣ \det D F (z) ∣^{2} \det g_{Ω^{'}} (F (z)), K_{Ω} (z, z) = ∣ \det D F (z) ∣^{2} K_{Ω^{'}} (F (z), F (z)),$

and consequently

$\frac{\det g_{Ω} (z)}{K_{Ω} (z, z)} = \frac{\det g_{Ω^{'}} (F (z))}{K_{Ω^{'}} (F (z), F (z))} (z \in Ω) .$

If each quotient is constant on its domain, then the two constants are equal. (For $m \geq 2$ these quotients are the invariants that distinguish the ball metric from the polydisc metric, but constancy is not claimed here.)

Facts & Assumptions

[A1]

The only choice assumption is ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), inherited through the Bergman metric, kernel and transformation suppliers; no full Axiom of Choice is used.

[F1]

The Bergman metric form of a bounded domain is the Hermitian form $g_{Ω} (z) (X, Y) = \sum_{j, k = 1}^{m} (g_{Ω})_{j \overset{ˉ}{k}} (z) X_{j} \overline{Y_{k}}$ with matrix $(g_{Ω})_{j \overset{ˉ}{k}} (z)$ , and $B_{Ω}^{2} (z; X) = g_{Ω} (z) (X, X)$ (The Bergman metric form on a bounded domain, The Levi form and strict plurisubharmonicity).

[F2]

A biholomorphism $F : Ω \to Ω^{'}$ of bounded domains satisfies $g_{Ω} (z) (X, Y) = g_{Ω^{'}} (F (z)) (D F (z) X, D F (z) Y)$ for all $z, X, Y$ (The Bergman metric is positive definite on bounded domains and biholomorphically invariant).

[F3]

A biholomorphism $F$ satisfies $K_{Ω} (z, w) = J_{F} (z) K_{Ω^{'}} (F (z), F (w)) \overline{J_{F} (w)}$ with $J_{F} = \det D F \neq 0$ ; in particular the diagonal kernel law $K_{Ω} (z, z) = ∣ \det D F (z) ∣^{2} K_{Ω^{'}} (F (z), F (z))$ holds (Transformation law of the Bergman kernel under a biholomorphism).

[F4]

On a bounded domain, $K_{Ω} (z, z) > 0$ for every $z$ (Smoothness of the Bergman kernel and positivity of its diagonal on bounded domains).

[F5]

For $A \in M_{n} (R)$ over a commutative ring, $\det (A) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} a_{σ (i), i}$ , and transposition leaves the determinant unchanged; the determinant is multiplicative: $\det (A B) = \det A \det B$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix, Finite rectangular matrices over a commutative ring, their entries, rows and columns, For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ , For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ ).

[F6]

Complex conjugation is a field automorphism of $C$ fixing the rationals, so it commutes with finite sums and products of complex numbers (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F7]

Matrices multiply by the usual row-column rule, and $A^{T}$ has entries $(A^{T})_{j i} = a_{i j}$ (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose, Finite rectangular matrices over a commutative ring, their entries, rows and columns).

Proof

technique · direct, comparing Hermitian matrices by their quadratic forms and taking determinants

Given: ${A C}_{ω}$ , bounded domains $Ω, Ω^{'}$ , a biholomorphism $F$ , a point $z \in Ω$ , and $J : = D F (z)$ .

1.1A1F1F2F7algebra

Put $G : = g_{Ω^{'}} (F (z))$ and $H : = g_{Ω} (z)$ , with entries $G_{l m}$ and $H_{j k}$ in the one-based aliases. By [F1] and [F2], for all $X, Y \in C^{m}$ , $\sum_{j, k} H_{j k} X_{j} \overline{Y_{k}} = \sum_{l, m} G_{l m} (J X)_{l} \overline{(J Y)_{m}} = \sum_{j, k} (\sum_{l, m} \overline{J_{m k}} G_{l m} J_{l j}) X_{j} \overline{Y_{k}} .$ Since the Hermitian form is determined by its coefficients, $H_{j k} = \sum_{l, m} \overline{J_{m k}} G_{l m} J_{l j}$ , which is the $(j, k)$ entry of $J^{T} G \overline{J}$ because $(J^{T} G \overline{J})_{j k} = \sum_{l, m} J_{l j} G_{l m} \overline{J_{m k}}$ by [F7]; in matrix notation $g_{Ω} (z) = J^{T} g_{Ω^{'}} (F (z)) \overline{J}$ .

1.2F5F6algebra

Conjugation is a field automorphism of $C$ [F6] applied entrywise to the Leibniz sum of [F5] gives $\det (\overline{J}) = \overline{\det J}$ ; since transposition leaves determinants unchanged [F5], $\det ({\overline{J}}^{T}) = \overline{\det J}$ .

2.1F3F5step 1.1step 1.2

Taking determinants in the matrix identity of step 1.1 and using multiplicativity and transposition invariance [F5] gives $\det g_{Ω} (z) = \det (J) \det g_{Ω^{'}} (F (z)) \det (\overline{J}) = \det J \det g_{Ω^{'}} (F (z)) \overline{\det J} = ∣ \det J ∣^{2} \det g_{Ω^{'}} (F (z))$ , the first displayed identity. The second displayed identity is the diagonal kernel law of [F3] with $J = D F (z)$ , whose determinant is nonzero.

3.1F3F4step 2.1∎

By [F4] the diagonal values $K_{Ω} (z, z)$ and $K_{Ω^{'}} (F (z), F (z))$ are positive, and $∣ \det D F (z) ∣^{2} > 0$ by [F3]; dividing the two identities of step 2.1 by each other and cancelling the common positive factor $∣ \det D F (z) ∣^{2}$ gives the displayed identity of the quotients for every $z \in Ω$ . If each quotient is constant on its domain, evaluating the identity at any $z$ shows the two constants are equal.

Depends on

Used by

Dependency tree · two levels

87 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Zbigniew Błocki, The Bergman Kernel and Metric (lecture notes) (standard reference, not scraped)

The determinant quotient det⁡gΩ/KΩdetgΩ​/KΩ​ is a biholomorphic invariant