Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 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.

Determinant trick for Nakayama

Statement

Let R be a commutative ring, let I⊴R be an ideal, and let M be a finitely generated left R-module. If IM=M, then there exists a∈I such that (1−a)M=0.

Facts & Assumptions

Given: A commutative ring R, an ideal I⊴R, and a finitely generated left R-module M with IM=M.

[L1]

A finitely generated module has a finite generating set (Generated submodule, cyclic and finitely generated modules, module basis and free module).

[L2]

The submodule IM consists of finite sums of products im with i∈I and m∈M (The submodule IM generated by products of elements of an ideal I with elements of a module M).

[L3]

For a positive-size square matrix A over a commutative ring, Aadj⁡(A)=det⁡(A)I (For every positive-sized square matrix over a commutative ring, Aadj⁡(A)=adj⁡(A)A=det⁡(A)I).

Proof

technique · direct
1.1L1givenchoose

If M=0, then a=0∈I satisfies (1−a)M=0. So assume M≠0 and choose generators m1,…,mn with n≥1 by [L1].

2.1L2step 1.1algebra

Since IM=M, each generator has the form mi=∑jaijmj with aij∈I. Writing A=(aij) and m=(m1,…,mn)T, this is (In−A)m=0.

3.1L3step 2.1algebra

Multiply the relation of step 2.1 by adj⁡(In−A). By [L3], this gives det⁡(In−A)m=0, so det⁡(In−A) annihilates every generator and hence all of M.

3.2step 2.1algebra

Expanding det⁡(In−A), the identity permutation contributes 1, and every other term contains at least one entry of A, hence lies in I. Therefore det⁡(In−A)=1−a for some a∈I.

4.1step 3.1step 3.2∎

Step 3.1 and step 3.2 give (1−a)M=0 for some a∈I.

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