TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-13

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.

For every ring R, the category R-Mod is complete and cocomplete

Statement

For every ring $R$ , the category $R - M o d$ of left $R$ -modules and $R$ -linear maps has all small limits and all small colimits.

Facts & Assumptions

Given: A fixed ring $R$ .

[L1]

Small products and equalizers characterize completeness, and small coproducts and coequalizers characterize cocompleteness (A category is complete exactly when it has all small products and equalizers, and cocomplete exactly when it has all small coproducts and coequalizers).

[F1]

Left modules and their homomorphisms form $R - M o d$ and obey the module and linearity axioms (Left modules over a fixed ring and module homomorphisms form the large locally small category $R - M o d$ , Unital left and right modules over a ring; unqualified module means left module, Module homomorphism and isomorphism, kernel, image and cokernel).

[F2]

Submodules are closed under addition, inverses, and scalar multiplication (Submodule of a module).

[F3]

A subset $B \subseteq M$ is a basis when every element of $M$ has a unique expression as a finite $R$ -linear combination of elements of $B$ , and a module possessing a basis is free (Generated submodule, cyclic and finitely generated modules, module basis and free module). This supplies the definition only; the free module on a set and its extension property are constructed in step 1.4 below.

[F4]

Quotients by submodules are modules, and a linear map factors uniquely through the quotient precisely when it kills that submodule (Quotient module $M / N$ with scalar multiplication on additive cosets, A module homomorphism vanishing on $N$ factors uniquely through $M / N$ ).

Proof

technique · explicit constructions and the criteria

1.1

A set-indexed Cartesian product of left $R$ -modules, with componentwise addition and scalar multiplication, is a module. Coordinatewise pairing gives its product universal property. The empty product is the zero module.

F1algebra

1.2

For parallel linear maps $f, g : M ⇉ N$ , their agreement set is $\ker (f - g)$ and is a submodule by [F1] and [F2]. Corestriction through its inclusion gives the equalizer universal property. Hence [L1] gives completeness.

F1F2L1

1.3

For $f, g : M ⇉ N$ , quotient $N$ by the submodule generated by ${f (m) - g (m) : m \in M}$ . The quotient map equalizes $f, g$ , and [F4] says every equalizing linear map factors through it uniquely. Thus this is a coequalizer.

F2F4

1.4

For a set $S$ , let $R^{(S)}$ be the set of functions $λ : S \to R$ vanishing outside some finite subset, with pointwise addition and scalar multiplication; these are again finitely supported, so [F1] makes $R^{(S)}$ a left $R$ -module. For $s \in S$ let $e_{s}$ take the value $1$ at $s$ and $0$ elsewhere. Each $λ$ is the finite sum $\sum_{s} λ (s) e_{s}$ over its support, and evaluating any such expression at a point of $S$ returns its coefficient there, so the expression is unique; hence ${e_{s} : s \in S}$ is a basis and $R^{(S)}$ is free in the sense of [F3]. Given a left $R$ -module $P$ and any function $g : S \to P$ , the assignment $λ \mapsto \sum_{s} λ (s) g (s)$ , summed over the finite support, is $R$ -linear by [F1] and sends $e_{s}$ to $g (s)$ ; and any linear map agreeing with $g$ on every $e_{s}$ agrees with it on every finite $R$ -combination of the $e_{s}$ , hence everywhere. So a linear map out of $R^{(S)}$ may be prescribed arbitrarily on the basis and is determined by that prescription.

F1F2F3algebra

2.1

For modules $(M_{i})$ , let $S = ∐_{i} {i} \times ∣ M_{i} ∣$ . In the free module $R^{(S)}$ of step 1.4, quotient by the submodule generated by $[i, 0]$ , $[i, x + y] - [i, x] - [i, y]$ , and $[i, r x] - r [i, x]$ . The maps $M_{i} \to R^{(S)} / N$ induced by $x \mapsto [i, x] + N$ are linear.

F2F4step 1.4

3.1

A family of linear maps $M_{i} \to P$ extends uniquely from $S$ to the free module by step 1.4, kills the displayed generators, and therefore factors uniquely through the quotient by [F4]. This is the coproduct universal property. For an empty family, it returns the zero module.

F4step 1.4step 2.1

4.1

Steps 2.1, 3.1, and 1.3 give all small coproducts and coequalizers, so [L1] gives cocompleteness.

L1step 2.1step 3.1step 1.3∎

Depends on

Used by

An infinite coproduct need not agree with the infinite product Counterexample
FALSE: every abelian category is equivalent to a module category False statement
Abelian groups form an abelian category Theorem
Module categories are Grothendieck categories Theorem
Modules over a ring form an abelian category Theorem

Dependency tree · two levels

24 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, Categories, Example 4.19.5 (standard reference, not scraped)
E. Riehl, Category Theory in Context, Section 3.6 (standard reference, not scraped)