TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

An additive functor preserves finite biproducts

Statement

An additive functor between additive categories preserves finite biproducts.

Facts & Assumptions

Given: An additive functor $F : C \to D$ between additive categories.

[L1]

Additive categories are preadditive with finite biproducts (Additive category).

[L2]

An additive functor preserves zero morphisms (An additive functor preserves zero morphisms).

[L3]

In a semiadditive category, the identity-sum relation characterizes a biproduct from product data and the zero equations (On a biproduct, the injections and projections satisfy the identity-sum relation).

[L4]

Additivity means the induced maps on hom-groups preserve sums (Additive functor).

Proof

technique · direct

1.1

Let $X = A \oplus B$ in $C$ with structure maps $i_{A}, i_{B}, p_{A}, p_{B}$ , and let $Y = F A \oplus F B$ in $D$ with injections $j_{A}, j_{B}$ and projections $q_{A}, q_{B}$ . By [L1] and [L3], the source maps satisfy the zero equations and the identity-sum relation $i_{A} p_{A} + i_{B} p_{B} = 1_{X}$ . Applying $F$ preserves the zero equations by [L2] and the identity-sum relation by [L4], so $F (p_{A}) F (i_{A}) = 1_{F A}$ , $F (p_{B}) F (i_{B}) = 1_{F B}$ , $F (p_{A}) F (i_{B}) = 0$ , $F (p_{B}) F (i_{A}) = 0$ , and $F (i_{A}) F (p_{A}) + F (i_{B}) F (p_{B}) = 1_{F (X)}$ .

L1L2L3L4

1.2

Let $α : F (X) \to Y$ be the unique morphism with $q_{A} α = F (p_{A})$ and $q_{B} α = F (p_{B})$ , and let $β : Y \to F (X)$ be the unique morphism with $β j_{A} = F (i_{A})$ and $β j_{B} = F (i_{B})$ . These exist because $Y$ is both a product and a coproduct by [L1].

L1construct

1.3

Let $0$ be a zero object of $C$ . Then $1_{0} = 0_{0, 0}$ , so [L2] and [L4] give $1_{F (0)} = F (1_{0}) = F (0_{0, 0}) = 0_{F (0), F (0)}$ . For any object $Z$ of $D$ and morphisms $u : Z \to F (0)$ and $v : F (0) \to Z$ , this implies $u = 1_{F (0)} u = 0$ and $v = v 1_{F (0)} = 0$ . Since [L1] gives zero morphisms in $D$ , these are the unique morphisms to and from $F (0)$ . Hence $F (0)$ is a zero object.

L1L2L4

2.1

Since $Y$ is a coproduct, the equalities $q_{A} α β j_{A} = 1_{F A} = q_{A} j_{A}$ , $q_{A} α β j_{B} = 0 = q_{A} j_{B}$ , $q_{B} α β j_{A} = 0 = q_{B} j_{A}$ , and $q_{B} α β j_{B} = 1_{F B} = q_{B} j_{B}$ force $q_{A} α β = q_{A}$ and $q_{B} α β = q_{B}$ . Because $Y$ is also a product, this implies $α β = 1_{Y}$ . On the other hand, step 1.1 gives $β α = F (i_{A}) F (p_{A}) + F (i_{B}) F (p_{B}) = F (i_{A} p_{A} + i_{B} p_{B}) = 1_{F (X)}$ . So $α$ and $β$ are inverse isomorphisms, and $F (X)$ is a biproduct of $F A$ and $F B$ .

L1L4step 1.1step 1.2

3.1

Therefore $F$ preserves binary biproducts and the empty biproduct. By the binary-plus-empty characterization in [L1], it preserves all finite biproducts.

L1step 2.1step 1.3∎

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

The Stacks Project, Section 12.3, Lemma 12.3.7 (standard reference, not scraped)