Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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 a flat module, faithful flatness is equivalent to detecting nonzero modules and residue fields

Statement

Assume the Axiom of Choice for the maximal-ideal detection step.

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

  1. M is faithfully flat.
  2. For every nonzero R-module N, one has NRM0.
  3. For every prime ideal pR, κ(p)RM0.
  4. For every maximal ideal mR, R/mRM=M/mM0.

Facts & Assumptions

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

[L1]

Faithful flatness means that tensoring with M reflects exactness (Flat and faithfully flat modules and ring homomorphisms).

[L2]

Flatness preserves injections, hence tensoring a monomorphism with M remains injective (Flatness is equivalent to preserving injections and to the ideal and finitely generated ideal tests).

Proof

technique · direct
1.1

If M is faithfully flat and N0, then the map 0N is nonzero. If NRM were zero, tensoring would turn the nonzero map 0N into the zero map, contradicting exactness reflection in [L1]. Thus 1 implies 2.

L1given
1.2

Condition 2 implies 3 by taking N=κ(p), and 3 implies 4 by restricting to maximal primes.

given
1.3

Assume 4. Let N0 and choose 0xN. The cyclic submodule RxR/Ann(x) injects into N. Choose a maximal ideal m containing Ann(x). Then there is a surjection R/Ann(x)R/m. Tensoring with M preserves the injection by [L2], and the target tensor is nonzero by 4. Hence NRM0. So 4 implies 2.

L2givenchoose
1.4

Assume 2 and let N1N2N3 be a complex whose tensor with M is exact. Since M is flat, it is enough to prove exactness at N2. If xker(N2N3) is not in the image of N1N2, then it defines a nonzero element of the quotient Q:=ker(N2N3)/im(N1N2). But tensoring with M kills Q, because the tensor complex is exact. This contradicts 2. Hence Q=0, and the original complex is exact. Therefore M is faithfully flat.

L1algebra
2.1

The four conditions are equivalent.

algebra

Depends on

Used by

Dependency tree · two levels

11 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