Algebra

Why the ring of germs

Local complex analytic geometry studies zero sets of holomorphic functions near a point. The natural algebraic object for this is the ring of germs $\mathcal{O}_p$ of holomorphic functions at $p \in \mathbb{C}^n$: two functions are identified if they agree near $p$. The ring $\mathcal{O}_p$ is the local ring of the complex manifold $\mathbb{C}^n$ at $p$ in the sense of analytic geometry; its algebraic properties (Noetherian, integral domain, unique factorization) are what make the local theory of analytic varieties, their irreducible components and their singular sets work. This mission formalizes the section of Jiří Lebl's textbook Tasty Bits of Several Complex Variables (jirka.org/scv) that establishes these properties, together with the two tools they rest on, the Weierstrass preparation and division theorems.

The preparation theorem goes back to Weierstrass (published 1886). Rückert (1933) used preparation and division to prove that the ring of convergent power series is Noetherian, the starting point of the algebraic treatment of local analytic geometry.

Setting

A point of $\mathbb{C}^n$ is $z = (z_1, \dots, z_n)$; when a last variable is singled out, $z = (z', z_n)$ with $z' \in \mathbb{C}^{n-1}$. A function on an open set is holomorphic if it is complex differentiable there; $\mathcal{O}(U)$ is the set of holomorphic functions on $U$. A domain is a nonempty connected open set.

A germ at $p$ is an equivalence class of functions defined on neighborhoods of $p$, two functions being equivalent if they agree on some neighborhood of $p$. Germs of complex-valued functions form a commutative ring under pointwise operations of representatives. The ring of germs of holomorphic functions $\mathcal{O}_p = {}_n\mathcal{O}_p$ consists of the germs having a representative holomorphic on a neighborhood of $p$.

For $f$ holomorphic near $p$, write $f(z) = \sum_k f_k(z - p)$ with $f_k$ homogeneous of degree $k$. The order of vanishing $\operatorname{ord}_p f$ is the least $k$ with $f_k \not\equiv 0$, and $\infty$ if $f \equiv 0$.

A Weierstrass polynomial of degree $k \ge 0$ on an open $U \ni 0$ in $\mathbb{C}^{n-1}$ is a monic polynomial in $z_n$,

$$P(z', z_n) = z_n^k + \sum_{\ell=0}^{k-1} c_\ell(z')\, z_n^\ell,$$

with coefficients $c_\ell$ holomorphic on $U$ and $c_\ell(0) = 0$. A polydisc is a product of open discs. For a fixed $z'$, zeros of $z_n \mapsto f(z', z_n)$ are geometrically distinct if they are distinct points; a zero is geometrically unique if it is the only one.

Formalization targets

Goal: Theorem 6.4.2

For every $n$ and $p \in \mathbb{C}^n$,

$$\mathcal{O}_p \text{ is a unique factorization domain:}$$

it is an integral domain, and up to multiplication by units and permutation every nonzero nonunit has a unique factorization into irreducible elements of $\mathcal{O}_p$.

Milestones

In attack order:

1. Theorem 6.2.3 (Weierstrass preparation). If $f \in \mathcal{O}(U)$, $0 \in U$, $f(0) = 0$, and $z_n \mapsto f(0, z_n)$ has order of vanishing $k \ge 1$ at $0$, then on some open polydisc $V = V' \times D$ with $0 \in V \subset U$,

$$f(z', z_n) = u(z', z_n)\, P(z', z_n)$$

with $u \in \mathcal{O}(V)$ nowhere zero and $P$ a Weierstrass polynomial of degree $k$ with coefficients holomorphic in $V'$ whose zeros in $z_n$ lie in $D$ for all $z' \in V'$; $u$ and $P$ are unique. 2. Theorem 6.2.5 (Weierstrass division). For $f$ holomorphic near $0$ and $P$ a Weierstrass polynomial of degree $k \ge 1$, there are a neighborhood $V$ of $0$ and unique $q, r \in \mathcal{O}(V)$, $r$ a polynomial in $z_n$ of degree less than $k$, with $f = qP + r$ on $V$. 3. Proposition 6.3.1. On domains $U' \times D$, if for every $z' \in U'$ the function $z_n \mapsto f(z', z_n)$ has a geometrically unique zero $\alpha(z') \in D$, then $\alpha$ is holomorphic in $U'$. 4. Theorem 6.3.3 (discriminant). For $D$ a bounded domain, $U'$ a domain, $f \in \mathcal{O}(U' \times D)$ whose zero set has no limit points on $U' \times \partial D$, there are $m$ and a holomorphic $\Delta \not\equiv 0$ on $U'$ such that $z_n \mapsto f(z', z_n)$ has exactly $m$ geometrically distinct zeros in $D$ for $\Delta(z') \ne 0$ and fewer than $m$ for $\Delta(z') = 0$. 5. Theorem 6.4.1. $\mathcal{O}_p$ is Noetherian.

Significance

The preparation theorem reduces a holomorphic function near a point, after a unit, to a polynomial in one variable over the ring of functions of the others; the division theorem is division with remainder by such a polynomial. Together they turn $\mathcal{O}_0$ in $n$ variables into an object controlled by the polynomial ring $\mathcal{O}_0[z_n]$ in $n - 1$ variables, and that is how both the Noetherian property and unique factorization are proved. Unique factorization gives the decomposition of a germ of a hypersurface into irreducible components; the Noetherian property says that every germ of an analytic variety is cut out by finitely many functions. Proposition 6.3.1 and Theorem 6.3.3 describe how the zeros of $z_n \mapsto f(z', z_n)$ move with $z'$, the input to the study of hypervarieties in the following sections.

The results are classical. The book proves them, leaving some steps as exercises: uniqueness in the division theorem (Exercise 6.2.10), the one-variable cases of 6.4.1 and 6.4.2 (Exercises 6.4.2, 6.4.6), and the irreducibility step in 6.4.2 (Exercise 6.4.7). Mathlib has the algebra (Noetherian rings, unique factorization monoids, Hilbert's basis theorem, the Gauss lemma for polynomial rings), germs along filters, and one-variable complex analysis. The platform has the Weierstrass preparation and division theorems for formal power series over complete local rings. None of the statements of this mission about convergent germs and holomorphic functions has a machine-checked proof.

Difficulty

The statements concern convergent objects, and the algebra alone does not see convergence. The formal preparation and division theorems produce a factorization or a quotient as formal power series; they do not say that the output converges, nor that it is holomorphic on a fixed neighborhood, nor where the zeros of the Weierstrass polynomial lie. Likewise, the formal power series ring is known to be a Noetherian UFD, but $\mathcal{O}_p$ is a proper subring and neither property passes to subrings. The coefficients of the Weierstrass polynomial are built from the zeros of $z_n \mapsto f(z', z_n)$, which in general cannot be chosen continuously in $z'$ (the two square roots of $z_1$ already show this), so the holomorphy of the coefficients cannot come from the zeros one at a time.

For the goal, the induction on $n$ requires identifying $\mathcal{O}_0$ in $n - 1$ variables, its polynomial ring, and a subring of $\mathcal{O}_0$ in $n$ variables, and moving between germs and representatives on explicit neighborhoods. A linear change of coordinates is needed to reach the hypothesis of the preparation theorem, so invariance of $\mathcal{O}_p$ under such changes is also part of the work.

Formalization scope

• $\mathbb{C}^n$ is Fin n → ℂ; where a last variable is singled out, $\mathbb{C}^{n-1} \times \mathbb{C}$ is (Fin d → ℂ) × ℂ with $d = n - 1$, so $d = 0$ is the case $n = 1$. Holomorphic on an open set is DifferentiableOn ℂ, which agrees with the book's Definition 1.1.2 on open sets.
• $\mathcal{O}_p$ is GermRing n p: the subring of Mathlib's germ ring (𝓝 p).Germ ℂ of germs with a representative complex-differentiable at every point near $p$. The goal produces the IsDomain structure and asserts UniqueFactorizationMonoid; Theorem 6.4.1 is IsNoetherianRing.
• Ruled out: replacing $\mathcal{O}_p$ by the ring of all germs of functions (not a domain) or by formal power series MvPowerSeries (Fin n) ℂ. Both change the theorem; convergence is the whole point.
• The order of vanishing is ℕ∞-valued: the least $k$ with nonzero $k$-th derivative at $p$, and $\infty$ if there is none.
• A Weierstrass polynomial is given by its coefficient tuple $c_0, \dots, c_{k-1}$; the polydisc $V' \times D$ of Theorem 6.2.3 is a coordinatewise polydisc with positive radii times an open disc, both centers arbitrary as in the book. "All $k$ zeros lie in $D$" is stated as "every zero lies in $D$", equivalent for a monic polynomial of degree $k$. Uniqueness in 6.2.3 and 6.2.5 is uniqueness on the $V$ produced.
• In Theorem 6.3.3 zeros are counted as distinct points with Set.encard. The book writes $m \in \mathbb{N}$ with $\mathbb{N} = \{1, 2, \dots\}$; the statement allows $m = 0$, since for $f$ without zeros no $m \ge 1$ can satisfy the conclusion.

A complete development needs the one-variable argument principle and Cauchy integral formula with holomorphic parameters, Newton's identities, Radó's theorem (for 6.3.3), Hilbert's basis theorem and the Gauss lemma (in Mathlib), and the identification of $\mathcal{O}_0$ in $n - 1$ variables with a subring of $\mathcal{O}_0$ in $n$ variables. A general API for rings of holomorphic germs and their changes of coordinates is reusable in the next mission of this series (hypervarieties and their singular sets); contributions of it as standalone lemmas are welcome.

Selected references

• J. Lebl, Tasty Bits of Several Complex Variables, version 4.4, 2026, Chapter 6, §§6.1–6.4. https://www.jirka.org/scv/scv.pdf
• W. Rückert, "Zum Eliminationsproblem der Potenzreihenideale", Mathematische Annalen 107 (1933).
• R. C. Gunning and H. Rossi, Analytic Functions of Several Complex Variables, Prentice-Hall, 1965; reprint AMS Chelsea, 2009, Chapter II.