LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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.

An additive module functor is cocontinuous exactly when it is right exact and preserves coproducts

Statement

Let $A, B$ be unital rings and $F : A - M o d \to B - M o d$ additive. Then $F$ preserves all small colimits if and only if $F$ preserves cokernels and arbitrary direct sums. Equivalently, $F$ is additive cocontinuous (Additive cocontinuous module functors and their schematic category) if and only if it is right exact (preserves every finite colimit that exists, Left exact and right exact functors) and preserves arbitrary coproducts. No commutativity and no choice are used.

Facts & Assumptions

Given: Unital rings $A$ and $B$ and an additive functor $F : A - M o d \to B - M o d$ .

[F1]

$F$ is additive cocontinuous when it is additive and preserves every small colimit (Additive cocontinuous module functors and their schematic category).

[F2]

A functor is right exact when it preserves every finite colimit that exists in its source category (Left exact and right exact functors).

[F3]

If $D : J \to C$ is small and the coproducts $R = ∐_{u : j \to k} D (j)$ , $S = ∐_{j} D (j)$ and the coequalizer of $d, c : R ⇉ S$ , with $d ι_{u} = ι_{j}$ and $c ι_{u} = ι_{k} D (u)$ , exist, then that coequalizer is a colimit of $D$ , with cocone built from the coproduct inclusions and the coequalizer map (Every small colimit can be constructed as a coequalizer between coproducts over the arrows and objects of the index category).

[F4]

$A - M o d$ has all small colimits (For every ring R, the category R-Mod is complete and cocomplete).

[F5]

In the additive category $A - M o d$ a coequalizer of a parallel pair is exactly a cokernel of the difference, and conversely (In a preadditive category, the coequalizer of a parallel pair is the cokernel of their difference); a cokernel is a coequalizer of the pair $(f, 0)$ , hence a finite colimit.

[F6]

An additive functor between additive categories preserves finite biproducts (An additive functor preserves finite biproducts).

[F7]

$A - M o d$ and $B - M o d$ are abelian, hence additive (Modules over a ring form an abelian category).

[F8]

In a module category the direct sum $⨁_{i \in I} X_{i}$ is the coproduct of the family with coordinate inclusions $ȷ_{i}$ , so a functor preserving arbitrary direct sums carries the coproduct cone of every family to a coproduct cone, and conversely (The direct sum of an indexed family of modules, Universal property of a direct sum of modules).

Proof

technique · direct

1.1F1F2F5F8

If $F$ preserves all small colimits, then it preserves cokernels and arbitrary direct sums, since a cokernel is the coequalizer of the pair $(f, 0)$ and a direct sum is a coproduct, both small colimits by [F5] and [F8]; and it is right exact, since every finite colimit is a small colimit. Hence the first alternative implies the second.

1.2F3F4F8

Conversely assume $F$ preserves cokernels and arbitrary direct sums, and let $D : J \to A - M o d$ be a small diagram with colimit $L$ . By [F4] the coproducts $R = ∐_{u : j \to k} D (j)$ and $S = ∐_{j} D (j)$ exist, and by [F3] the coequalizer $q : S \to L$ of $d, c : R ⇉ S$ is a colimit of $D$ with its canonical cocone.

1.3F2F3F5F6F8

The two hypothesis families agree for additive $F$ : if $F$ is right exact and preserves arbitrary coproducts, then it preserves cokernels, since cokernels are finite colimits; and conversely, if $F$ preserves cokernels and arbitrary direct sums, then it preserves every finite coproduct by [F6], because finite coproducts in an additive category are finite biproducts, and it preserves every finite colimit by the finite instance of the construction [F3] together with [F5], since the coproducts over the arrows and objects of a finite index category are finite coproducts. Hence cokernel-plus-direct-sum preservation is equivalent to right-exactness-plus-coproduct preservation.

2.1F3F5F7F8step 1.2

Under the assumption of step 1.2, $F (R)$ together with the maps $F (ι_{u})$ is a coproduct of the family $(F (D (j)))_{u : j \to k}$ and $F (S)$ with the maps $F (ι_{j})$ is a coproduct of the family $(F (D (j)))_{j}$ , because $F$ preserves the coproduct cones by [F8]; moreover $F (d) \circ F (ι_{u}) = F (ι_{j})$ and $F (c) \circ F (ι_{u}) = F (ι_{k}) F (D (u))$ , and $F (q)$ is a cokernel of $F (d - c) = F (d) - F (c)$ because $F$ preserves the cokernel of $d - c$ . By [F5] applied in $B - M o d$ , $F (q)$ is therefore the coequalizer of $F (d), F (c)$ , and by [F3] applied to the small diagram $F \circ D$ the object $F (L)$ with the image of the colimit cocone of $D$ is a colimit of $F \circ D$ . Hence $F$ preserves the colimit of $D$ .

3.1F1step 1.1step 1.3step 2.1∎

Step 1.1 gives the forward and step 2.1 the reverse implication of the first equivalence, so an additive $F$ preserves all small colimits exactly when it preserves cokernels and arbitrary direct sums; step 1.3 identifies the second hypothesis family with right exactness plus coproduct preservation, so $F$ is additive cocontinuous if and only if it is right exact and preserves arbitrary coproducts. No element, presentation, or diagram is chosen globally, so no choice is used.

Depends on

Used by

Cited to discharge well-definedness by Additive cocontinuous module functors and their schematic category.

Dependency tree · two levels

33 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

M. Kamensky, Non-Commutative Algebra (BGU course notes, Spring 2017), §5.1, Theorem 5.1.43, Proposition 5.1.40, Lemma 5.1.46, Corollaries 5.1.48-5.1.49 (standard reference, not scraped)
A. Nyman and S. P. Smith, A Generalization of Watts's Theorem: Right Exact Functors on Module Categories, arXiv:0806.0832, Theorem 1.1-1.2, Propositions 3.2-3.3, Lemma 3.4 (standard reference, not scraped)