CorollaryStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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 complex Jacobian determinant of a composite of equidimensional holomorphic maps is the product

Statement

Let $m \geq 1$ , let $U, V \subseteq C^{m}$ be open, let $F : U \to V$ be holomorphic at $a \in U$ and let $G : V \to C^{m}$ be holomorphic at $F (a)$ . Then $J_{C} F (a)$ , $J_{C} G (F (a))$ and $J_{C} (G \circ F) (a)$ are $m \times m$ matrices over $C$ and

$\det J_{C} (G \circ F) (a) = \det J_{C} G (F (a)) \cdot \det J_{C} F (a) .$

Consequently, if $F$ is holomorphic on $U$ with a holomorphic two-sided inverse $F^{- 1} : V \to U$ , then $\det J_{C} F (a) \neq 0$ for every $a \in U$ .

Facts & Assumptions

Given: Equidimensional holomorphic maps $F$ and $G$ as above.

[L1]

For holomorphic $F$ at $a$ and $G$ at $F (a)$ , the composite is holomorphic at $a$ and $J_{C} (G \circ F) (a) = J_{C} G (F (a)) J_{C} F (a)$ (The composite of holomorphic maps is holomorphic and its complex Jacobian is the product).

[L2]

$J_{C} F (a)$ is the matrix of the $C$ -linear differential in the standard bases, an $n \times m$ matrix over $C$ (Holomorphic maps $C^{m} \to C^{n}$ and the complex Jacobian matrix, Coordinate columns $[v]_{B}$ and matrices $[T]_{B}^{C}$ of linear maps relative to ordered bases).

[L3]

For $n \geq 1$ and $A, B \in M_{n} (R)$ over a commutative ring, $\det (A B) = \det (A) \det (B)$ (For same-sized finite square matrices over a commutative ring, $\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).

[L4]

Matrices over a commutative ring and their product are those of Finite rectangular matrices over a commutative ring, their entries, rows and columns, and $C$ is a field, hence a commutative ring ( $C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ ).

[L5]

If $A \in M_{n} (R)$ is invertible over a commutative ring then $\det (A)$ is a unit, with inverse $\det (A^{- 1})$ (An invertible square matrix over a commutative ring has unit determinant).

Proof

technique · direct

1.1

Since the source and target dimensions are all $m$ , [L2] makes each of the three Jacobians an $m \times m$ matrix over $C$ , which is a commutative ring by [L4].

givenL2L4

2.1

By [L1] the composite Jacobian is the matrix product $J_{C} G (F (a)) J_{C} F (a)$ , so [L3] applied over $C$ gives $\det J_{C} (G \circ F) (a) = \det J_{C} G (F (a)) \det J_{C} F (a)$ .

step 1.1L1L3L4

3.1

If $F$ has a holomorphic two-sided inverse $F^{- 1}$ , applying step 2.1 to $G = F^{- 1}$ gives $\det J_{C} F^{- 1} (F (a)) \det J_{C} F (a) = \det J_{C} (i d) (a) = 1$ , since the identity map is holomorphic with identity differential by [L2]; so $\det J_{C} F (a)$ is a unit of the field $C$ , in particular nonzero, as [L5] also records.

step 2.1L2L4L5∎

Depends on

Used by

The complex Jacobian and its determinant for (z₀z₁, z₀+z₁) Example

Dependency tree · two levels

48 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

J. Lebl, Tasty Bits of Several Complex Variables, §1.3 (standard reference, not scraped)