Coherently shift-compatible functors and transformations form k-linear hom categories

The identity functor $1$ of ${\mathrm{GrMod}}_0(A)$ with ${\theta }_{X,r}:=1_{X\{r\}}:1(X\{r\})=X\{r\}\to X\{r\}=1(X)\{r\}$ is coherently shift-compatible: each ${\theta }_{X,r}$ is a natural degree-zero $A$-linear isomorphism (it is an identity), ${\theta }_{X,0}=1_X$ because $X\{0\}=X$, and $({\theta }_{X,r}\{s\})\circ {\theta }_{X\{r\},s}=1_{X\{r\}\{s\}}=1_{X\{r+s\}}={\theta }_{X,r+s}$ by the strict shift identities.

Given coherent $F$ and $G$, the composite comparison ${\theta }_{X,r}^{GF}:={\theta }_{F(X),r}^G\circ G({\theta }_{X,r}^F)$ is a composite of natural degree-zero isomorphisms and hence a natural degree-zero $C$-linear isomorphism $(GF)(X\{r\})\to (GF)(X)\{r\}$; its unit is ${\theta }_{F(X),0}^G\circ G({\theta }_{X,0}^F)=1\circ G(1)=1$, and its cocycle follows by expanding ${\theta }_{X,r+s}^{GF}={\theta }_{F(X),r+s}^G\circ G({\theta }_{X,r+s}^F)$, rewriting the inner factor with the cocycle of ${\theta }^F$, applying the functor $G$, substituting the naturality of ${\theta }^G$ at the morphism ${\theta }_{X,r}^F$ with parameter $s$, and finally the cocycle of ${\theta }^G$ at $F(X)$; the comparisons are strictly associative and unital, ${\theta }^{(HG)F}={\theta }^{H(GF)}$ and ${\theta }^{1\circ F}={\theta }^F={\theta }^{F\circ 1}$, because both sides are the same composites of ${\theta }^H$, $H({\theta }^G)$ and $H(G({\theta }^F))$ and $H$ preserves composition and identities.

If $\eta :F\Rightarrow G$ and $\nu :G\Rightarrow H$ are coherent, then $\nu \circ \eta$ is natural and ${\theta }_{X,r}^H(\nu \circ \eta {)}_{X\{r\}}={\theta }_{X,r}^H{\nu }_{X\{r\}}{\eta }_{X\{r\}}=({\nu }_X\{r\}){\theta }_{X,r}^G{\eta }_{X\{r\}}=({\nu }_X\{r\})({\eta }_X\{r\}){\theta }_{X,r}^F=((\nu \circ \eta {)}_X\{r\}){\theta }_{X,r}^F$ by the coherence of $\nu$ and $\eta$, so $\nu \circ \eta$ is coherent; the identity transformations are coherent by the condition (i) of the definition.

For coherent $\eta ,{\eta }^{\mathrm{\prime }}:F\Rightarrow G$ and $\lambda \in k$, the pointwise sum $\eta +{\eta }^{\mathrm{\prime }}$ and scalar multiple $\lambda \eta$ are natural transformations, and they satisfy the equivariance square because both sides are additive in the component: ${\theta }_{X,r}^G(\eta +{\eta }^{\mathrm{\prime }}{)}_{X\{r\}}={\theta }_{X,r}^G{\eta }_{X\{r\}}+{\theta }_{X,r}^G{\eta }_{X\{r\}}^{\mathrm{\prime }}=({\eta }_X\{r\}){\theta }_{X,r}^F+({\eta }_X^{\mathrm{\prime }}\{r\}){\theta }_{X,r}^F=((\eta +{\eta }^{\mathrm{\prime }}{)}_X\{r\}){\theta }_{X,r}^F$, and likewise ${\theta }_{X,r}^G(\lambda \eta {)}_{X\{r\}}=\lambda {\theta }_{X,r}^G{\eta }_{X\{r\}}=(\lambda {\eta }_X\{r\}){\theta }_{X,r}^F$; the zero transformation is coherent and $-\eta =(-1)\eta$, so the coherent transformations $F\Rightarrow G$ form a subgroup of all natural transformations closed under the pointwise $k$-action.

Let $F,G$ be $k$-linear, right exact and coproduct preserving, and let $\kappa ,{\kappa }^{\mathrm{\prime }}:F\Rightarrow G$ be coherent with ${\kappa }_{P_X}={\kappa }_{P_X}^{\mathrm{\prime }}$ for every graded module $X$. For each $X$ the cover $q_X:P_X\to X$ of [L3] is an epimorphism, hence $F(q_X)$ and $G(q_X)$ are epimorphisms because right exact functors preserve epimorphisms [L16]; naturality gives ${\kappa }_{X}F(q_X)=G(q_X){\kappa }_{P_X}=G(q_X){\kappa }_{P_X}^{\mathrm{\prime }}={\kappa }_X^{\mathrm{\prime }}F(q_X)$, and cancelling the epimorphism $F(q_X)$ gives ${\kappa }_X={\kappa }_X^{\mathrm{\prime }}$; since $X$ was arbitrary, $\kappa ={\kappa }^{\mathrm{\prime }}$.

If $\kappa ,{\kappa }^{\mathrm{\prime }}:F\Rightarrow G$ agree on every component at a shifted regular module $A\{d\}$, they agree on every $P_X$: writing $P_X={⨁}_{x\in H_X}A\{\mathrm{deg}x\}$ with coordinate inclusions ${\mathrm{ȷ}}_x$ [L3], the modules $F(A\{\mathrm{deg}x\})$ with the maps $F({\mathrm{ȷ}}_x)$ present $F(P_X)$ as a coproduct, so a morphism out of $F(P_X)$ is determined by its composites with all $F({\mathrm{ȷ}}_x)$; naturality of $\kappa ,{\kappa }^{\mathrm{\prime }}$ at ${\mathrm{ȷ}}_x$ gives ${\kappa }_{P_X}F({\mathrm{ȷ}}_x)=G({\mathrm{ȷ}}_x){\kappa }_{A\{\mathrm{deg}x\}}$ and the same with ${\kappa }^{\mathrm{\prime }}$, and the right sides agree, so ${\kappa }_{P_X}={\kappa }_{P_X}^{\mathrm{\prime }}$; with step 1.5, $\kappa ,{\kappa }^{\mathrm{\prime }}$ then agree everywhere.

Vertical composition is associative and unital with the identity transformations of step 1.3 as identities. The pointwise operations of step 1.4 satisfy the vector-space identities componentwise, and vertical composition is $k$-bilinear because composition in ${\mathrm{GrMod}}_0(B)$ is $k$-bilinear. For arbitrary large-source coherent functors these are operations on metatheoretic hom-collections; the set-sized hom-spaces of $\mathrm{C}\mathrm{o}\mathrm{h}\mathrm{F}\mathrm{u}\mathrm{n}$ are established below.

For coherent $\eta :F\Rightarrow F^{\mathrm{\prime }}$ and $\nu :G\Rightarrow G^{\mathrm{\prime }}$ the horizontal composite $\nu \ast \eta$ has components ${\nu }_{F^{\mathrm{\prime }}(X)}\circ G({\eta }_X)$ [L7] and is coherent: substituting the naturality of $\nu$ at the morphism ${\theta }_{X,r}^{F^{\mathrm{\prime }}}$, the coherence of $\eta$ under the functor $G$, the naturality of ${\theta }^G$ at ${\eta }_X$ with parameter $r$, and the coherence of $\nu$ at the object $F^{\mathrm{\prime }}(X)$ turns ${\theta }_{X,r}^{G^{\mathrm{\prime }}{F}^{\mathrm{\prime }}}(\nu \ast \eta {)}_{X\{r\}}$ into $((\nu \ast \eta {)}_X\{r\}){\theta }_{X,r}^{GF}$; horizontal composition preserves identity 2-cells and satisfies the interchange law [L18]. These are componentwise identities for supplied functors, before any category of functor objects is formed.

The identity functor of ${\mathrm{GrMod}}_0(A)$ is $k$-linear and preserves all colimits, hence is right exact and coproduct preserving, and it is coherent by step 1.1; the composite of two $k$-linear right exact coproduct-preserving coherent functors is $k$-linear, right exact and coproduct preserving (each factor preserves the same colimits) and coherent by step 1.2; hence $\mathrm{C}\mathrm{o}\mathrm{h}\mathrm{F}\mathrm{u}\mathrm{n}$ is closed under composition and contains the identity functors.

If ${\kappa }_A={\kappa }_A^{\mathrm{\prime }}$ for coherent $\kappa ,{\kappa }^{\mathrm{\prime }}:F\Rightarrow G$, then for every $d$ the equivariance squares at $A$ give ${\theta }_{A,d}^G{\kappa }_{A\{d\}}=({\kappa }_A\{d\}){\theta }_{A,d}^F=({\kappa }_A^{\mathrm{\prime }}\{d\}){\theta }_{A,d}^F={\theta }_{A,d}^G{\kappa }_{A\{d\}}^{\mathrm{\prime }}$, and ${\theta }_{A,d}^G$ is an isomorphism, so ${\kappa }_{A\{d\}}={\kappa }_{A\{d\}}^{\mathrm{\prime }}$; by step 2.1 the two transformations agree everywhere.

For the family in clause 4, a word $w=(p_1,\dots ,p_n)$ with $B_{p_i}=A_{p_{i+1}}$ represents $F_w=F_{p_n}\cdots F_{p_1}$ with the iterated comparisons of step 1.2. Evaluation of a finite word on any object, morphism or comparison is uniformly definable by a finite sequence of intermediate values. Empty words, tagged with their algebra, represent identities. All words are sets and form a definable class, and concatenation is literally associative and unital; its interpretation is composition of coherent functors by steps 1.1, 1.2 and 2.4. Different words representing the same functor may remain different objects.

To define the transformation codes without quantifying over classes, fix $t\in {\mathrm{Hom}}_B(F(A),G(A))$ and put $t_d=({\theta }_{A,d}^G{)}^{-1}(t\{d\}){\theta }_{A,d}^F$. For each $X$, coproduct preservation defines a unique $t_{P_X}:F(P_X)\to G(P_X)$ by $t_{P_X}F({\mathrm{ȷ}}_x)=G({\mathrm{ȷ}}_x)t_{\mathrm{deg}x}$. Write $d_X:P_{K_X}\to P_X$ for the canonical presentation map. The map $q_X$ is a cokernel of $d_X$: a degree-zero map vanishing on its image $\ker q_X$ factors uniquely along the surjection $q_X$, preserving action and degree. Hence $F(q_X)$ is a cokernel of $F(d_X)$. Whenever $G(q_X)t_{P_X}F(d_X)=0$, there is a unique degree-zero $B$-linear $t_X$ with $t_{X}F(q_X)=G(q_X)t_{P_X}$. Require this vanishing for every $X$, require $t_A=t$, and require the resulting $t_X$ to satisfy naturality for every degree-zero map and the coherence square for every $X,r$. These are first-order conditions on sets, using the fixed defining formulas of $F,G,{\theta }^F,{\theta }^G$; separation therefore gives a set $H(F,G)$ of such $t$. Each code gives a definable coherent transformation. Conversely any supplied coherent transformation with component $t$ has these $t_d,t_{P_X},t_X$ by coherence, coproduct naturality and naturality at $q_X$, so its code lies in $H(F,G)$ and reconstruction recovers it. Evaluation and reconstruction are inverse by step 3.1.

For words $w,v:A\to B$, apply step 4.1 to $F_w,F_v$. Its predicates are uniform in $w,v$ by step 3.2, so triples $(w,v,t)$ with $t\in H(F_w,F_v)$ form a definable class of set morphisms with source $w$ and target $v$. The identity code is $1_{F_w(A)}$; vertical composition is composition of the component codes. Reconstruction identifies these operations with those of steps 1.3 and 2.2, so they satisfy the category laws. Pointwise sums and scalar multiples give $k$-vector spaces $H(F_w,F_v)$, and vertical composition is $k$-bilinear. Thus ${\mathrm{C}\mathrm{o}\mathrm{h}\mathrm{F}\mathrm{u}\mathrm{n}}_J(A,B)$ is an actual locally small $k$-linear category.

On words, horizontal composition is concatenation. On transformation codes it is the component at $A$ of the horizontal composite reconstructed in step 4.1, namely ${\nu }_{F_{w^{\mathrm{\prime }}}(A)}{F}_u({\eta }_A)$ for $\eta :F_w\Rightarrow F_{w^{\mathrm{\prime }}}$ and $\nu :F_u\Rightarrow F_{u^{\mathrm{\prime }}}$. This is uniformly definable and is again a valid code by step 2.3. Interchange makes it a functor on the hom-categories of step 5.1. For three transformations, expanding either horizontal bracketing gives the same components by functoriality of the outer functor and associativity of module-map composition; the empty words and their identity transformations are strict units. The comparison identities are those of step 1.2, and code injectivity turns all componentwise equalities into literal equalities. Thus these hom-categories and operations give the asserted strict 2-category. For any finite list of supplied definable functors, combine their defining formulas by a finite case distinction on labels to obtain a family $J$ containing them. No quantification over arbitrary formulas or proper-class graphs is used, and all reconstruction maps are unique, so no choice or universe axiom is required.