Natural transformations of additive cocontinuous module functors are determined at the regular module

The identity functor $1_{A\text{-}\mathbf{M}\mathbf{o}\mathbf{d}}$ is additive, its induced maps on hom-groups being identity homomorphisms, and it preserves every colimit; hence it is additive cocontinuous.

If $F:A\text{-}\mathbf{M}\mathbf{o}\mathbf{d}\to B\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$ and $G:B\text{-}\mathbf{M}\mathbf{o}\mathbf{d}\to C\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$ are additive cocontinuous, then $GF$ is additive, a composite of hom-group homomorphisms being one, and cocontinuous, since for a small diagram $D$ with colimit $L$ the object $F(L)$ is a colimit of $F\circ D$ and $G(F(L))$ is a colimit of $G\circ F\circ D$.

Identity transformations and vertical composites are natural by [F4]. Associativity and the identity laws hold at each component. Thus the categorical operations satisfy their laws for fixed functor and transformation schemas; this does not form a category whose objects are proper classes.

Free modules: let $I$ be a set and let ${\iota }_i:A\to A^{(I)}$ be the coordinate inclusions of the free module $A^{(I)}={⨁}_{i\in I}A$, a coproduct of copies of $A$. Since $F$ and $G$ preserve this coproduct, $F(A^{(I)})$ with the maps $F({\iota }_i):M\to F(A^{(I)})$, where $M=F(A)$, is a coproduct of copies of $M$, and by [F9] a map out of $F(A^{(I)})$ is determined by its composites with the maps $F({\iota }_i)$; the same holds for $G(A^{(I)})$ with $N=G(A)$. Naturality [F3] gives ${\eta }_{A^{(I)}}\circ F({\iota }_i)=G({\iota }_i)\circ {\eta }_A$ for every $i$, so ${\eta }_{A^{(I)}}$ is determined by ${\eta }_A$: if ${\eta }_A=0$ then ${\eta }_{A^{(I)}}=0$.

Epic free covers: the canonical surjection $q_X:A^{(X)}\to X$ is an epimorphism, since two maps out of $X$ agreeing after composition with $q_X$ agree everywhere by surjectivity of $q_X$. Each of $F,G$ is right exact by [F8], and $A\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$, $B\text{-}\mathbf{M}\mathbf{o}\mathbf{d}$ are abelian by [F7], so $F(q_X)$ and $G(q_X)$ are epimorphisms by [F6].

Suppose ${\eta }_A={\theta }_A$ for two natural transformations $F\Rightarrow G$. Step 1.4 and naturality at every coordinate inclusion give ${\eta }_{A^{(X)}}={\theta }_{A^{(X)}}$. Naturality at $q_X$ then gives ${\eta }_X\circ F(q_X)=G(q_X)\circ {\eta }_{A^{(X)}}=G(q_X)\circ {\theta }_{A^{(X)}}={\theta }_X\circ F(q_X)$; epicness of $F(q_X)$ from step 1.5 yields ${\eta }_X={\theta }_X$. Hence the transformations agree at every module.

To obtain set codes, fix the defining formulas and parameters for $F,G$. For $h\in {\mathrm{Hom}}_B(F(A),G(A))$ and a module $X$, let $p_{h,X}:F(A^{(X)})\to G(X)$ be the unique map whose composite with $F({\iota }_x)$ is $G(q_X{\iota }_x)h$ for every $x\in X$; it exists by coproduct preservation and [F9]. Call $h$ admissible when, for every $X$, there is a map $a_X:F(X)\to G(X)$ with $a_{X}F(q_X)=p_{h,X}$, these maps satisfy $G(u)a_X=a_{Y}F(u)$ for every $u:X\to Y$, and $a_A=h$. The descents are unique by step 1.5, so this is a predicate quantifying only over sets and set-coded module maps, not over class families. Separation gives the set of admissible $h$. Every natural transformation gives such a code by naturality at $q_X{\iota }_x$, and each admissible code defines its component family uniquely. Together with steps 1.3 and 2.1 this proves the claimed schematic category laws and local smallness, without applying replacement to proper-class-valued outputs. No choice is used.