TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 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.

The equational criterion characterizes flat modules by lifting finite relations on generators

Statement

Let $R$ be a commutative ring and let $M$ be an $R$ -module. Then $M$ is flat if and only if the following condition holds:

Whenever $x_{1}, \dots, x_{n} \in M$ and $a_{1}, \dots, a_{n} \in R$ satisfy

\sum_{i = 1}^{n} a_{i} x_{i} = 0,

there exist elements $y_{1}, \dots, y_{m} \in M$ and coefficients $b_{i j} \in R$ such that

x_{i} = \sum_{j = 1}^{m} b_{i j} y_{j} for every i,

and

\sum_{i = 1}^{n} a_{i} b_{i j} = 0 for every j .

Facts & Assumptions

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

[L1]

Flatness means exactness of tensoring (Flat and faithfully flat modules and ring homomorphisms).

[L2]

Tensor products commute with finite direct sums and the regular module is a tensor unit, so $R^{n} \otimes_{R} M ≅ M^{n}$ canonically (Tensor products commute with arbitrary direct sums, The regular module is a tensor unit: $R \otimes_{R} N ≅ N$ and $M \otimes_{R} R ≅ M$ ).

[L3]

Flatness is equivalent to injectivity of $I \otimes_{R} M \to M$ for every finitely generated ideal $I \subseteq R$ (Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests).

Proof

technique · direct

1.1

Assume $M$ is flat, and let $I = (a_{1}, \dots, a_{n}) \subseteq R$ . The surjection $π : R^{n} \to I$ sending $e_{i}$ to $a_{i}$ has kernel $K$ . Tensoring the exact sequence $K ⟶ R^{n} \overset{π}{\to} I ⟶ 0$ with $M$ remains exact by [L1].

L1givenalgebra

1.2

Conversely, assume the stated relation-lifting property. To prove flatness it is enough by [L3] to show that for every finitely generated ideal $I = (a_{1}, \dots, a_{n})$ , the multiplication map $I \otimes_{R} M \to M$ is injective. Take an element $\sum_{i = 1}^{n} a_{i} \otimes x_{i}$ in its kernel, so $\sum_{i} a_{i} x_{i} = 0$ . By the relation-lifting property, $x_{i} = \sum_{j} b_{i j} y_{j}$ and $\sum_{i} a_{i} b_{i j} = 0$ for every $j$ . Then $\sum_{i} a_{i} \otimes x_{i} = \sum_{j} (\sum_{i} a_{i} b_{i j}) \otimes y_{j} = 0$ in $I \otimes_{R} M$ . Hence the map is injective.

L3givenalgebra

1.3

The ideal-injection criterion [L3] now shows that $M$ is flat.

2.1

The relation $\sum_{i = 1}^{n} a_{i} x_{i} = 0$ says exactly that the tensor $η = \sum_{i} a_{i} \otimes x_{i} \in I \otimes_{R} M$ maps to $0$ under the multiplication map $I \otimes_{R} M \to M$ . By [L3], that map is injective, so $η = 0$ . Therefore the tensor $\tilde{η} : = \sum_{i} e_{i} \otimes x_{i} \in R^{n} \otimes_{R} M$ lies in the image of $K \otimes_{R} M \to R^{n} \otimes_{R} M$ from step 1.1.

L3step 1.1algebra

3.1

Write a preimage of $\tilde{η}$ as a finite sum $\sum_{j = 1}^{m} k_{j} \otimes y_{j}$ with $k_{j} \in K$ and $y_{j} \in M$ . Under the identification $R^{n} \otimes_{R} M ≅ M^{n}$ from [L2], if $k_{j} = (b_{1 j}, \dots, b_{n j})$ , then comparing coordinates gives $x_{i} = \sum_{j = 1}^{m} b_{i j} y_{j} for every i .$ Since each $k_{j}$ lies in $\ker π$ , one also has $\sum_{i = 1}^{n} a_{i} b_{i j} = 0 for every j .$ This is the required decomposition.

L2step 2.1algebra

4.1

Therefore the equational criterion is equivalent to flatness.

algebra∎

Depends on

Used by

Dependency tree · two levels

17 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, Theorem (9.18) (standard reference, not scraped)
Stacks Project, Section 10.39: Flat modules and flat ring maps (standard reference, not scraped)