Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

Semilocal completion decomposes into completed local factors

Example

Let R be a Noetherian commutative ring, let t1, and let m1,,mt be distinct maximal ideals. Set

m:=m1mt.

Then the m-adic completion of R decomposes as

R^mi=1tRmi^.

Facts & Assumptions

Given: A Noetherian commutative ring R, an integer t1, pairwise distinct maximal ideals m1,,mt, and m=imi.

[L1]

Completion is the inverse limit of the residue rings modulo the powers of the defining ideal (The I-adic completion of a module).

[L2]

Pairwise comaximal ideals give a product decomposition modulo their intersection (Chinese remainder theorem for pairwise comaximal ideals).

Verification

technique · direct
1.1

Distinct maximal ideals are pairwise comaximal. If I+J=R, expanding (a+b)2n1=1 for aI, bJ, and a+b=1 shows that In+Jn=R; hence the powers min are again pairwise comaximal. Applying [L2] first to the mi and then to their powers gives, for every n1, mn=(i=1tmi)n=i=1tmin=i=1tmin and R/mni=1tR/min.

L2givenchoosealgebra
2.1

Localizing R/min at Rmi changes nothing. Indeed, if smi, maximality gives aR and umi with as+u=1, and as(1+u++un1)=1un1(modmin). Thus every such s is already a unit modulo min, and R/minRmi/minRmi. Taking inverse limits and using [L1] yields R^mlimni=1tRmi/minRmi.

L1step 1.1choosealgebra
3.1

A compatible tuple in the inverse limit of the finite products in step 2.1 is exactly a choice, for each i, of a compatible tuple in the ith quotient tower. Therefore inverse limit commutes with this finite product, and R^mi=1tlimnRmi/minRmi=i=1tRmi^. This is the claimed decomposition.

L1step 2.1algebra

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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