TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passaudited 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.

Morphisms between finite biproducts correspond to matrices

Statement

Let $C$ be additive, let $A = ⨁_{i = 1}^{m} A_{i}$ , and let $B = ⨁_{j = 1}^{n} B_{j}$ . Then

$C (A, B) ≅ \prod_{i = 1}^{m} \prod_{j = 1}^{n} C (A_{i}, B_{j})$

by the map sending $f : A \to B$ to the matrix of entries $f_{j i} : = p_{j} f i_{i}$ . This is an isomorphism of abelian groups.

Facts & Assumptions

Given: An additive category with finite biproducts $A = ⨁_{i} A_{i}$ and $B = ⨁_{j} B_{j}$ .

[L1]

An additive category is preadditive, so hom-sets are abelian groups with finite sums (Additive category).

[L2]

On a biproduct, the identity is the sum of injection-projection terms (On a biproduct, the injections and projections satisfy the identity-sum relation).

[L3]

Finite biproducts are canonically associative and commutative, so the bracketing of the finite sums does not matter (Biproducts are associative, commutative, and unital up to canonical isomorphism).

Proof

technique · direct

1.1

Define $Φ : C (A, B) \to \prod_{i, j} C (A_{i}, B_{j})$ by $Φ (f) = (p_{j} f i_{i})_{j, i}$ . This is a group homomorphism because each $p_{j} (-) i_{i}$ is additive by bilinearity in [L1].

1.2

For a matrix $(u_{j i})$ of morphisms $u_{j i} : A_{i} \to B_{j}$ , define $Ψ ((u_{j i})) : = \sum_{i, j} i_{j} u_{j i} p_{i} : A \to B$ . This finite sum is legitimate by [L1] and [L3].

L1L3construct

2.1

Using the zero equations and [L2], one gets $p_{k} Ψ ((u_{j i})) i_{ℓ} = \sum_{i, j} p_{k} i_{j} u_{j i} p_{i} i_{ℓ} = u_{k ℓ}$ . Hence $Φ Ψ$ is the identity on the matrix product.

L1L2step 1.2algebra

2.2

For $f : A \to B$ , the identity-sum relation on both source and target gives $f = 1_{B} f 1_{A} = (\sum_{j} i_{j} p_{j}) f (\sum_{i} i_{i} p_{i}) = \sum_{i, j} i_{j} (p_{j} f i_{i}) p_{i} = Ψ (Φ (f))$ . So $Ψ Φ = 1_{C (A, B)}$ .

L1L2step 1.2

3.1

Thus $Φ$ and $Ψ$ are inverse group homomorphisms, giving the asserted matrix description of $C (A, B)$ .

step 1.1step 2.1step 2.2∎

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

Merlin Christ, Tobias Dyckerhoff, and Tashi Walde, Lax Additivity, matrix-calculus discussion after Lemma 2.4 (standard reference, not scraped)