Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

A short exact sequence with flat quotient remains short exact after tensoring

Statement

Let

0AiBpC0

be a short exact sequence of modules over a commutative ring R. If C is flat, then for every R-module N the sequence

0ARNi1BRNp1CRN0

is short exact.

Facts & Assumptions

Given: A short exact sequence 0AiBpC0 with C flat, and an R-module N.

[L1]

Flatness makes tensoring preserve injections (Flat and faithfully flat modules and ring homomorphisms).

[L2]

Tensoring is right exact (Tensoring is right exact).

[L3]

Free modules are flat, and flatness means that tensoring preserves exact sequences; hence tensoring a short exact sequence with a free module preserves short exactness (Under the stated choice boundary, free modules are projective and hence flat, Flat and faithfully flat modules and ring homomorphisms).

[L4]

Every module admits a canonical surjection from a free module (Every module is a quotient of a free module).

[L5]

A short exact sequence has an injective first map, a surjective second map, and image equal to kernel (Exact sequences and short exact sequences of modules).

Proof

technique · direct
1.1

By [L4], choose a surjection ε:FN from a free module and let K=kerε, so 0KFN0 is short exact.

L4L5choose
2.1

Tensor the sequence in step 1.1 with each of A,B,C. By [L2], the three resulting columns XRKXRFXRN0 are right exact. The map CRKCRF is injective by flatness of C and [L1].

step 1.1L1L2
2.2

Tensor the given short exact sequence with F. Since F is flat by [L3], the middle row 0ARFBRFCRF0 is short exact. Tensoring it with K and N gives right-exact bottom and top rows by [L2].

givenstep 1.1L2L3
3.1

Let xARN map to zero in BRN. By right exactness of the A-column, lift x to yARF. Its image yBBRF maps to zero in BRN, so right exactness of the B-column gives zBRK mapping to yB.

step 2.1step 2.2choose
4.1

The image of z in CRK maps in CRF to the image of yB, which is zero because y came from ARF. The injectivity in step 2.1 therefore makes the image of z in CRK zero.

step 2.1step 3.1L5
5.1

By right exactness of the bottom row in step 2.2, choose wARK mapping to z. In BRF, the images of y and of w are both yB; injectivity of ARFBRF from step 2.2 makes y the image of w.

step 2.2step 3.1step 4.1choose
6.1

The composite ARKARFARN is zero because KFN is zero. Hence step 5.1 gives x=0, proving i1 injective.

step 3.1step 5.1algebra
7.1

Right exactness [L2] already gives exactness at BRN, surjectivity onto CRN, and the terminal zero. Together with step 6.1, the tensored sequence is short exact.

step 6.1L2L5

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 47 results over 18 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