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.

Additive functors from a ring to abelian groups are left modules

Statement

Let $R$ be viewed as the one-object preadditive category of A one-object preadditive category is the same thing as a ring. Then an additive functor $F : R \to A b$ determines a left $R$ -module on the abelian group $F (*)$ , and every left $R$ -module arises in this way.

Facts & Assumptions

Given: A ring $R$ , its one-object preadditive category with object $*$ , and an additive functor $F : R \to A b$ or a left $R$ -module $M$ .

[L1]

A ring may be read as a one-object preadditive category whose endomorphisms compose by ring multiplication (A one-object preadditive category is the same thing as a ring).

[L2]

A left $R$ -module is an abelian group with an action satisfying the four module axioms (Unital left and right modules over a ring; unqualified module means left module).

[L3]

A module homomorphism preserves the additive group law and the scalar action (Module homomorphism and isomorphism, kernel, image and cokernel).

Proof

technique · direct

1.1

Let $M : = F (*)$ . Since $F$ is additive, the map $F (r) : M \to M$ is a group homomorphism for each $r \in R$ . Define $r \cdot m : = F (r) (m)$ .

L1L2

1.2

Conversely, if $M$ is a left $R$ -module, define $F_{M} (*) = M$ and $F_{M} (r) (m) = r \cdot m$ . The module axioms in [L2] give preservation of addition on the unique hom-set, preservation of composition, and preservation of the identity. So $F_{M}$ is an additive functor.

L1L2

2.1

The identity morphism of $*$ is $1_{R}$ by [L1], so $1_{R} \cdot m = F (1_{R}) (m) = m$ . Also $(r s) \cdot m = F (r s) (m) = F (r) F (s) (m) = r \cdot (s \cdot m)$ . Additivity of $F$ on the hom-group $R$ gives $(r + s) \cdot m = r \cdot m + s \cdot m$ , and each $F (r)$ being a group homomorphism gives $r \cdot (m + n) = r \cdot m + r \cdot n$ . Thus $M$ is a left $R$ -module by [L2].

L1L2step 1.1

3.1

Steps 2.1 and 1.2 are inverse constructions on the underlying action, so additive functors $R \to A b$ are exactly left $R$ -modules. If one also tracks maps between such functors, the same equations are exactly the ones in [L3] for module homomorphisms.

L2L3step 2.1step 1.2∎

Depends on

Used by

Additive functors out of the matrix category Example

Dependency tree · two levels

10 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

Kiran S. Kedlaya, Solid modules over an ordinary ring, Example 1.2.2 (standard reference, not scraped)
Mike Prest, Modules as exact functors, Modules as functors (standard reference, not scraped)