Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-08-28
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 m,n≥1, let U⊆Cm be open, let F:U→Cn be holomorphic, and suppose the complex rank of DF is the constant value r on a neighbourhood of a∈U. Then there are biholomorphic coordinate changes α near a and β near F(a) such that

β∘F∘α−1(u,v)=(u,0)

for (u,v)∈Cr×Cm−r near 0. Empty blocks are omitted when r=0, r=m, or r=n.

Facts & Assumptions

Given: The holomorphic map F:U→Cn, the point a∈U, and a neighbourhood on which rank⁡CDF=r.

[L1]

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).

[L2]

Components of a holomorphic map are holomorphic, and holomorphic scalar functions are separately holomorphic on coordinate discs (A map into Cn is holomorphic exactly when each of its components is, A holomorphic function of several variables is continuous and separately holomorphic).

[L3]

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

technique · direct
1.1givenL1construct

After composing on the source and target with coordinate permutations, we may assume that the first r×r minor of JCF(a) is invertible. Write z=(x,y)∈Cr×Cm−r,F(z)=(F′(x,y),F′′(x,y))∈Cr×Cn−r, and define α(x,y):=(F′(x,y),y). The complex Jacobian of α at a is block triangular with diagonal blocks ∂xF′(a) and Im−r, so it is invertible. Hence [L1] makes α biholomorphic after shrinking around a.

2.1step 1.1algebra

Set G:=F∘α−1. Because α−1(u,v) has second block v, one has G(u,v)=(u,h(u,v)) for a holomorphic map h into Cn−r. Since DG=DF∘Dα−1 and Dα−1 is invertible, rank⁡DG is also r on the shrunken neighbourhood.

3.1step 2.1algebra

In the Jacobian of G, the first r output coordinates are exactly the coordinates u1,…,ur, so the first r rows already contain the r×r identity block. If some partial derivative ∂hk/∂vj were nonzero at a point, adjoining the corresponding row and vj column would create an (r+1)×(r+1) minor with nonzero determinant there, contradicting rank⁡DG=r. Therefore every ∂hk/∂vj vanishes on the neighbourhood.

4.1step 3.1L2L3

Fix u, fix all v-coordinates except vj, and fix a component hk. By [L2], the slice λ⟼hk(u,v1,…,vj−1,λ,vj+1,…,vm−r) is holomorphic on a disc, and step 3.1 says its derivative is identically 0. Hence [L3] makes it constant. Repeating this for each j shows that h(u,v) is independent of v; writing ϕ(u):=h(u,0), [L2] makes ϕ holomorphic and gives h(u,v)=ϕ(u).

5.1step 1.1step 4.1constructalgebra∎

Define the target shear β(ξ,η):=(ξ,η−ϕ(ξ)). Its inverse is (ξ,η)↦(ξ,η+ϕ(ξ)), so β is biholomorphic near F(a). Using step 4.1, β∘F∘α−1(u,v)=β(u,ϕ(u))=(u,0). This is the claimed normal form, and when one of the dimensions r, m−r, or n−r is 0 the same formula is read with the corresponding block omitted.

Depends on

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