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 ring of holomorphic germs is Noetherian
Statement
For every integer , the holomorphic germ ring is a Noetherian commutative ring.
Facts & Assumptions
Given: A fixed dimension .
A commutative ring is Noetherian exactly when every ideal is finitely generated (Noetherian commutative rings and modules).
A finite module over a Noetherian ring is Noetherian (Finite modules over Noetherian rings are Noetherian).
Quotienting by a Weierstrass polynomial yields a finite module over the smaller germ ring (A quotient by a Weierstrass polynomial is a finite module over the smaller germ ring).
A nonzero germ becomes regular after a linear coordinate change, and a regular germ admits Weierstrass preparation (After a linear coordinate change, every nonzero germ is regular in the last variable, Weierstrass preparation theorem).
One-variable holomorphic functions factor by their zero order, and units in the germ ring are exactly the nonvanishing germs (The order of a zero is the exponent in its local holomorphic factorization, A germ is a unit exactly when its value at is nonzero, so is local).
Weierstrass division gives a quotient and remainder modulo the prepared polynomial (Weierstrass division theorem).
Proof
The proof is by induction on . For , let be a nonzero proper ideal. Choose of minimal zero order . By [L5], with a unit. If , then , so again by [L5] one has for some holomorphic germ . Since is a unit, , so . Thus every ideal is principal, hence finitely generated. The zero ideal and whole ring are generated by and . Therefore [L1] makes Noetherian.
Assume and that is Noetherian. Let be a proper nonzero ideal. Choose nonzero . By [L4], after a complex-linear coordinate change we may assume that is regular in ; this replaces by an isomorphic ideal under a ring automorphism, so finite generation is unaffected. By [L4] and [L5], write with a unit and a Weierstrass polynomial. Since is an ideal and exists, also lies in .
Let be the quotient map. By [L3], the quotient is a finite -module, so [L2] and the induction hypothesis make it a Noetherian -module. Hence the submodule is generated by finitely many classes with .
Let . Since , there are with Thus so lies in the ideal generated by . Therefore is finitely generated. By [L1], is Noetherian.
Depends on
- Noetherian commutative rings and modules
- Finite modules over Noetherian rings are Noetherian
- A quotient by a Weierstrass polynomial is a finite module over the smaller germ ring
- After a linear coordinate change, every nonzero germ is regular in the last variable
- Weierstrass preparation theorem
- Weierstrass division theorem
- The order of a zero is the exponent in its local holomorphic factorization
- A germ is a unit exactly when its value at $0$ is nonzero, so $\mathcal O_{m,0}$ is local
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
33 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, Theorem 6.4.1 (standard reference, not scraped)
- Jaap Korevaar and Jan Wiegerinck, Several Complex Variables, Theorem 4.5.9 (standard reference, not scraped)