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.

Adic completion is exact on finite modules over a Noetherian ring

Statement

Assume the Axiom of Choice.

Let R be a Noetherian commutative ring, let IR be an ideal, and let

0MMM0

be a short exact sequence of finitely generated R-modules. Then the induced sequence of I-adic completions

0M^M^M^0

is exact.

Facts & Assumptions

Given: A Noetherian commutative ring R, an ideal IR, and a short exact sequence 0MMM0 of finitely generated R-modules.

[L1]

Countable inverse limits preserve short exact sequences whenever the left system is Mittag-Leffler (Countable Mittag-Leffler systems preserve short exactness on inverse limits).

[L2]

The I-adic completion is the inverse limit of the quotients by the powers of I (The I-adic completion of a module).

Proof

technique · direct
1.1

For each n0, the given short exact sequence induces an exact sequence 0M/(MInM)M/InMM/InM0. The first map is injective because its kernel is (MInM)/(MInM), and the second map is surjective because every class in M/InM lifts to a class in M/InM.

givenalgebra
2.1

The left inverse system M/(MInM) has surjective transition maps, hence is Mittag-Leffler. Indeed, if nm and xM, then the class of x in M/(MImM) is the image of the class of the same x in M/(MInM). Therefore every transition map M/(MInM)M/(MImM) is surjective.

step 1.1algebra
3.1

Taking inverse limits in the sequences of step 1.1 and using [L1] yields an exact sequence 0limM/(MInM)limM/InMlimM/InM0.

L1step 2.1
4.1

By [L2], the middle and right inverse limits are M^ and M^. For the left inverse limit, the induced filtration MInM on M is equivalent to the intrinsic I-adic filtration InM by The filtration induced on a submodule is equivalent to its intrinsic ideal-adic filtration, so its completion is M^.

L2step 3.1
5.1

Substituting these identifications into step 3.1 gives 0M^M^M^0, which is the claimed exactness.

step 4.1

Depends on

Used by

Dependency tree · two levels

13 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