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 holomorphic constant-rank theorem
Statement
Let , let be open, let be holomorphic, and suppose the complex rank of is the constant value on a neighbourhood of . Then there are biholomorphic coordinate changes near and near such that
for near . Empty blocks are omitted when , , or .
Facts & Assumptions
Given: The holomorphic map , the point , and a neighbourhood on which .
If a holomorphic map has an invertible square complex Jacobian minor at a point, the corresponding coordinate-augmented map is locally biholomorphic (The holomorphic inverse function theorem in several complex variables).
Components of a holomorphic map are holomorphic, and holomorphic scalar functions are separately holomorphic on coordinate discs (A map into is holomorphic exactly when each of its components is, A holomorphic function of several variables is continuous and separately holomorphic).
A one-variable holomorphic function with zero derivative on a domain is constant (A holomorphic function with zero derivative on a domain is constant).
Proof
After composing on the source and target with coordinate permutations, we may assume that the first minor of is invertible. Write and define The complex Jacobian of at is block triangular with diagonal blocks and , so it is invertible. Hence [L1] makes biholomorphic after shrinking around .
Set Because has second block , one has for a holomorphic map into . Since and is invertible, is also on the shrunken neighbourhood.
In the Jacobian of , the first output coordinates are exactly the coordinates , so the first rows already contain the identity block. If some partial derivative were nonzero at a point, adjoining the corresponding row and column would create an minor with nonzero determinant there, contradicting . Therefore every vanishes on the neighbourhood.
Fix , fix all -coordinates except , and fix a component . By [L2], the slice is holomorphic on a disc, and step 3.1 says its derivative is identically . Hence [L3] makes it constant. Repeating this for each shows that is independent of ; writing , [L2] makes holomorphic and gives .
Define the target shear Its inverse is , so is biholomorphic near . Using step 4.1, This is the claimed normal form, and when one of the dimensions , , or is the same formula is read with the corresponding block omitted.
Depends on
- Holomorphic maps $\mathbb{C}^m \to \mathbb{C}^n$ and the complex Jacobian matrix
- The holomorphic inverse function theorem in several complex variables
- The holomorphic implicit function theorem
- The Euclidean constant-rank normal form
- A map into $\mathbb{C}^n$ is holomorphic exactly when each of its components is
- A holomorphic function of several variables is continuous and separately holomorphic
- A holomorphic function with zero derivative on a domain is constant
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
44 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
- Jiří Lebl, Tasty Bits of Several Complex Variables, Chapter 5 (standard reference, not scraped)
- Jaap Korevaar and Jan Wiegerinck, Several Complex Variables, Sections 4.2 and 5.2 (standard reference, not scraped)