Recovering addition from products and coproducts
Written by GPT-6.1 Sol (OpenAI), reasoning effort Ultra, October 2026. Self-checked by GPT-6.1 Sol, the AI that wrote it; no independent review. Public domain (CC0).
Addition of maps can be part of a category's definition. It can also be forced by the category's ordinary universal properties. A zero object gives zero maps, and a compatible product and coproduct give a way to combine two maps. An inverse condition then turns this combination into an abelian group operation.
This recovery explains a useful rigidity phenomenon. A functor to sets that preserves finite products automatically carries abelian group structures. Natural transformations between such functors preserve those structures, even when their components were initially arbitrary functions.
We assume categories, finite products and coproducts, natural transformations and abelian groups. All categories are locally small in a fixed universe; their object collections need not be small. Functor categories can be formed in a larger universe when necessary. Retain the complete zero-object proof, product-to-coproduct proof and binary additive-functor criterion in the AI-integrated Stacks baseline. Section 1 supplies the exact zero-map and coordinate interfaces used below. Mathlib's Preadditive.Biproducts provides the corresponding constructions. The lesson Formal linear combinations and finite sums develops the corresponding free constructions.
1. The enriched starting point
A category is preadditive when each set of maps is an abelian group and composition is additive in each variable. A functor between preadditive categories is additive when its map on each group of maps is a group homomorphism. These are the definitions in Stacks, Definition 12.3.1.
For example, the category \(\mathbf{Ab}\) of abelian groups is preadditive. If \(f,g:A\to B\) are group homomorphisms, their pointwise sum is a homomorphism because \(B\) is commutative. Pointwise zero and negatives give an abelian group of homomorphisms. Distributing composition over pointwise addition proves both required distributive laws.
In a preadditive category, either an initial object or a terminal object is a zero object. Equivalently, an object \(Z\) is zero when \(1_Z=0\). Maps factoring through a zero object are exactly the zero maps. Retain the complete canonical zero-object equivalence. For the factorization assertion, the maps into and out of a zero object are the unique maps and hence the zeros of their groups of maps. Bilinearity makes their composite zero. Conversely, this composite exists for each pair of objects and equals the zero map, giving its factorization. Thus the ordinary zero maps used later agree exactly with the enriched zero maps.
Here is the precise canonical product interface we will use. Suppose maps \(i_s:X_s\to B\) and \(p_r:B\to X_r\), for \(r,s\in\{1,2\}\), satisfy
\[ \begin{gathered} p_ri_s=\begin{cases}1&r=s,\\0&r\ne s,\end{cases}\\ i_1p_1+i_2p_2=1_B. \end{gathered} \tag{1.1} \]Then \(B\) is both a product, with projections \(p_r\), and a coproduct, with inclusions \(i_s\). Here are the inverse maps in the coordinate criterion. Given \(a\colon T\to X_1\), \(b\colon T\to X_2\), the map \(i_1a+i_2b\) has projections \(a,b\). If \(h\colon T\to B\) has those projections, the second equation gives \(h=(i_1p_1+i_2p_2)h=i_1a+i_2b\), proving uniqueness. Given \(a\colon X_1\to T\), \(b\colon X_2\to T\), the map \(ap_1+bp_2\) has restrictions \(a,b\). Any map \(k\colon B\to T\) with those restrictions satisfies \(k=k(i_1p_1+i_2p_2)=ap_1+bp_2\), proving the coproduct property too.
Conversely, a product supplies the unique inclusions with identity and zero coordinates. The complete canonical product-to-coproduct proof shows that \(i_1p_1+i_2p_2\) has the same two projections as \(1_B\), so it is \(1_B\). The preceding coordinate formulas then specify the coproduct on this very object. For the reverse direction, apply that proved product-to-coproduct result to \(C^{\mathrm{op}}\): its groups of maps are the same groups with reversed objects, and both distributive laws hold because the original composition is bilinear. A coproduct in \(C\) is a product in \(C^{\mathrm{op}}\); the resulting inclusions there are the projections in \(C\). Reversing the coordinate identities gives exactly (1.1), and the displayed inverse formulas give both universal structures in \(C\). This supplies the precise dual interface without adding a zero object or any other products. Mathlib provides the corresponding finite and binary constructions in the reference above.
In particular, when a product exists, the coproduct exists too. The canonical comparison from the coproduct to the product is invertible: its coordinates on the two inclusions are the identity and zero entries of (1.1). The simultaneous object is a biproduct, written \(X_1\oplus X_2\). For a small, possibly infinite family, the notation \(\bigoplus_i X_i\) means its coproduct when that exists; it does not assert that an infinite product is the same object.
An additive category in the enriched convention is a preadditive category with all finite products, including the empty product. The empty product is terminal and hence zero, and binary products are biproducts. This is Stacks, Definition 12.3.8. We now recover this convention from ordinary categorical data.
2. A monoid law without sums of maps
For this section assume only the following ordinary structures. The category \(C\) has a zero object \(0\), binary products and binary coproducts. Zero maps are defined by factorization through \(0\). For every pair, the canonical map
\[ r_{X,Y}:X\amalg Y\longrightarrow X\times Y \tag{2.1} \]is invertible. Its coordinates on the coproduct inclusions are identity maps on the matching factor and zero maps on the other factor. No group structure on a set of maps is assumed here.
Regard \(X\times Y\) also as a coproduct, transporting its inclusions through \(r_{X,Y}\). Denote it by \(X\oplus Y\). Its inclusions are the product maps with coordinates \((1,0)\) and \((0,1)\). The codiagonal of the transported coproduct gives a map
\[ \begin{gathered} \mu_X:X\times X\longrightarrow X, \\ \mu_X=[1_X,1_X]. \end{gathered} \tag{2.2} \]The brackets in (2.2) mean the unique map out of a coproduct with the indicated restrictions. They do not mean a sum of maps.
Lemma 2.1. The maps \(\mu_X\) and \(e_X:0\to X\) make \(X\) a commutative monoid object. Every map \(h:X\to Y\) preserves these monoid structures.
Proof. The two axes of \(X\times X\) are its transported coproduct inclusions. Restriction of \(\mu_X\) to either axis is \(1_X\), proving both unit identities. Interchanging the two factors interchanges the inclusions; both restrictions remain \(1_X\). Coproduct uniqueness therefore proves commutativity.
Iterating the biproduct gives an object \(X\oplus X\oplus X\) which is both the threefold product and the threefold coproduct. To see the identification precisely, each parenthesized object has the three coordinate projections of the product and the three inclusions of the coproduct. The unique product comparison between parenthesizations takes every inclusion to the matching inclusion, by its three coordinates. Thus the two structures agree under that comparison.
The maps \(\mu_X(\mu_X\times1_X)\) and \(\mu_X(1_X\times\mu_X)\) restrict to \(1_X\) on each of the three inclusions. For instance, the first restriction first enters the first axis of the inner pair and then the first axis of the outer pair. The third restriction enters the second axis of the outer pair. The other restrictions are checked in the same way, using zero maps on the unused coordinates and the two unit identities. Threefold coproduct uniqueness proves associativity.
Finally, \(h\mu_X\) and \(\mu_Y(h\times h)\) restrict to \(h\) on each axis. Indeed, \(h\times h\) takes an axis to the corresponding axis followed by \(h\), as follows by the two product projections. The two maps are equal by coproduct uniqueness. Also \(he_X=e_Y\), since there is only one map \(0\to Y\). Hence every \(h\) preserves multiplication and the unit. \(\square\)
Each set \(\operatorname{Hom}_C(T,X)\) consequently has a commutative monoid operation
\[ \begin{gathered} f+g=\mu_X\langle f,g\rangle, \\ 0_{T,X}:T\to0\to X. \end{gathered} \tag{2.3} \]Here the angled brackets mean the product pairing. The monoid identities follow by composing the identities in Lemma 2.1 with the appropriate pairings. Precomposition preserves this operation because pairings commute with precomposition. Postcomposition preserves it by the last assertion of that lemma. Thus composition distributes over (2.3), although negatives may not exist.
3. The inverse condition and unique enrichment
Add one more ordinary condition: for each \(X\), there exists a map \(a_X:X\to X\) such that
\[ \mu_X\langle a_X,1_X\rangle=0_{X,X}. \tag{3.1} \]In terms of the original products and coproducts, (3.1) is the composite of the diagonal, \(a_X\times1_X\), the inverse of \(r_{X,X}\), and the codiagonal. It uses only the structures already specified.
Theorem 3.1. A category satisfying the zero-object, product, coproduct, comparison and inverse conditions above has a unique preadditive structure. In that structure it is additive, and (2.3) is its addition of maps. Conversely, a preadditive category with finite products satisfies all these ordinary conditions.
Proof. For any \(f:T\to X\), composing (3.1) with \(f\) gives
\[ a_Xf+f=0_{T,X}. \tag{3.2} \]Commutativity gives the inverse identity in the other order. Each commutative monoid \(\operatorname{Hom}_C(T,X)\) is therefore an abelian group. The distributive laws proved after Lemma 2.1 make \(C\) preadditive. Its existing products and zero object give all finite products, so it is additive.
The map \(a_X\) is forced: it is the inverse of \(1_X\) in the just-constructed group of endomorphisms. Every \(h:X\to Y\) commutes with these inverse maps. Its preservation of the monoid operations takes inverses to inverses, so \(ha_X=a_Yh\). In particular, each \(X\) is a commutative group object, with multiplication \(\mu_X\), unit \(e_X\), and inverse \(a_X\).
For uniqueness, suppose the same ordinary category already has some preadditive structure. The zero of a group of maps is exactly the map through the zero object, by the zero-object criterion in Section 1. Its biproduct inclusions have the fixed identity and zero coordinates, so they are the same inclusions used above. If \(f,g:T\to X\), the map \(i_1f+i_2g\) has projections \(f,g\), by bilinearity and the coordinate identities. It is therefore \(\langle f,g\rangle\). Composing with \(\mu_X\), whose restrictions to the inclusions are identities, gives
\[ \mu_X\langle f,g\rangle=f+g \tag{3.3} \]for the existing group operation. Thus every preadditive structure has precisely (2.3) as its addition. A group's zero and inverse are determined by addition, proving uniqueness of the whole structure. Mathlib also records this uniqueness once zero maps and binary biproducts are fixed; the zero object here fixes those zero maps.
Conversely, in a preadditive category with finite products, the terminal object is zero and Section 1 supplies binary coproducts and the invertible canonical comparisons. The map \(-1_X\) satisfies (3.1), because the recovered operation agrees with the given addition. This verifies the inverse condition as well. \(\square\)
The construction is independent of choices of products and coproducts. The unique comparisons preserving their projections and inclusions carry \(\mu_X\), its pairings and its unit to the corresponding maps for the other choices, so (2.3) gives the identical operation on the original sets of maps.
The opposite category is additive too. Reverse composition in the abelian groups of maps; both distributive laws remain valid. Finite products in the opposite are the finite coproducts supplied by the biproducts. The converse direction of Theorem 3.1 then supplies the ordinary conditions in the opposite category, including its inverse condition. Its product-coproduct comparison is represented, in the original category, by the inverse of the original comparison.
There is also a symmetric formula for addition. Writing \(\Delta_T:T\to T\oplus T\) for the diagonal and \(\nabla_X:X\oplus X\to X\) for the codiagonal, one has
\[ f+g=\nabla_X(f\oplus g)\Delta_T. \tag{3.4} \]Indeed, the map \((f\oplus g)\Delta_T\) has projections \(f,g\), so it is the pairing in (2.3). The same formula holds when only the two indicated doubled biproducts exist in a preadditive category: their given zero maps and Section 1's criterion give \(\Delta_T=i_1+i_2\); the codiagonal composed with \((f\oplus g)i_1\) is \(f\), and its composite with \((f\oplus g)i_2\) is \(g\). Bilinearity now gives (3.4), without requiring a zero object or other biproducts.
4. Product-preserving functors to sets
Let \(C\) be additive and let \(F:C\to\mathbf{Set}\) preserve finite products. Preservation here means that the canonical comparison
\[ \begin{gathered} c_{X,Y}:F(X\times Y) \\ \longrightarrow F(X)\times F(Y) \end{gathered} \tag{4.1} \]given by the two projections is bijective, and \(F(0)\) is a singleton. Define operations on the set \(F(X)\) by
\[ \begin{aligned} u+v&=F(\mu_X)c_{X,X}^{-1}(u,v),\\ 0&=F(e_X)(*),\\ -u&=F(a_X)(u). \end{aligned} \tag{4.2} \]The symbol \(*\) is the unique element of \(F(0)\).
Proposition 4.1. These operations make \(F(X)\) an abelian group. Every \(F(h)\) is a group homomorphism, and thus \(F\) lifts to a functor \(\widetilde F:C\to\mathbf{Ab}\) on the very same underlying sets and functions.
Proof. Product comparisons commute with pairings: for maps \(s:W\to X\), \(t:W\to Y\), both coordinates of \(c_{X,Y}F\langle s,t\rangle\) are \(F(s),F(t)\). They also commute with permutations and with iterated product comparisons, since all coordinate projections agree. Applying \(F\) to the associativity and commutativity identities for \(\mu_X\), then using these comparisons, proves associativity and commutativity in (4.2).
For the unit, the image of the axis \(\langle1_X,0\rangle\) is the function \(u\mapsto(u,0)\): its first coordinate is \(u\), and its second factors through the singleton \(F(0)\). Applying \(F\) to the unit identity for that axis gives \(u+0=u\). The other axis gives \(0+u=u\). The image of (3.1) gives \((-u)+u=0\), and commutativity gives the other inverse identity. These are all the abelian group axioms.
The identity \(h\mu_X=\mu_Y(h\times h)\) from Lemma 2.1, together with the naturality of product comparisons, proves that \(F(h)\) preserves addition. The identity \(he_X=e_Y\) proves preservation of zero, and inverses then follow. The existing functor identity and composition laws are unchanged as equalities of functions. They are therefore also the functor laws in \(\mathbf{Ab}\). \(\square\)
No extra choice of group operation was made. The operations are the explicit functions in (4.2). The lift preserves finite products in \(\mathbf{Ab}\): its comparisons are bijective group homomorphisms, and its value at \(0\) is the trivial group.
Lemma 4.2. If \(H:C\to\mathbf{Ab}\) is an ordinary functor preserving finite products, the recovered group structure on its underlying sets is its already given group structure.
Proof. Its value \(H(0)\) is the trivial group, so \(H\) takes each map through \(0\) to the zero homomorphism. The images of the two axes of \(X\times X\) are consequently the ordinary group inclusions \(u\mapsto(u,0)\) and \(v\mapsto(0,v)\). The function
\[ \begin{gathered} H(\mu_X)c_{X,X}^{-1}: \\ H(X)\times H(X)\longrightarrow H(X) \end{gathered} \tag{4.3} \]is a group homomorphism, because its two factors are group homomorphisms. Its restriction to each axis is the identity. Every pair is the sum of its two axis elements, so (4.3) sends \((u,v)\) to the already given sum \(u+v\). Zero and inverse then agree too. \(\square\)
5. All natural transformations and compatible uniqueness
Let \(F,G:C\to\mathbf{Set}\) both preserve finite products. Suppose \(\alpha:F\to G\) is any natural transformation of sets.
Theorem 5.1. Every component \(\alpha_X\) is a homomorphism for the groups in (4.2). In particular, for product-preserving functors to \(\mathbf{Ab}\), forgetting group structures gives a bijection on their sets of natural transformations.
Proof. Naturality on the two projections gives
\[ c^G_{X,X}\alpha_{X\times X} =(\alpha_X\times\alpha_X)c^F_{X,X}. \tag{5.1} \]Use this equation and naturality on \(\mu_X\) in (4.2). For any \(u,v\), the result is
\[ \alpha_X(u+v)=\alpha_X(u)+\alpha_X(v). \tag{5.2} \]Naturality on \(e_X\) proves preservation of zero: the component \(\alpha_0\) is the unique function between singletons. Hence \(\alpha_X\) is a group homomorphism, including preservation of negatives. The same component maps remain natural in \(\mathbf{Ab}\), because equality of group homomorphisms is equality of their underlying functions. Conversely, every natural transformation in \(\mathbf{Ab}\) gives one in sets. Forgetting is injective on each set of component maps, so the correspondence is bijective. Lemma 4.2 identifies the recovered operations with the original operations when the two functors already take values in \(\mathbf{Ab}\). \(\square\)
Thus the forgetful functor from finite-product-preserving \(\mathbf{Ab}\)-valued functors to finite-product-preserving set-valued functors is fully faithful, and Proposition 4.1 makes it essentially surjective. It is an equivalence of these categories. If the source is large, this statement is interpreted in a universe containing the relevant collections of natural transformations; it does not assert they form small sets in the original universe.
The uniqueness assertion has a precise comparison requirement. Given a product-preserving lift \(H:C\to\mathbf{Ab}\) and a specified natural isomorphism
\[ \eta:UH\xrightarrow{\sim}F, \tag{5.3} \]where \(U\) forgets group structures, there is exactly one natural isomorphism \(H\to\widetilde F\) whose underlying comparison is \(\eta\). Theorem 5.1 applied to \(\eta\) and its inverse supplies the isomorphism; faithfulness gives uniqueness. Comparisons between two such lifts are likewise uniquely determined by the specified identifications with \(F\).
Even if product preservation of \(H\) was not specified, (5.3) forces it. The natural comparison (4.1) becomes a bijection on underlying sets after conjugation by \(\eta\). It is a group homomorphism and hence an isomorphism in \(\mathbf{Ab}\); similarly, \(H(0)\) has a one-element underlying set. The preceding uniqueness result therefore still applies.
There need not be just one unrestricted isomorphism between the lifts. For example, the identity functor on \(\mathbf{Ab}\) has both identity and negation as natural automorphisms. Exactly one respects a chosen underlying identity comparison. Specifying the comparison is what makes the isomorphism unique.
6. Recognizing additive functors
The recovered addition also detects when an ordinary functor \(K:C\to D\) between additive categories is additive. We retain the stronger canonical criterion from the complete canonical additive-functor proof: preserving binary products alone, preserving binary coproducts alone, and being additive are equivalent. Each entails preservation of all finite products and coproducts, including the zero object.
For the finite-product direction needed here, the mechanism is explicit. Preservation of \(0\) implies preservation of zero maps. Under product comparisons the images of the axes of \(X\times X\) are the axes of \(KX\times KX\), by their identity and zero coordinates. The map \(K(\mu_X)\) consequently has identity restrictions on both axes, so it is \(\mu_{KX}\). The image of the pairing \(\langle f,g\rangle\) is the corresponding pairing. Applying \(K\) to (2.3) therefore gives
\[ K(f+g)=K(f)+K(g). \tag{6.1} \]Conversely, an additive functor preserves (1.1), so it preserves binary biproducts. It also preserves a zero object since it sends \(1_0=0\) to \(1_{K0}=0\). Iteration gives the finite products. In particular the lift \(\widetilde F\) of Section 4 is additive as a functor to \(\mathbf{Ab}\).
For abelian groups the recovered operations are pointwise, as Section 1 shows. For vector spaces they give the usual sums of linear maps. The following exercises examine both the rigidity and its hypotheses.
7. Four graded exercises
Exercise 1 (foundational). Let \(C_{\mathbb N}\) have objects the nonnegative integers and maps \(m\to n\) the \(n\times m\) matrices over \(\mathbb N\), with matrix multiplication as composition. Show that it has a zero object and all canonical binary product-coproduct comparisons are invertible. Compute the operation (2.3). Show that it fails the inverse condition for the object \(1\), and that its underlying ordinary category cannot carry a preadditive structure.
Solution. The object \(0\) has unique maps in either direction, represented by empty matrices. For objects \(m,n\), take \(m+n\), with the two block inclusions and block projections. A matrix into \(m+n\) is uniquely its two row blocks, giving the product property. A matrix out of \(m+n\) is uniquely its two column blocks, giving the coproduct property. The canonical comparison is the identity matrix on this common object. Thus all the required comparisons are invertible.
For an object \(n\), the codiagonal is the block row \([I_n\ I_n]\). The pairing of two matrices \(A,B:m\to n\) is their stacked block column. Multiplication gives
\[ [I_n\ I_n]\begin{pmatrix}A\\B\end{pmatrix}=A+B, \tag{7.1} \]with entrywise addition in \(\mathbb N\). For \(n=1\), an inverse map would be a one-entry matrix \([a]\) with \(a\in\mathbb N\) and \(a+1=0\), which is impossible. If a preadditive structure existed on this same ordinary category, its terminal object would be zero and Section 3's uniqueness argument would force its addition to be this entrywise addition. The identity \([1]\) would then have no additive inverse, a contradiction. The example shows why a zero object and biproducts alone do not suffice.
Exercise 2 (intermediate). Let \(U:\mathbf{Ab}\to\mathbf{Set}\) be the forgetful functor. Classify all natural transformations \(U\to U\) and all natural transformations \(U\times U\to U\). Which transformations \(U\to U\) are natural automorphisms? Show directly how naturality forces additivity of each component in both classifications.
Solution. For \(\tau:U\to U\), put \(n=\tau_{\mathbb Z}(1)\in\mathbb Z\). Given \(x\in A\), there is a group homomorphism \(s_x:\mathbb Z\to A\) with \(s_x(1)=x\). Naturality forces
\[ \tau_A(x)=s_x(n)=nx. \tag{7.2} \]Conversely, multiplication by any fixed integer is natural in group homomorphisms. Thus the integer \(n\) classifies \(\tau\), and (7.2) is additive on every abelian group. If \(\tau\) is invertible, its component on \(\mathbb Z\) is invertible, forcing \(n=1\) or \(n=-1\). Both values give natural automorphisms.
For \(\beta:U\times U\to U\), evaluate on the ordered pair of basis vectors \((e_1,e_2)\) in \(\mathbb Z^2\). Write its value as \(me_1+ne_2\). Every pair \((x,y)\) in any abelian group \(A\) is the image of that ordered pair under the homomorphism \(\mathbb Z^2\to A\) with those two basis images. Naturality therefore forces
\[ \beta_A(x,y)=mx+ny. \tag{7.3} \]Every pair \((m,n)\in\mathbb Z^2\) gives such a natural operation, uniquely. For pairs \((x,y),(x',y')\), the value on their sum is \(m(x+x')+n(y+y')\), which equals the sum of the two values by commutativity in \(A\). Hence each \(\beta_A:A\times A\to A\) is a group homomorphism. These arguments start with arbitrary functions and use only naturality to force their linear formulas.
Exercise 3 (advanced). On finite-dimensional rational vector spaces let \(Q(V)=V\otimes_{\mathbb Q}V\), and let \(Q(f)=f\otimes f\). Show that \(Q\) is an ordinary functor but is not additive. Compute the kernel of the canonical binary-product comparison for \(V,W\). Show that \(v\mapsto v\otimes v\) is a natural transformation of underlying sets from the identity functor to \(Q\), but has a nonadditive component. Explain why Theorem 5.1 does not apply.
Solution. Tensor multiplication respects composition, so \(Q(gf)=Q(g)Q(f)\), and \(Q(1)=1\). Thus \(Q\) is a functor. On \(\mathbb Q\), however, \(Q(2\cdot1)=4\cdot1\), while \(Q(1)+Q(1)=2\cdot1\). These endomorphisms differ, so it is not additive.
Distributing the tensor product of \(V\oplus W\) with itself gives four summands. The comparison induced by the two product projections is identity on the matching summands and zero on the crossed summands. Its kernel is
\[ (V\otimes W)\oplus(W\otimes V), \tag{7.4} \]of dimension \(2\dim(V)\dim(W)\). In particular, for two one-dimensional nonzero spaces the comparison is not invertible. Hence \(Q\), including its underlying set-valued functor, fails binary-product preservation.
The functions \(d_V(v)=v\otimes v\) are natural, because \((f\otimes f)(v\otimes v)=f(v)\otimes f(v)\). In \(V=\mathbb Q^2\), for basis vectors \(e_1,e_2\), the difference
\[ \begin{gathered} d_V(e_1+e_2) \\ {}-d_V(e_1)-d_V(e_2) \\ =e_1\otimes e_2+e_2\otimes e_1 \end{gathered} \tag{7.5} \]is nonzero: the two crossed elementary tensors are distinct basis elements of \(V\otimes V\). Thus \(d_V\) is not additive. The target functor in this natural transformation does not preserve finite products, so the hypothesis of Theorem 5.1 fails exactly where the crossed terms occur.
Exercise 4 (synthesis). Let \(\mathrm{Free}_{\mathbb Z}\) be the category with objects \(\mathbb Z^n\), \(n\geq0\), and all group homomorphisms between them, represented by integer matrices. Classify its finite-product-preserving functors to sets and all their natural transformations. Construct the correspondence with abelian groups explicitly and verify its action on every matrix, not just on the coordinate projections.
Solution. Start with an abelian group \(A\). Define \(F_A(\mathbb Z^n)=A^n\), including \(A^0=\{*\}\). For an \(m\times n\) integer matrix \(M\), set
\[ F_A(M)(x)_i=\sum_{j=1}^n M_{ij}x_j. \tag{7.6} \]The identity matrix acts as the identity, and applying (7.6) twice gives the coefficient sum \(\sum_i N_{ki}M_{ij}\), so \(F_A(NM)=F_A(N)F_A(M)\). Empty sums give the unique maps involving \(A^0\). Block projections identify \(F_A(\mathbb Z^{n+m})\) with \(A^n\times A^m\), so finite products are preserved.
Conversely, let \(F\) preserve finite products and put \(A=F(\mathbb Z)\) with the group structure of Section 4. Its lift \(\widetilde F\) is additive by Section 6. The product comparison gives a specified isomorphism
\[ c_n:F(\mathbb Z^n)\xrightarrow{\sim}A^n \tag{7.7} \]of groups. Denote coordinate inclusions and projections by \(i_j\) and \(p_i\). For a matrix \(M:\mathbb Z^n\to\mathbb Z^m\), its entry equation is \(p_iMi_j=M_{ij}1_{\mathbb Z}\). Additivity of the lift makes the corresponding image equation multiplication by \(M_{ij}\) on \(A\). Also, under \(c_n\), each \(F(i_j)\) is the inclusion of the \(j\)-th coordinate: its projections are identities on the matching coordinate and zero elsewhere.
Every element of \(A^n\) is the sum of these coordinate inclusions of its entries. Since \(F(M)\) is a group homomorphism, its \(i\)-th output coordinate is exactly (7.6). Therefore the maps \(c_n\) form a natural isomorphism \(F\to F_A\) on all integer matrices, including those with negative entries and all empty matrices.
For two groups \(A,B\), any group homomorphism \(t:A\to B\) induces the natural transformation \(t^n:A^n\to B^n\); formula (7.6) verifies naturality on every matrix. Conversely, a natural transformation \(F_A\to F_B\) has group-homomorphism components by Theorem 5.1. Put \(t=\alpha_{\mathbb Z}\). Naturality on the coordinate projections forces \(\alpha_{\mathbb Z^n}=t^n\), including the unique component at \(n=0\). Thus all transformations are accounted for, and evaluation at \(\mathbb Z\) and the construction \(A\mapsto F_A\) are inverse up to the specified natural isomorphisms (7.7). This gives the asserted equivalence with \(\mathbf{Ab}\).
References
- The Stacks Project Authors, AI-integrated fork at the linked immutable revision, Homology: complete proofs of the zero-object equivalence, product-to-coproduct construction and binary additive-functor criterion. The canonical source remains available under GFDL 1.2 or later; no canonical text is copied here. Section 1 supplies the zero-factorization and full coordinate/dual interfaces.
- The Stacks Project, Section 12.3: preadditive structures, zero objects and finite biproducts.
- The Stacks Project, Lemma 12.7.1: the binary-product and binary-coproduct criteria for additive functors.
- Mathlib, Preadditive.Biproducts: finite and binary biproduct constructions and uniqueness of preadditive enrichment when zero maps and binary biproducts are fixed.
- Mathlib, Preadditive.Basic: abelian groups of maps and bilinear composition.
- Formal linear combinations and finite sums: free additive constructions and extension of natural transformations.