Alphabeta Math
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.

The subalgebra k[x,xy,xy2,…] of k[x,y] is not Noetherian

Example

Let k be a field and work inside k[x,y]=k[x][y] (Polynomial rings in finitely many commuting indeterminates by iteration). Put

A  :=  k+x k[x,y]  =  { c+xf  :  c∈k, f∈k[x,y] }.

Then A is a subring of k[x,y] containing k, and it is the subalgebra k[x,xy,xy2,…] generated over k by the elements xyi for i∈N. The ideal a of A generated by those elements is x k[x,y], and it is not finitely generated, so A is not Noetherian — even though k[x,y] is.

Two consequences follow: a subring of a Noetherian ring need not be Noetherian, and a subalgebra of an algebra of finite type over a field need not itself be of finite type.

Facts & Assumptions

Given: A field k, the ring k[x,y]=k[x][y], the subset A=k+xk[x,y] of it, and the elements xyi for i∈N. Coefficients are read in the iterated form: an element of k[x][y] is a finitely supported family of elements of k[x], indexed by the exponent of y.

[L1]

A subset S of a ring is a subring when 1∈S and S is closed under addition, additive inverses and multiplication; it is then a ring with the same zero and identity (Subring: a subset containing 1R and closed under addition, additive inverses and multiplication).

[L2]

R[x] is the set of finitely supported functions N→R with (a+b)i=ai+bi and (ab)i=∑j+k=iajbk (The polynomial ring over a commutative ring as finitely supported coefficient sequences with convolution).

[L3]

Polynomial rings in finitely many indeterminates are defined by R[x1,…,x0]:=R and R[x1,…,xn+1]:=R[x1,…,xn][xn+1] (Polynomial rings in finitely many commuting indeterminates by iteration).

[L4]

For S⊆R, (S) is the intersection of all two-sided ideals containing S, so S⊆(S) (The ideal generated by a subset and principal ideals).

[L5]

In a commutative ring, (S) consists of finite sums ∑risi, and (a)=Ra; the empty sum is included and equals 0 (In a commutative ring, (S) consists of finite sums ∑risi, and (a)=Ra).

[L8]

If R is a Noetherian commutative ring then R[x1,…,xn] is Noetherian for every n∈N (If R is Noetherian then R[x1,…,xn] is Noetherian for every n∈N).

[L9]

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).

[L10]

R[a1,…,an] is the smallest subring of A containing the image of R and a1,…,an, and A is of finite type over R when it equals such a subring for a finite list (Subalgebra generated by a subset, algebras of finite type, and module-finite algebras).

Verification

technique · direct
1.1L1L2L3given

A is a subring of k[x,y]. It contains 1=1+x⋅0; it is closed under addition and additive inverses because k and xk[x,y] both are; and (c+xf)(c′+xf′)=cc′+x(cf′+c′f+xff′) lies in A.

1.2L1L3L10given

A=k[x,xy,xy2,…], the smallest subring of k[x,y] containing k and every xyi. That subring is contained in A because A is a subring containing k and each xyi=0+x⋅yi. Conversely every c+xf lies in it: expanding f as a k-linear combination of monomials xayb gives xf as a k-linear combination of xa+1yb=xa⋅(xyb), and each of x=xy0 and xyb is one of the listed generators.

2.1L4L5step 1.1

The ideal a of A generated by {xyi:i∈N} equals x k[x,y]. An element of a is a finite sum ∑jaj xynj with aj∈A, which lies in x k[x,y]; conversely, for f∈k[x,y] expanded as a k-linear combination of monomials xayb, the element xf is the corresponding combination of xa⋅(xyb) with xa∈A, hence lies in a.

3.1L2L4L5step 2.1

Suppose a=(f1,…,fm) as an ideal of A, with m∈N and fj∈a. Since x=xy0∈a and x≠0, the ideal a is nonzero, so at least one fj is nonzero; let N∈N be an index beyond which every fj has vanishing y-coefficients, that is, the yb-coefficient of every fj is 0 for b>N. Any element of (f1,…,fm) is ∑jajfj with aj∈A; writing aj=cj+xhj with cj∈k and hj∈k[x,y], and using fj∈x k[x,y] from step 2.1, this element equals ∑jcjfj+x2 g for some g∈k[x,y]. Its yN+1-coefficient is therefore the sum of ∑jcj⋅0=0 and an element of x2k[x], hence lies in x2k[x].

4.1L2L6step 3.1

But xyN+1 lies in a and its yN+1-coefficient is x, which is not in x2k[x]: every element of x2k[x] has vanishing coefficient at x1, whereas x has coefficient 1≠0 there. So xyN+1∉(f1,…,fm), contradicting a=(f1,…,fm). Hence a is not finitely generated and A is not Noetherian.

5.1L7L8L9L10step 4.1∎

The ambient ring k[x,y] is Noetherian, since k is a field and a polynomial ring in finitely many variables over a Noetherian ring is Noetherian. So the Noetherian ring k[x,y] has the non-Noetherian subring A. And A is not of finite type over k: an algebra of finite type over the Noetherian ring k would be Noetherian, which A is not, while k[x,y] itself is of finite type over k.

Remarks

  • Where finite generation actually fails. The ideal a needs the elements xyi for arbitrarily large i: multiplying by an element of A either scales by a constant, which cannot raise the y-exponent, or introduces a factor x, which pushes the term into x2k[x,y] and out of reach of the coefficient examined in step 3.1.

  • The failure is not a failure of the ambient ring. k[x,y] satisfies every chain condition the Hilbert basis theorem gives it. What the subring lacks is any map back to it, which is exactly the hypothesis A subring that admits a module retraction from a Noetherian ring is Noetherian adds in order to make the conclusion descend.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

35 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