TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

Left exactness, right exactness, and exactness are characterized by short exact sequences

Statement

Let $F : A \to B$ be a functor between abelian categories.

$F$ is left exact if and only if for every short exact sequence $0 \to A^{'} \to A \to A^{''} \to 0$ in $A$ , the sequence $0 \to F (A^{'}) \to F (A) \to F (A^{''})$ is exact.
$F$ is right exact if and only if for every short exact sequence $0 \to A^{'} \to A \to A^{''} \to 0$ in $A$ , the sequence $F (A^{'}) \to F (A) \to F (A^{''}) \to 0$ is exact.
$F$ is exact if and only if it carries every short exact sequence in $A$ to a short exact sequence in $B$ .

Facts & Assumptions

Given: A functor $F : A \to B$ between abelian categories.

[L1]

Left exactness or right exactness already forces additivity (A left or right exact functor between abelian categories is automatically additive).

[L2]

A functor between additive categories is additive exactly when it preserves finite biproducts (A functor between additive categories is additive exactly when it preserves finite biproducts).

[L3]

An additive functor is left exact exactly when it preserves kernels (An additive functor is left exact exactly when it preserves kernels).

[L4]

Abelian categories remain abelian after passing to the opposite (The opposite of an abelian category is abelian).

[L5]

In an abelian category every monomorphism is the kernel of its cokernel (Every monomorphism is the kernel of its cokernel, and dually every epimorphism is the cokernel of its kernel).

Proof

technique · direct

1.1L1L3L4

If $F$ is left exact, then [L1] makes it additive, and [L3] says that it preserves kernels. Therefore whenever $0 \to K \overset{k}{\to} A \overset{c}{\to} Q \to 0$ is short exact, the map $F (k)$ is a kernel of $F (c)$ , which is exactly the left-exact short-sequence criterion. The right-exact half is the dual statement applied in opposite categories using [L4].

1.2L2L3L4L5

Conversely, assume $F$ carries every short exact sequence to one exact through the middle. Applying that to the two split short exact sequences $0 \to A \to A \oplus B \to B \to 0$ and $0 \to B \to A \oplus B \to A \to 0$ shows that $F (A \oplus B)$ is a biproduct of $F (A)$ and $F (B)$ , so $F$ preserves finite biproducts and is additive by [L2]. Now every kernel $k : K \to A$ fits into a short exact sequence $0 \to K \to A \to A / K \to 0$ by [L5], so the hypothesis makes $F (k)$ a kernel. Then [L3] gives left exactness. The right-exact converse is the dual argument in opposite categories using [L4].

2.1step 1.1step 1.2∎

Clause 3 is exactly the conjunction of the first two clauses: a short exact sequence stays short exact precisely when the transformed sequence is both left exact and right exact.

Depends on

Used by

Dependency tree · two levels

22 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

The Stacks Project, Section 12.7, Lemma 12.7.2(2)-(4) (standard reference, not scraped)
Gautam Tamme, Algebra II Lecture 10, §10.4 (standard reference, not scraped)