Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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 KN, the induced map KRMNRM is injective.
  3. For every ideal IR, the multiplication map IRMM, amam, 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 RRMM; consequently RnRMMn (Tensor products commute with arbitrary direct sums, The regular module is a tensor unit: RRNN and MRRM).

[L4]

A finite list x1,,xn in a module determines a homomorphism RnN 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 MRN 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.1

Claim 1 implies claim 2 by applying [L1] to 0KN; claim 2 implies claim 3 by taking the inclusion IR and using RRMM; claim 3 implies claim 4 by restriction to finitely generated ideals.

L1L2L3L5
1.2

Assume claim 4. Claim 3 follows: an element xIRM is represented by finitely many coefficients from I, hence comes from I0RM 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.

givenL5
1.3

Let KN be injective and let xKRM 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 NRM. Hence there are finitely generated submodules K0K and N0N with K0N0 for which x comes from an element killed in N0RM.

givenL6
2.1

Under claim 3, for every submodule LRn, the map LRMMn is injective, by induction on n. For n=0 it is the unique map 00; for n=1 it is claim 3 by [L5].

step 1.2L3L4
2.2

Present N0=Rn/L using [L4], and let LRn be the inverse image of K0. Right exactness identifies N0RM with Mn/im(LRM) and K0RM with the quotient of LRM by im(LRM).

step 1.3L2L3L4
3.1

For the induction step, let QRn, put Q:=Q(R0n1), and let Q be the image of Q in Rn1. Tensoring the exact rows 0QQQ0 and 0RRnRn10 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.

step 2.1L2L3
4.1

If zQRM maps to zero in Mn, its image in QRM maps to zero in Mn1 and hence is zero by the right vertical injection in step 3.1. Right exactness of the top row lifts z from some yQRM. The image of y in RRM 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.

step 3.1L2L3
5.1

By step 4.1, both LRM and LRM 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.

step 4.1step 2.2
6.1

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.

step 5.1L1L2
7.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.

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

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources