Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Completion of a Noetherian ring is Noetherian

Statement

Assume the Axiom of Choice.

Let R be a Noetherian commutative ring and let IR be an ideal. Then the I-adic completion R^ is a Noetherian ring.

Facts & Assumptions

Given: The Axiom of Choice, a Noetherian commutative ring R, and an ideal IR.

[L1]

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

[L3]

A finite-variable polynomial ring over a Noetherian ring is Noetherian (If R is Noetherian then R[x1,,xn] is Noetherian for every nN).

[L4]

For a finite module, completion commutes with quotients and ideal powers (Completion commutes with finite quotients and induced submodules).

Proof

technique · direct
1.1

By [L2], choose generators f1,,fr of I. The quotient R/I is Noetherian by [L1], hence the polynomial ring (R/I)[T1,,Tr] is Noetherian by [L3].

L1L2L3choose
2.1

The graded ring grI(R):=n0In/In+1 is a quotient of (R/I)[T1,,Tr] via Tjfj, so grI(R) is Noetherian.

step 1.1algebra
3.1

By part 3 of Completion commutes with finite quotients and induced submodules, R^/InR^R/In for every n, and part 2 identifies InR^ with the completion of In. Therefore InR^/In+1R^In/In+1 for all n, so the associated graded ring grIR^(R^) is canonically isomorphic to grI(R). Hence it is Noetherian.

L4step 2.1
4.1

Let JR^ be an ideal. Since grIR^(R^) is Noetherian, [L2] makes the graded ideal gr(J):=n0JInR^JIn+1R^ finitely generated. Taking homogeneous components of a finite generating set, choose homogeneous generators g1,,gm, where gjJIdjR^.

L2step 3.1choosealgebra
5.1

We claim that g1,,gm generate J. Put r0=xJ. Inductively, suppose rnJInR^. Express its degree-n class in gr(J) as rn=djnaj,ngj, with aj,n homogeneous of degree ndj. Lift it to aj,nIndjR^, and put aj,n=0 when dj>n. Then rn+1:=rnjaj,ngjJIn+1R^. The assumed Choice principle supports this countable recursion. Consequently, for every N0, xn=0Njaj,ngj=rN+1JIN+1R^.

step 4.1inductionchoosealgebra
6.1

The completion ring R^ is complete for the IR^-adic topology because it is already the inverse limit of the quotients R/In and step 3.1 identifies these with R^/InR^. For fixed j, step 5.1 has aj,n=0 for n<dj and aj,nIndjR^ thereafter, so its partial sums are Cauchy and converge to some AjR^. For Ndj, the tail satisfies Ajn=0Naj,nIN+1djR^. Multiplying by gjIdjR^ and using step 5.1 gives xjAjgjIN+1R^ for every sufficiently large N. Completeness includes separatedness, so the intersection of the powers is 0 and therefore x=jAjgj. Thus J=(g1,,gm) is finitely generated.

step 3.1step 5.1algebra
7.1

Every ideal JR^ is finitely generated, so R^ is Noetherian by the ideal characterization.

L2step 6.1

Depends on

Used by

Dependency tree · two levels

23 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