Alphabeta Math
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.

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

Statement

For a functor between additive categories, the following are equivalent:

  1. the functor is additive;
  2. the functor preserves finite biproducts.

Facts & Assumptions

Given: A functor F:C→D between additive categories.

[L1]

Additive functors preserve finite biproducts (An additive functor preserves finite biproducts).

[L2]

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

[L3]

In a preadditive category, finite products are automatically biproducts (In a preadditive category, a finite product is automatically a biproduct).

[L4]

In an additive category, the preadditive hom-group law is a bilinear commutative-monoid enrichment compatible with the finite biproduct diagrams. Indeed, product uniqueness gives ⟨f,g⟩=i1f+i2g, and bilinearity then gives ∇⟨f,g⟩=f+g. By uniqueness this is the canonical biproduct addition (The commutative-monoid enrichment of a category with finite biproducts is unique).

Proof

technique · direct
1.1

The implication from 1 to 2 is exactly [L1].

L1
1.2

Assume F preserves finite biproducts. In an additive category, for parallel morphisms f,g:A→B, the pairing into B⊕B is the unique morphism ⟨f,g⟩ with projections f and g, and the codiagonal is the unique morphism ∇B:B⊕B→B with both composites equal to 1B. Since F preserves the relevant biproducts, it preserves those pairings and codiagonals.

L2L3
1.3

By [L4], the hom-group addition in an additive category is the canonical biproduct addition. [L2, L4, step 1.2] f+g=∇B⟨f,g⟩. Step 1.2 therefore gives F(f+g)=F(∇B)F(⟨f,g⟩)=∇FB⟨Ff,Fg⟩=Ff+Fg. So F is additive.

L2L4step 1.2
2.1

Steps 1.1 and 1.3 prove the equivalence.

step 1.1step 1.3∎

Depends on

Used by

Dependency tree · two levels

14 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