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.
After a linear coordinate change, every nonzero germ is regular in the last variable
Statement
Let and let be nonzero. Then there is an invertible complex-linear map and an integer such that the pulled-back germ is regular in the last variable of order .
Facts & Assumptions
Given: A nonzero germ .
On a sufficiently small polydisc around , a holomorphic representative of has an absolutely convergent power-series expansion (A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc).
Such a multivariable power-series expansion has uniquely determined coefficients (The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique).
Regularity in the last variable is the one-variable exact-order condition of Regular holomorphic germs in the last variable.
Proof
Choose a holomorphic representative of on a small polydisc, and expand it by [L1] as Because is nonzero, some coefficient is nonzero. Let be the smallest total degree for which , and put Then is a nonzero homogeneous polynomial of degree .
If for every , then the polynomial function vanishes identically on all of ; applying [L2] to that finite power series would force every coefficient with to be , contradicting step 1.1. Therefore choose with .
Choose an invertible complex-linear map sending the last basis vector to . Along the last axis one then has The bracketed factor is holomorphic and nonzero at because . Hence [L3] makes regular in the last variable of order .
Depends on
- Regular holomorphic germs in the last variable
- A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc
- The coefficients of a convergent multi-indexed power series are its derivative coefficients, hence unique
Used by
- A linear shear makes z₁z₂ regular in z₂ Example
- A nonzero holomorphic hypersurface in complex dimension at least two has no isolated points Theorem
- Riemann extension across a holomorphic hypersurface zero set Theorem
- The ring of holomorphic germs is a UFD Theorem
- The ring of holomorphic germs is Noetherian Theorem
Dependency tree · two levels
30 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, Exercise 6.2.5 (standard reference, not scraped)
- Jaap Korevaar and Jan Wiegerinck, Several Complex Variables, Section 4.1 (standard reference, not scraped)