Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-16
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.

Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests

Statement

Let R be a commutative ring and let M be an R-module. The following are equivalent:

  1. M is flat.
  2. For every injection K↪N, the induced map K⊗RM→N⊗RM is injective.
  3. For every ideal I⊆R, the multiplication map I⊗RM→M, a⊗m↦am, is injective.
  4. The map in claim 3 is injective for every finitely generated ideal I.

Facts & Assumptions

Given: A commutative ring R and an R-module M.

[L1]

Flatness means that −⊗RM preserves exact sequences (Flat and faithfully flat modules and ring homomorphisms).

[L2]

Tensoring is right exact (Tensoring is right exact).

[L3]

Tensor products commute with direct sums and R⊗RM≅M; consequently Rn⊗RM≅Mn (Tensor products commute with arbitrary direct sums, The regular module is a tensor unit: R⊗RN≅N and M⊗RR≅M).

[L4]

A finite list x1,…,xn in a module determines a homomorphism Rn→N taking ej to xj; if the list generates N, this map is surjective. Also R0=0 (The free module on a set and its standard basis, Universal property of the free module on a set).

[L5]

In a commutative ring, every submodule of the regular module R is an ideal (Left, right and two-sided ideals).

[L6]

A tensor product is the quotient of the free Z-module on pairs by the subgroup generated by the additive and balance relations (The tensor product M⊗RN from the additive group underlying the free Z-module on M×N, elementary tensors, and finite tensor sums). Consequently, a tensor expression and a derivation that it is zero involve only finitely many generators and defining relations.

Proof

technique · direct
1.1L1L2L3L5

Claim 1 implies claim 2 by applying [L1] to 0→K→N; claim 2 implies claim 3 by taking the inclusion I↪R and using R⊗RM≅M; claim 3 implies claim 4 by restriction to finitely generated ideals.

1.2givenL5

Assume claim 4. Claim 3 follows: an element x∈I⊗RM is represented by finitely many coefficients from I, hence comes from I0⊗RM for the finitely generated ideal I0 they generate; if its image in M is zero, injectivity for I0 makes its representative zero, so x=0.

1.3givenL6

Let K↪N be injective and let x∈K⊗RM map to zero. By [L6], the tensor x uses finitely many elements of K, and a derivation of its zero image uses only finitely many generators and defining relations in N⊗RM. Hence there are finitely generated submodules K0⊆K and N0⊆N with K0⊆N0 for which x comes from an element killed in N0⊗RM.

2.1step 1.2L3L4

Under claim 3, for every submodule L⊆Rn, the map L⊗RM→Mn is injective, by induction on n. For n=0 it is the unique map 0→0; for n=1 it is claim 3 by [L5].

2.2step 1.3L2L3L4

Present N0=Rn/L using [L4], and let L′⊆Rn be the inverse image of K0. Right exactness identifies N0⊗RM with Mn/im⁡(L⊗RM) and K0⊗RM with the quotient of L′⊗RM by im⁡(L⊗RM).

3.1step 2.1L2L3

For the induction step, let Q⊆Rn, put Q′:=Q∩(R⊕0n−1), and let Q′′ be the image of Q in Rn−1. Tensoring the exact rows 0→Q′→Q→Q′′→0 and 0→R→Rn→Rn−1→0 gives right-exact rows by [L2]; the left and right vertical maps are injective by the n=1 case and the induction hypothesis from step 2.1.

4.1step 3.1L2L3

If z∈Q⊗RM maps to zero in Mn, its image in Q′′⊗RM maps to zero in Mn−1 and hence is zero by the right vertical injection in step 3.1. Right exactness of the top row lifts z from some y∈Q′⊗RM. The image of y in R⊗RM maps to the zero image of z in Mn; the left vertical injection in step 3.1 makes y=0, and therefore z=0. This completes the induction of step 2.1.

5.1step 4.1step 2.2

By step 4.1, both L⊗RM and L′⊗RM inject into Mn. Therefore the induced map of the quotients in step 2.2 is injective, so x=0. This proves claim 2 from claim 4.

6.1step 5.1L1L2

Finally claim 2 and right exactness [L2] imply claim 1: for an exact sequence, replace the left map by the injection of its image into the middle term; tensoring preserves that injection by claim 2 and preserves the remaining image and cokernel statements by right exactness.

7.1step 1.1step 1.2step 2.1step 3.1step 4.1step 1.3step 2.2step 5.1step 6.1∎

Steps 1.1 through 6.1 prove the cycle of equivalences. The zero ideal, n=0, and zero module cases occur explicitly in steps 1.2 and 2.1; no choice is made, and both directions of every equivalence have been supplied.

Depends on

Used by

Dependency tree · two levels

25 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