PropositionStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30

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.

Products and coproducts of complexes are degreewise when they exist and preserve differentials

Statement

Let $(C_{∙}^{(i)})_{i \in I}$ be a family of chain complexes in an abelian category where the termwise products or coproducts exist.

If every $\prod_{i} C_{n}^{(i)}$ exists, then these products form a chain complex with differential characterized by the component differentials, and it is the product of the family in $Ch (A)$ .
If every $∐_{i} C_{n}^{(i)}$ exists, then these coproducts form a chain complex with differential characterized by the component differentials, and it is the coproduct of the family in $Ch (A)$ .

Facts & Assumptions

Given: A family of chain complexes $(C_{∙}^{(i)})_{i \in I}$ in an abelian category.

[L1]

A chain complex is a graded family with $d_{n - 1} d_{n} = 0$ (Chain complex in an abelian category).

[L2]

Products and coproducts are determined by their universal properties (Products and coproducts as limits and colimits of discrete diagrams, including their existence-and-uniqueness equations).

Proof

technique · constructive

1.1L1L2givenconstruct

Suppose the products exist. For each degree $n$ , let $P_{n} : = \prod_{i} C_{n}^{(i)}$ . By [L2] there is a unique map $d_{n}^{P} : P_{n} \to P_{n - 1}$ such that for every $i$ , $π_{i}^{n - 1} d_{n}^{P} = d_{n}^{(i)} π_{i}^{n},$ where $π_{i}^{n} : P_{n} \to C_{n}^{(i)}$ is the $i$ th projection. Then $π_{i}^{n - 2} d_{n - 1}^{P} d_{n}^{P} = d_{n - 1}^{(i)} d_{n}^{(i)} π_{i}^{n} = 0$ by [L1], so $d_{n - 1}^{P} d_{n}^{P} = 0$ because all projections of that composite are zero. Thus $P_{∙}$ is a chain complex and has the required product universal property degreewise.

2.1L1L2givenconstructdischarge-construct∎

The coproduct case is dual. If $Q_{n} : = ∐_{i} C_{n}^{(i)}$ exists in each degree, [L2] gives a unique $d_{n}^{Q} : Q_{n} \to Q_{n - 1}$ such that for every $i$ , $d_{n}^{Q} ι_{i}^{n} = ι_{i}^{n - 1} d_{n}^{(i)},$ where $ι_{i}^{n} : C_{n}^{(i)} \to Q_{n}$ is the $i$ th coproduct injection. By [L1], $d_{n - 1}^{Q} d_{n}^{Q} ι_{i}^{n} = d_{n - 1}^{Q} ι_{i}^{n - 1} d_{n}^{(i)} = ι_{i}^{n - 2} d_{n - 1}^{(i)} d_{n}^{(i)} = 0,$ so $d_{n - 1}^{Q} d_{n}^{Q} = 0$ because its composites with every injection vanish. Hence $Q_{∙}$ is the coproduct complex.

Depends on

Used by

Dependency tree · two levels

5 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

Charles A. Weibel, Chapter 1 of An Introduction to Homological Algebra (standard reference, not scraped)