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.

Composition of morphisms between finite biproducts is matrix multiplication

Statement

Let $C$ be an additive category. Let $f : ⨁_{i = 1}^{m} A_{i} \to ⨁_{j = 1}^{n} B_{j}$ have matrix $F = (f_{j i})_{j, i}$ and let $g : ⨁_{j = 1}^{n} B_{j} \to ⨁_{k = 1}^{r} C_{k}$ have matrix $G = (g_{k j})_{k, j}$ . Then the matrix of $g f$ is

$((g f)_{k i})_{k, i}, (g f)_{k i} = \sum_{j = 1}^{n} g_{k j} f_{j i} .$

The finiteness of the middle index set is part of the statement.

Facts & Assumptions

Given: Morphisms $f$ and $g$ between finite biproducts in an additive category, with matrix entries $f_{j i}$ and $g_{k j}$ .

[L1]

A morphism between finite biproducts is reconstructed from its matrix by a finite sum of injection-entry-projection terms (Morphisms between finite biproducts correspond to matrices).

Proof

technique · direct

1.1

By [L1], one may write $f = \sum_{i, j} i_{j} f_{j i} p_{i}$ and $g = \sum_{j, k} i_{k}^{'} g_{k j} q_{j}$ , where $q_{j}$ are the projections of the middle biproduct and $i_{k}^{'}$ are the injections of the target biproduct.

2.1

Multiply the two finite sums and use the zero equations $q_{j} i_{j^{'}} = 0$ for $j \neq j^{'}$ and $q_{j} i_{j} = 1_{B_{j}}$ . The only surviving terms are $i_{k}^{'} g_{k j} f_{j i} p_{i}$ , so $g f = \sum_{i, j, k} i_{k}^{'} g_{k j} f_{j i} p_{i}$ .

L1step 1.1algebra

3.1

Taking the $(k, i)$ entry of the matrix, again by [L1], yields $(g f)_{k i} = \sum_{j = 1}^{n} g_{k j} f_{j i}$ . The sum is finite because the middle biproduct has only $n$ summands.

L1step 2.1∎

Depends on

Used by

Dependency tree · two levels

7 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

Merlin Christ, Tobias Dyckerhoff, and Tashi Walde, Lax Additivity, formula (2.6) (standard reference, not scraped)