Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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

0⟶A→iB→pC⟶0

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

0⟶A⊗RN→i⊗1B⊗RN→p⊗1C⊗RN⟶0

is short exact.

Facts & Assumptions

Given: A short exact sequence 0→A→iB→pC→0 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.1L4L5choose

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

2.1step 1.1L1L2

Tensor the sequence in step 1.1 with each of A,B,C. By [L2], the three resulting columns X⊗RK→X⊗RF→X⊗RN→0 are right exact. The map C⊗RK→C⊗RF is injective by flatness of C and [L1].

2.2givenstep 1.1L2L3

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

3.1step 2.1step 2.2choose

Let x∈A⊗RN map to zero in B⊗RN. By right exactness of the A-column, lift x to y∈A⊗RF. Its image yB∈B⊗RF maps to zero in B⊗RN, so right exactness of the B-column gives z∈B⊗RK mapping to yB.

4.1step 2.1step 3.1L5

The image of z in C⊗RK maps in C⊗RF to the image of yB, which is zero because y came from A⊗RF. The injectivity in step 2.1 therefore makes the image of z in C⊗RK zero.

5.1step 2.2step 3.1step 4.1choose

By right exactness of the bottom row in step 2.2, choose w∈A⊗RK mapping to z. In B⊗RF, the images of y and of w are both yB; injectivity of A⊗RF→B⊗RF from step 2.2 makes y the image of w.

6.1step 3.1step 5.1algebra

The composite A⊗RK→A⊗RF→A⊗RN is zero because K→F→N is zero. Hence step 5.1 gives x=0, proving i⊗1 injective.

7.1step 6.1L2L5∎

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

Depends on

Used by

Dependency tree · two levels

20 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