ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-09-01

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.

A Noetherian domain can have a completion that is not a domain

Example

Let $k$ be a field of characteristic different from $2$ , and set

A : = k [x, y]_{(x, y)} / (y^{2} - x^{2} - x^{3}) .

Then $A$ is a Noetherian local domain, but its completion at the maximal ideal is not a domain.

Facts & Assumptions

Given: A field $k$ with $char (k) \neq 2$ .

[L1]

Quotients and localizations of Noetherian rings are Noetherian (Every quotient and every localisation of a Noetherian ring is Noetherian).

[L2]

Completion of a Noetherian ring is Noetherian (Completion of a Noetherian ring is Noetherian).

Verification

technique · direct

1.1

The polynomial ring $k [x, y]$ is Noetherian, so [L1] makes $k [x, y]_{(x, y)}$ and its quotient $A$ Noetherian. The quotient is local because it is a quotient of the local ring $k [x, y]_{(x, y)}$ .

L1algebra

1.2

In the formal power-series ring $k [⁣ [x] ⁣]$ , the binomial series gives an element $u = (1 + x)^{1 / 2} \in k [⁣ [x] ⁣]$ with $u^{2} = 1 + x$ . Consequently, in $k [⁣ [x, y] ⁣]$ , $y^{2} - x^{2} - x^{3} = (y - x u) (y + x u) .$ Neither factor is a unit because each has zero constant term.

givenalgebra

2.1

The polynomial $f (y) : = y^{2} - x^{2} - x^{3} = y^{2} - x^{2} (1 + x)$ is irreducible in $k (x) [y]$ : it is quadratic in $y$ , so reducibility would force $x^{2} (1 + x)$ to be a square in $k (x)$ , but $1 + x$ is not a square in $k (x)$ because its divisor has the simple zero $x = - 1$ . Hence the ideal $(f)$ is prime in $k [x, y]$ , and localizing preserves primality. Therefore $A$ is a domain.

step 1.1algebra

2.2

For every $n$ , localization away from $(x, y)$ does not change the quotient modulo $(x, y)^{n}$ , so $A / m^{n} ≅ k [x, y] / ((x, y)^{n}, f) .$ Passing to the inverse limit identifies the completion coefficientwise with $\hat{A} ≅ k [⁣ [x, y] ⁣] / (f) .$ Let $α, β$ be the images of $y - x u$ and $y + x u$ in $\hat{A}$ . Their product is $0$ by step 1.2. If $α = 0$ , then in the domain $k [⁣ [x, y] ⁣]$ one would have $(y - x u) = (y - x u) (y + x u) h$ for some $h$ , hence $1 = (y + x u) h,$ which is impossible because $y + x u$ lies in the maximal ideal. So $α \neq 0$ , and similarly $β \neq 0$ . Thus $\hat{A}$ has nonzero zero divisors and is not a domain.

L2step 1.2algebra

3.1

Therefore a Noetherian local domain can have a completion that is not a domain.

step 2.1step 2.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., completion chapter pathology example (standard reference, not scraped)
The Stacks Project, completion chapter background (standard reference, not scraped)