Simple classes freely generate the Grothendieck group of a length category

Since $\mathcal{C}$ is essentially small, $\mathrm{Iso}(\mathcal{C})$ is a set by [F1]. Simplicity is invariant under isomorphism, so $\mathrm{Simp}(\mathcal{C})\subseteq \mathrm{Iso}(\mathcal{C})$ is a set. Put $F:=\mathbb{Z}[\mathrm{Simp}(\mathcal{C})]$. The universal property of the free abelian group defines $\mathrm{\Phi }:F\to G_0(\mathcal{C})$ by $e_{[S]}\mapsto [S]$.

For $M\in \mathcal{C}$, choose a composition series $0=M_0<M_1<\cdots <M_n=M$. Define $[M:S]$ to be the number of indices $i$ for which $M_i\mathrm{/}{M}_{i-1}\cong S$. By [F4], this number is independent of the chosen series and of the representative of $[M]$. Only finitely many factors occur, so $\mu ([M]):={\sum }_{[S]\in \mathrm{Simp}(\mathcal{C})}[M:S]e_{[S]}$ is a well-defined finite-support element of $F$. Since this value is unique, no composition series is selected simultaneously for all isomorphism classes.

The class function $[M]\mapsto \mu ([M])$ is additive on short exact sequences. Indeed, take $0\to X\stackrel{i}{\to }Y\stackrel{p}{\to }Z\to 0$ and composition series $0=X_0<\cdots <X_r=X$ and $0=Z_0<\cdots <Z_s=Z$. Regard the first series as a series in $Y$ through the kernel isomorphism $i:X\cong \ker p$. For each $j$, let $Y_j$ be the inverse-image subobject of $Z_j$ under $p$, formed by the pullback of $p$ along $Z_j\hookrightarrow Z$. Then $Y_0=i(X)$ and $Y_s=Y$. The projection $Y_j\to Z_j$ is epic by [F7]; composing it with the quotient epimorphism $Z_j\to Z_j\mathrm{/}{Z}_{j-1}$ gives an epimorphism with kernel $Y_{j-1}$. The kernel assertion follows from the pullback universal property [F6]: a map into $Y_j$ is killed by the composite precisely when its $Z_j$-component factors through $Z_{j-1}$, which is precisely the defining property of $Y_{j-1}$. By [F8] this composite is a cokernel of $Y_{j-1}\hookrightarrow Y_j$, and by [F9] it therefore identifies $Y_j\mathrm{/}{Y}_{j-1}\cong Z_j\mathrm{/}{Z}_{j-1}$. These quotients are simple. Thus the chain $0=i(X_0)<\cdots <i(X_r)=Y_0<Y_1<\cdots <Y_s=Y$ is a composition series of $Y$, with the factors of the chosen $X$-series followed by those of the chosen $Z$-series.

The spliced series in step 1.3 has, for each simple $S$, exactly $[X:S]+[Z:S]$ factors isomorphic to $S$. Jordan-Hölder [F4] identifies these counts with the counts from any composition series of $Y$. Therefore $[Y:S]=[X:S]+[Z:S]$ for every simple $S$, so $\mu ([Y])=\mu ([X])+\mu ([Z])$. If $X=0$ or $Z=0$, the corresponding series is empty and the same argument gives the endpoint identity. Only two finite composition series are chosen for this one sequence; no arbitrary-index choice is used.

By steps 1.2 and 2.1, $\mu$ is an additive class function on $\mathrm{Iso}(\mathcal{C})$. The universal property [F10] gives a unique homomorphism $\bar{\mu }:G_0(\mathcal{C})\to F$ with $\bar{\mu }([M])=\mu ([M])$.

If $S$ is simple, then $0<S$ is a composition series with sole factor $S$ by [F5]. Hence $\bar{\mu }\mathrm{\Phi }(e_{[S]})=e_{[S]}$ for every basis vector, so $\bar{\mu }\mathrm{\Phi }=1_F$.

For a composition series $0=M_0<\cdots <M_n=M$, each short exact sequence $0\to M_{i-1}\to M_i\to M_i\mathrm{/}{M}_{i-1}\to 0$ gives $[M_i]=[M_{i-1}]+[M_i\mathrm{/}{M}_{i-1}]$ in $G_0(\mathcal{C})$ by [F1]. Since $[M_0]=[0]=0$, telescoping gives $[M]={\sum }_{i=1}^n[M_i\mathrm{/}{M}_{i-1}]=\mathrm{\Phi }\bar{\mu }([M])$. The classes $[M]$ generate $G_0(\mathcal{C})$, so $\mathrm{\Phi }\bar{\mu }=1_{G_0(\mathcal{C})}$.

Steps 4.1 and 4.2 show that $\mathrm{\Phi }$ and $\bar{\mu }$ are inverse isomorphisms. If $\mathrm{Simp}(\mathcal{C})$ is empty, every nonzero object would have a nonempty composition series with a simple first factor; thus every object is zero up to isomorphism, $F=0$, and the same inverse identities give $G_0(\mathcal{C})=0$. For $M=0$, the empty composition series gives $\mu ([0])=0$, consistent with $[0]=0$ from [F1]. The theorem is not an iff statement.