Alphabeta Math
TheoremStatement: AI-adaptedProof: 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.

For an R-finite module over a local map, flatness modulo I and injectivity of IMM imply flatness

Statement

Assume the Axiom of Choice.

Let RS be a local homomorphism of Noetherian local rings, let IR be an ideal, and let M be a finite S-module that is also finitely generated as an R-module. Assume:

  1. M/IM is flat over R/I;
  2. the multiplication map IRMM is injective.

Then M is flat over R.

Facts & Assumptions

Given: The Axiom of Choice, a local map of Noetherian local rings RS, a proper ideal IR, and a finite S-module M that is finitely generated as an R-module and satisfies the two hypotheses.

[L1]

The equational criterion characterizes flatness by lifting finite relations on generators (The equational criterion characterizes flat modules by lifting finite relations on generators).

[L2]

For a finite module over a local ring, lifts of generators modulo the maximal ideal generate the module under the assumed Choice boundary (Assuming the Axiom of Choice, generators modulo an ideal in the Jacobson radical lift to generators).

[L3]

Over a Noetherian ring, kernels of maps from finite free modules to finite modules are finitely generated (Over a Noetherian ring a module is Noetherian exactly when it is finitely generated, exactly when it is finitely presented).

[L4]

Tensor products are right exact, and JRRrJr for every ideal J and integer r0 (Tensoring is right exact, The regular module is a tensor unit: RRNN and MRRM).

[L5]

If K is a finite module over a local ring and mK=K, then K=0 (Assuming the Axiom of Choice, Nakayama's lemma).

Proof

technique · direct
1.1

Let m be the maximal ideal of R. We first prove that the multiplication map mRMM is injective. Take an element z=i=1nfixi in its kernel, so fim and ifixi=0. Reducing modulo I, the module M/IM is flat over R/I, so [L1] applied over R/I yields elements y1,,ytM/IM and coefficients aijR/I with xi=j=1taijyjandi=1n(fi)aij=0 for every j. Choose lifts yjM and aijR. Then xijaijyjIM and ifiaijI for every j. Writing each xijaijyj as a finite sum of terms bm with bI, one sees that z is the image in mRM of an element of IRM whose product in M is also 0. Hypothesis 2 makes that element zero, hence z=0.

L1givenchoosealgebra
1.2

Let k=R/m. Choose elements x1,,xrM whose images form a k-basis of M/mM. By [L2], these elements generate M, so they define a surjection π:F:=RrM. Let K:=ker(π). Because R is Noetherian, [L3] makes K finitely generated.

L2L3givenchoose
2.1

Tensoring the exact sequence KFM0 with the ideal m gives an exact sequence mRKmRFmRM0 by [L4]. Step 1.1 identifies mRM with its image mMM, and [L4] identifies mRF with mF. Under these identifications, the kernel of mFmM is exactly KmF, while the image of mRK is mK. Therefore KmF=mK.

L4step 1.1step 1.2algebra
3.1

The induced map F/mFM/mM sends the standard basis of kr to the chosen basis from step 1.2, so it is an isomorphism. Its kernel is (K+mF)/mFK/(KmF)=K/mK by step 2.1. Hence K/mK=0, so mK=K. Now [L5] gives K=0. Therefore π is an isomorphism, MRr is free, and in particular M is flat over R.

L5step 1.2step 2.1algebra
4.1

Thus M is flat over R.

step 3.1

Depends on

Used by

Dependency tree · two levels

27 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