ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

$k [x, y] / (x y)$ and $Z [x] / (x^{2} - 2)$ are Noetherian without classifying their ideals

Example

Let $k$ be a field. The rings

$k [x, y] / (x y) and Z [x] / (x^{2} - 2)$

are Noetherian (The quotient ring $R / I$ with $(r + I) (s + I) = r s + I$ ). The argument sees only that each is a quotient of a polynomial ring in finitely many variables over a Noetherian base ring; it inspects neither ring further, and in particular it does not depend on whether the ring has zero divisors, which the first one does.

Facts & Assumptions

Given: A field $k$ , the polynomial rings $k [x, y]$ and $Z [x]$ , and the ideals $(x y) \subseteq k [x, y]$ and $(x^{2} - 2) \subseteq Z [x]$ .

[L1]

For an ideal $I$ of a ring $R$ the quotient ring $R / I$ has the additive cosets of $I$ as elements and multiplication $(r + I) (s + I) = r s + I$ (The quotient ring $R / I$ with $(r + I) (s + I) = r s + I$ ).

[L2]

Polynomial rings in finitely many commuting indeterminates are defined by $R [x_{1}, \dots, x_{0}] : = R$ and $R [x_{1}, \dots, x_{n + 1}] : = R [x_{1}, \dots, x_{n}] [x_{n + 1}]$ (Polynomial rings in finitely many commuting indeterminates by iteration).

[L3]

A commutative $R$ -algebra is of finite type over $R$ exactly when it is isomorphic as an $R$ -algebra to a quotient $R [x_{1}, \dots, x_{n}] / a$ for some $n \in N$ and some ideal $a$ (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

[L4]

Every field $K$ is a Noetherian ring, and so is $Z$ (Fields and $Z$ are Noetherian, and so are their polynomial rings in finitely many variables).

[L5]

Every commutative algebra of finite type over a Noetherian commutative ring is a Noetherian ring (Every algebra of finite type over a Noetherian ring is a Noetherian ring).

[L6]

For commutative rings $R, S$ , a unital ring homomorphism $φ ⁣ : R \to S$ and $s \in S$ , there is a unique unital ring homomorphism $R [x] \to S$ extending $φ$ on constants and sending $x$ to $s$ (Universal property of $R [x]$ : a coefficient homomorphism and the image of $x$ determine a unique ring homomorphism).

[L7]

For $S \subseteq R$ , $(S)$ is the intersection of all two-sided ideals containing $S$ , so $S \subseteq (S)$ ; $({a})$ is written $(a)$ (The ideal generated by a subset and principal ideals).

[L8]

In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ (In a commutative ring, $(S)$ consists of finite sums $\sum r_{i} s_{i}$ , and $(a) = R a$ ).

Verification

technique · direct

1.1L1L2L3L7given

Each ring is a quotient of a polynomial ring in finitely many indeterminates over its base ring: $k [x, y]$ is $k [x_{1}, x_{2}]$ after renaming the indeterminates, and $Z [x]$ is $Z [x_{1}]$ . Being such a quotient is exactly the condition of being an algebra of finite type over that base ring, so $k [x, y] / (x y)$ is of finite type over $k$ and $Z [x] / (x^{2} - 2)$ is of finite type over $Z$ .

1.2L4given

The base rings $k$ and $Z$ are Noetherian.

2.1L5step 1.1step 1.2

An algebra of finite type over a Noetherian commutative ring is a Noetherian ring, so both displayed rings are Noetherian.

3.1L1L6L7L8step 1.1step 2.1∎

The first ring has zero divisors, and the argument above never asked. Let $π$ denote the quotient map $k [x, y] \to k [x, y] / (x y)$ . Evaluating at $0$ in the last indeterminate gives a ring homomorphism $ε ⁣ : k [x] [y] \to k [x]$ that fixes $k [x]$ and sends $y$ to $0$ . Every element of $(x y)$ is $f \cdot x y$ with $f \in k [x, y]$ , and $ε (f \cdot x y) = ε (f) ε (x) ε (y) = ε (f) x \cdot 0 = 0$ , whereas $ε (x) = x \neq 0$ ; so $x \notin (x y)$ and $π (x) \neq 0$ . Exchanging the roles of the two indeterminates gives $π (y) \neq 0$ in the same way. Yet $π (x) π (y) = π (x y) = 0$ .

Remarks

The same conclusion follows from the Hilbert basis theorem plus the quotient theorem, since $k [x, y]$ and $Z [x]$ are Noetherian by If $R$ is Noetherian then $R [x_{1}, \dots, x_{n}]$ is Noetherian for every $n \in N$ and a quotient of a Noetherian ring is Noetherian by Every quotient and every localisation of a Noetherian ring is Noetherian. The route through Every algebra of finite type over a Noetherian ring is a Noetherian ring packages both steps and is the form later pages use.
Nothing here describes the ideals. For $k [x, y] / (x y)$ the ideals can be listed with more work, and for $Z [x] / (x^{2} - 2)$ they can be studied by number-theoretic means; neither is needed, and neither is claimed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 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

J. S. Milne, A Primer of Commutative Algebra, v4.03, §3 Theorem 3.7 (standard reference, not scraped)
A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., (16.12) (standard reference, not scraped)

k[x,y]/(xy)k[x,y]/(xy) and Z[x]/(x2−2)Z[x]/(x2−2) are Noetherian without classifying their ideals