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,n1, let UCm be open, let F:UCn be holomorphic, and suppose the complex rank of DF is the constant value r on a neighbourhood of aU. Then there are biholomorphic coordinate changes α near a and β near F(a) such that

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

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

Facts & Assumptions

Given: The holomorphic map F:UCn, the point aU, and a neighbourhood on which rankCDF=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.1

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×Cmr,F(z)=(F(x,y),F(x,y))Cr×Cnr, and define α(x,y):=(F(x,y),y). The complex Jacobian of α at a is block triangular with diagonal blocks xF(a) and Imr, so it is invertible. Hence [L1] makes α biholomorphic after shrinking around a.

givenL1construct
2.1

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 Cnr. Since DG=DFDα1 and Dα1 is invertible, rankDG is also r on the shrunken neighbourhood.

step 1.1algebra
3.1

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 rankDG=r. Therefore every hk/vj vanishes on the neighbourhood.

step 2.1algebra
4.1

Fix u, fix all v-coordinates except vj, and fix a component hk. By [L2], the slice λhk(u,v1,,vj1,λ,vj+1,,vmr) 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).

step 3.1L2L3
5.1

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, mr, or nr is 0 the same formula is read with the corresponding block omitted.

step 1.1step 4.1constructalgebra

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