TheoremStatement: AI-adaptedProof: 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.

The hom-bifunctor of a preadditive category takes values in abelian groups

Statement

If $C$ is preadditive, then each hom-set $C (A, B)$ is an abelian group, the covariant and contravariant hom-functors take values in $A b$ , and the hom-bifunctor lifts from $S e t$ to $A b$ .

Facts & Assumptions

Given: A preadditive category $C$ and objects $A, B$ .

[L1]

The hom-assignment is a bifunctor to $S e t$ (The hom-assignment $C (-, -) : C^{o p} \times C \to S e t$ is a bifunctor).

[L2]

The covariant, contravariant, and bifunctorial hom-assignments have the displayed actions on morphisms (The covariant and contravariant hom-assignments and the hom-bifunctor of a locally small category).

[L3]

In a preadditive category, hom-sets are abelian groups and composition is bilinear (Preadditive category).

Proof

technique · direct

1.1L3

The first clause is immediate from [L3]: each $C (A, B)$ is already an abelian group.

1.2L2L3

If $u : B \to B^{'}$ , then the map $u_{*} : C (A, B) \to C (A, B^{'})$ of [L2] is a group homomorphism because $u_{*} (f + g) = u (f + g) = u f + u g = u_{*} (f) + u_{*} (g)$ by bilinearity in [L3]. The same calculation shows that precomposition $h^{*} : C (B^{'}, A) \to C (B, A)$ is a group homomorphism.

2.1L1step 1.1step 1.2∎

Step 1.2 shows that the one-variable hom-functors actually land in $A b$ , and [L1] then lifts the whole hom-bifunctor to $A b$ because its action in each variable is additive.

Depends on

Used by

Dependency tree · two levels

9 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: Preadditive and additive categories (standard reference, not scraped)