The triangulated K_0 of the Khovanov–Seidel projective category

The coded projective category is small and represents $C_m$. For each finite list $\mathbf{r}=(r_1,\dots ,r_s)$ the graded submodules $N\subseteq F_{\mathbf{r}}={⨁}_j{A}_m\{r_j\}$ form a set, and the lists themselves form a set; hence the pairs $(\mathbf{r},N)$ used in ${\mathcal{M}}_m^{\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}}$ form a set. For each pair of codes the degree-zero maps between the represented quotient modules form a set of functions, so [L4] makes ${\mathcal{M}}_m^{\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}}$ small. By finite generation in [L2], every module in $A_m\text{-mod}$ is isomorphic to a quotient represented by a code. A bounded complex has only finitely many nonzero terms, so choosing a code and an isomorphism for each such term and transporting its differentials gives an isomorphic code complex; these choices are finite for each complex, and no simultaneous choice over all complexes is made. If its terms are projective, the corresponding code terms are projective because they are isomorphic to them. The code complexes with projective terms and their chain-homotopy classes form a small category: there is a set of finite-support sequences of codes, a set of differentials between their represented modules, and a set of chain maps and homotopies. It is closed under shifts and cones, since finite direct sums are represented by concatenating presentations and a direct sum of finite projectives is projective. Thus it has a set of isomorphism types, and the realization functor is full and faithful and represents every object of $C_m$. Finally, each distinguished triangle of $C_m$ is isomorphic to a cone triangle by [L1]; code its first two objects, transport the first map, and form its cone with the coded direct-sum terms. Therefore every triangle type is represented in the small coded category as well.

$K_0(C_m)$ is a well-defined abelian group. By step 1.1 the index set ${\mathrm{Iso}}_{\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}}(C_m)$ is a set, so the free abelian group ${\mathbb{Z}}^{({\mathrm{Iso}}_{\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}}(C_m))}$ of [L3] is defined. Distinguished triangles in the small coded category form a set of diagrams, so their relation elements form a set; [L3] therefore gives the subgroup $R$ and quotient group $K_0(C_m)=F\mathrm{/}R$. For any object $X\in C_m$, its represented type $\tau (X)$ is unique: if two coded complexes realize objects isomorphic to $X$, the composite of those isomorphisms is an isomorphism in the coded category because its realization is full and faithful. Thus $[X]=e_{\tau (X)}+R$ is independent of the code used.

Code types and choice. The generators use the isomorphism types in the small coded category, not a skeleton of the large class of all complexes. For a fixed $X$, the existence of a code complex isomorphism is established by finitely many presentations, and uniqueness of its type follows from step 2.1; no choice function over all objects is needed. Hence the construction uses neither the Axiom of Choice nor dependent choice.

The relations are genuine triangle relations. By [L1] the category $C_m$ carries the triangulated structure inherited from $K(A_m\text{-mod})$. Step 1.1 shows that every one of its distinguished triangles is isomorphic to a cone triangle in the coded category; the relations defining $R$ therefore include exactly the usual relation $[Y]-[X]-[Z]$ for every triangle type of $C_m$. The shift $[1]$ in these triangles is the homological shift of $C_m$ of [L1], never the internal shift.

Isomorphic objects have equal classes, and $[0]=0$. Let $f:X\to Y$ be an isomorphism of $C_m$. The triangle $X\stackrel{f}{\to }Y\to 0\to X[1]$ is isomorphic to the distinguished triangle $X\stackrel{1_X}{\to }X\to 0\to X[1]$ of [L5] via the identity on the third and fourth vertices and $f$ on the first two, so it is distinguished by the first axiom of [L5]; its relation reads $[Y]=[X]+[0]$, while the triangle $X\stackrel{1_X}{\to }X\to 0\to X[1]$ itself gives $[X]=[X]+[0]$ and hence $[0]=0$ in $K_0(C_m)$. Therefore $[X]=[Y]$ for isomorphic $X$ and $Y$, as the notation $[X]$ for an isomorphism class requires, and no relation depends on a choice of representative.

Direct sums add. By [L5] the canonical biproduct triangle $X\to X\oplus Y\to Y\to X[1]$ is distinguished whenever $X\oplus Y$ exists in $C_m$, which it does since $C_m$ is an additive full subcategory closed under finite direct sums of complexes of finite graded projective modules; its relation in $F$ is $[X\oplus Y]=[X]+[Y]$ in $K_0(C_m)$, so the group operation of $K_0(C_m)$ is compatible with finite direct sums.

Conclusion. The set ${\mathrm{Iso}}_{\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}}(C_m)$ is supplied by step 1.1, so $F={\mathbb{Z}}^{({\mathrm{Iso}}_{\mathrm{c}\mathrm{o}\mathrm{d}\mathrm{e}}(C_m))}$ and the subgroup $R$ generated by the distinguished-triangle relations are well defined and $K_0(C_m)=F\mathrm{/}R$ is an abelian group by step 2.1; the relations represent every triangle type of $C_m$ by step 3.2; isomorphic objects define the same class and $[0]=0$ by step 4.1 while $[X\oplus Y]=[X]+[Y]$ by step 4.2; and the construction needs neither a skeleton nor any choice principle by step 3.1. All sums in $F$ are finite sums of basis elements, and the relations cover every distinguished triangle type of $C_m$.