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 local ring is local with the same residue field

Statement

Assume the Axiom of Choice.

Let (R,m) be a Noetherian local ring, and let R^ be its m-adic completion.

  1. R^ is a Noetherian local ring with maximal ideal mR^.
  2. The residue field is unchanged: R^/mR^R/m.
  3. The completion map RR^ is faithfully flat.

Facts & Assumptions

Given: A Noetherian local ring (R,m).

[L1]

The completion R^ of a Noetherian ring is Noetherian (Completion of a Noetherian ring is Noetherian).

[L2]

If the defining ideal lies in the Jacobson radical, then completion is faithfully flat (Jacobson-adic completion is faithfully flat).

[L3]

Completion commutes with quotient by the defining ideal (Completion commutes with finite quotients and induced submodules).

[L4]

In an adically complete ring, every element congruent to 1 modulo the defining ideal is a unit (Elements congruent to 1 modulo a defining ideal are units).

[L5]

A local ring is a ring with a unique maximal ideal (A local ring is a nonzero commutative ring with a unique maximal ideal).

Proof

technique · direct
1.1

Since R is local, its unique maximal ideal m equals J(R). Hence [L2] applies and shows that RR^ is faithfully flat.

L2L5
1.2

By [L1], the ring R^ is Noetherian. By [L3], R^/mR^R/m, and the right-hand side is a field because R is local. Thus mR^ is a maximal ideal of R^.

L1L3L5
1.3

For each n1, part 3 of [L3] gives R^/mnR^R/mn. Therefore the canonical map R^limnR^/mnR^ identifies with the identity of limnR/mn=R^. So R^ is complete for the mR^-adic topology.

L3algebra
2.1

Let xR^ with xmR^. Its residue class in R^/mR^ is then nonzero, hence a unit. Choose yR^ with xy1(modmR^). By [L4] and step 1.3, the element xy is a unit, hence x is a unit. Therefore every nonunit lies in mR^, so mR^ is the unique maximal ideal of R^.

L4step 1.2step 1.3choose
3.1

Step 1.2 proves the residue-field isomorphism, and steps 1.1, 1.3, and 2.1 prove that R^ is Noetherian local with maximal ideal mR^ and that RR^ is faithfully flat.

step 1.1step 1.2step 1.3step 2.1

Depends on

Used by

Dependency tree · two levels

20 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