Alphabeta Math
CorollaryStatement: AI-adaptedProof: AI-adaptedverified 2026-09-24 (gpt-6-sol)
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.

A finite flat module over a Noetherian ring is finite projective

Statement

Let R be a Noetherian commutative ring and let M be a finite flat R-module. Then M is finite projective.

Facts & Assumptions

Given: A Noetherian commutative ring R and a finite flat R-module M.

[L2]

Flatness gives the equational criterion for each finite relation (The equational criterion characterizes flat modules by lifting finite relations on generators).

[L3]

A module is projective exactly when every map from it lifts across an epimorphism (Equivalent characterizations of projective modules).

Proof

technique · direct
1.1L1givenchoose

By [L1], choose a finite presentation Rm→DRn→πM→0. Put xi=π(ei), and write the columns of D as relation rows u(1),…,u(m)∈Rn, so ker⁡π is generated by those rows. Start with x=Ay, where A is the identity matrix and y is the column of the xi.

2.1L2step 1.1induction

Process the m relation rows in order. Suppose x=Ay and the first h−1 rows satisfy u(j)A=0. For the next row u(h), the equality u(h)x=0 says (u(h)A)y=0. Applying [L2] to this one finite relation gives a finite column z of elements of M and a matrix B with y=Bz and (u(h)A)B=0. Replace (A,y) by (AB,z). The new matrix satisfies u(h)AB=0, and each earlier relation remains zero because u(j)AB=(u(j)A)B=0. After the finite last stage, write x=Cz with u(j)C=0 for every j. This finite induction makes only finitely many choices.

3.1step 1.1step 2.1construct

Let z have t entries, and define s0:Rn→Rt by sending ei to the ith row of C. Every generator u(j) of ker⁡π is killed by s0 because u(j)C=0. Thus s0 descends to s:M→Rt. Define q:Rt→M by sending its basis vectors to the entries of z. The identity x=Cz says qs(xi)=xi for every generator xi, hence qs=1M.

4.1L3step 3.1choose∎

Let E↠N be any epimorphism and g:M→N any map. For each of the finitely many basis vectors of Rt, choose a preimage in E of its image under gq, and extend linearly to a lift h:Rt→E. Then hs lifts g because qs=1M. By [L3], M is projective. It is finite by hypothesis, so it is finite projective.

Depends on

Used by

Dependency tree · two levels

21 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