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.

On a biproduct, the injections and projections satisfy the identity-sum relation

Statement

Let $A \oplus B$ be a biproduct in a category with finite biproducts, with injections $i_{A}, i_{B}$ and projections $p_{A}, p_{B}$ . Then

$i_{A} p_{A} + i_{B} p_{B} = 1_{A \oplus B} .$

Conversely, if an object $X$ in a semiadditive category is a product of $A$ and $B$ with projections $p_{A}, p_{B}$ , and if morphisms $i_{A} : A \to X$ and $i_{B} : B \to X$ satisfy the zero equations together with $i_{A} p_{A} + i_{B} p_{B} = 1_{X}$ , then $X$ is also their coproduct and hence their biproduct.

Facts & Assumptions

Given: A semiadditive category and a biproduct or product diagram for $A, B$ .

[L1]

Biproduct data are characterized by the product and coproduct universal properties plus the zero equations (Biproduct data characterisation without addition).

[L2]

A semiadditive category has a commutative-monoid law on hom-sets with bilinear composition (A category with finite biproducts is enriched in commutative monoids).

Proof

technique · direct

1.1

Suppose $X = A \oplus B$ is a biproduct. By [L1], the maps satisfy $p_{A} i_{A} = 1_{A}$ , $p_{B} i_{B} = 1_{B}$ , $p_{A} i_{B} = 0$ , and $p_{B} i_{A} = 0$ . Therefore $p_{A} (i_{A} p_{A} + i_{B} p_{B}) = p_{A}$ and $p_{B} (i_{A} p_{A} + i_{B} p_{B}) = p_{B}$ by bilinearity from [L2]. Since $X$ is the product of $A$ and $B$ , these equalities force $i_{A} p_{A} + i_{B} p_{B} = 1_{X}$ .

L1L2

1.2

Conversely, assume $(X, p_{A}, p_{B})$ is a product and that $i_{A}, i_{B}$ satisfy the same zero equations together with $i_{A} p_{A} + i_{B} p_{B} = 1_{X}$ . For any $f : A \to Y$ and $g : B \to Y$ , define $h : = f p_{A} + g p_{B} : X \to Y$ . Then $h i_{A} = f$ and $h i_{B} = g$ by the zero equations and bilinearity.

L1L2construct

2.1

If $k : X \to Y$ also satisfies $k i_{A} = f$ and $k i_{B} = g$ , then using the identity-sum relation and bilinearity gives $k = k 1_{X} = k (i_{A} p_{A} + i_{B} p_{B}) = k i_{A} p_{A} + k i_{B} p_{B} = f p_{A} + g p_{B} = h$ . So $(X, i_{A}, i_{B})$ is a coproduct. Together with the zero equations, [L1] makes $X$ a biproduct.

L1L2step 1.2

3.1

This proves both the identity-sum relation on a biproduct and the converse recovery of the coproduct structure from that relation.

step 1.1step 2.1∎

Depends on

Used by

An additive functor preserves split biproduct diagrams Proposition
An additive category with kernels is idempotent complete Theorem
An additive functor preserves finite biproducts Theorem
Morphisms between finite biproducts correspond to matrices Theorem

Dependency tree · two levels

6 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, Remark 12.3.6 (standard reference, not scraped)
Saunders Mac Lane, Categories for the Working Mathematician, VIII.2 (standard reference, not scraped)