[proofplan]
We compute $K_0(\mathcal A)$ by measuring each object through its Jordan-Hölder composition factors. First, a composition series and the defining additivity relation in $K_0(\mathcal A)$ express $[M]$ as the sum of the classes of the simple subquotients. Jordan-Hölder makes the resulting multiplicities well-defined, and concatenation of filtrations in a short exact sequence proves that the multiplicity functions are additive. These additive functions give a homomorphism from $K_0(\mathcal A)$ to the free abelian group on the simple classes, and the inverse sends the basis element corresponding to $S_\lambda$ to the class of $S_\lambda$.
[/proofplan]
[step:Define the composition-factor coordinate map]
Let
\begin{align*}
F := \bigoplus_{\lambda \in \Lambda} \mathbb Z e_\lambda
\end{align*}
be the free abelian group with basis symbols $e_\lambda$ indexed by $\Lambda$. These symbols are temporarily distinct from the classes $[S_\lambda] \in K_0(\mathcal A)$.
Since $\mathcal A$ is a length category, every object $M$ of $\mathcal A$ admits a finite composition series. For each $\lambda \in \Lambda$, define $m_\lambda(M) \in \mathbb Z_{\ge 0}$ to be the number of composition factors isomorphic to $S_\lambda$ in any composition series of $M$. By the Jordan-Hölder theorem, this number is independent of the chosen composition series. Since a composition series is finite, only finitely many values $m_\lambda(M)$ are nonzero. Let $\operatorname{Ob}(\mathcal A)$ denote the class of objects of $\mathcal A$. Define the composition-factor coordinate map
\begin{align*}
c:\operatorname{Ob}(\mathcal A) \longrightarrow F
\end{align*}
by
\begin{align*}
c(M) := \sum_{\lambda \in \Lambda} m_\lambda(M)e_\lambda.
\end{align*}
The finite-support observation shows that $c(M)$ is an element of $F$ for every object $M$ of $\mathcal A$.
[/step]
[step:Prove that composition-factor multiplicities are additive on short exact sequences]
Let
\begin{align*}
0 \longrightarrow M' \xrightarrow{i} M \xrightarrow{p} M'' \longrightarrow 0
\end{align*}
be a short exact sequence in $\mathcal A$. We prove that
\begin{align*}
c(M) = c(M') + c(M'').
\end{align*}
Choose a composition series of $M'$,
\begin{align*}
0 = M'_0 \subset M'_1 \subset \cdots \subset M'_a = M',
\end{align*}
and a composition series of $M''$,
\begin{align*}
0 = N_0 \subset N_1 \subset \cdots \subset N_b = M''.
\end{align*}
Using the monomorphism $i$, regard each $M'_r$ as a subobject of $M$. For $1 \le j \le b$, define $L_j := p^{-1}(N_j)$, a subobject of $M$. Also define $L_0 := p^{-1}(N_0)$. Since $N_0=0$ and the sequence is exact, $L_0=\ker p=\operatorname{im} i=M'$.
Thus the two filtrations concatenate to give
\begin{align*}
0 = M'_0 \subset M'_1 \subset \cdots \subset M'_a = L_0 \subset L_1 \subset \cdots \subset L_b = M.
\end{align*}
For $1 \le r \le a$, the quotient $M'_r/M'_{r-1}$ is a simple composition factor of $M'$. For $1 \le j \le b$, the map $p:L_j \to N_j$ induces an isomorphism
\begin{align*}
L_j/L_{j-1} \cong N_j/N_{j-1},
\end{align*}
by the isomorphism theorem, because $L_{j-1}=p^{-1}(N_{j-1})$. Hence the concatenated filtration is a composition series of $M$ whose simple factors are exactly the factors of the chosen series for $M'$ together with the factors of the chosen series for $M''$.
Therefore, for every $\lambda \in \Lambda$,
\begin{align*}
m_\lambda(M) = m_\lambda(M') + m_\lambda(M'').
\end{align*}
Multiplying by $e_\lambda$ and summing over the finite support gives
\begin{align*}
c(M) = c(M') + c(M'').
\end{align*}
[guided]
The point of this step is to show that the composition-factor count is compatible with the defining relation of $K_0(\mathcal A)$. We start with a short exact sequence
\begin{align*}
0 \longrightarrow M' \xrightarrow{i} M \xrightarrow{p} M'' \longrightarrow 0.
\end{align*}
The exactness means that $i$ identifies $M'$ with the kernel of $p$, and that $p$ maps $M$ onto $M''$.
Choose a composition series of the subobject $M'$:
\begin{align*}
0 = M'_0 \subset M'_1 \subset \cdots \subset M'_a = M',
\end{align*}
and choose a composition series of the quotient $M''$:
\begin{align*}
0 = N_0 \subset N_1 \subset \cdots \subset N_b = M''.
\end{align*}
We want to turn these two series into a single composition series for $M$. The first part already lives inside $M$, after identifying $M'$ with its image under $i$. For the second part, each subobject $N_j \subset M''$ has a preimage under $p$. Define
\begin{align*}
L_j := p^{-1}(N_j)
\end{align*}
for $0 \le j \le b$. Since $N_0=0$, exactness gives
\begin{align*}
L_0 = p^{-1}(0) = \ker p = \operatorname{im} i = M'.
\end{align*}
Since $N_b=M''$ and $p$ is surjective, $L_b=M$.
Thus we obtain a filtration of $M$:
\begin{align*}
0 = M'_0 \subset M'_1 \subset \cdots \subset M'_a = L_0 \subset L_1 \subset \cdots \subset L_b = M.
\end{align*}
The quotients in the first part are precisely the quotients $M'_r/M'_{r-1}$ from the chosen composition series of $M'$, so they are simple. For the second part, the map $p:L_j \to N_j$ has preimage $L_{j-1}$ of $N_{j-1}$. The isomorphism theorem gives
\begin{align*}
L_j/L_{j-1} \cong N_j/N_{j-1}.
\end{align*}
Because $N_j/N_{j-1}$ is simple, each quotient $L_j/L_{j-1}$ is also simple.
So the concatenated filtration is a composition series of $M$. Its factors are exactly the factors of the chosen series of $M'$ followed by the factors of the chosen series of $M''$. Therefore the number of factors isomorphic to $S_\lambda$ satisfies
\begin{align*}
m_\lambda(M) = m_\lambda(M') + m_\lambda(M'')
\end{align*}
for every $\lambda \in \Lambda$. Since only finitely many multiplicities are nonzero for each object, summing these equalities in the free abelian group $F$ gives
\begin{align*}
c(M) = c(M') + c(M'').
\end{align*}
[/guided]
[/step]
[step:Construct the homomorphism from $K_0(\mathcal A)$ to the free group on simple objects]
The Grothendieck group $K_0(\mathcal A)$ is generated by symbols $[M]$ for objects $M$ of $\mathcal A$, subject to the relations
\begin{align*}
[M] = [M'] + [M'']
\end{align*}
for every short exact sequence
\begin{align*}
0 \longrightarrow M' \longrightarrow M \longrightarrow M'' \longrightarrow 0.
\end{align*}
The additivity proved above shows that the assignment $[M] \mapsto c(M)$ respects all these defining relations. Therefore it induces a [group homomorphism](/page/Group%20Homomorphism)
\begin{align*}
\alpha:K_0(\mathcal A) \longrightarrow F
\end{align*}
defined by
\begin{align*}
\alpha([M]) = \sum_{\lambda \in \Lambda} m_\lambda(M)e_\lambda
\end{align*}
for every object $M$ of $\mathcal A$.
[/step]
[step:Construct the reverse homomorphism by sending each simple basis element to its $K_0$ class]
Define a group homomorphism
\begin{align*}
\beta:F \longrightarrow K_0(\mathcal A)
\end{align*}
on the basis of $F$ by
\begin{align*}
\beta(e_\lambda) := [S_\lambda].
\end{align*}
This uniquely determines $\beta$, because $F$ is the free abelian group on the basis $\{e_\lambda\}_{\lambda \in \Lambda}$.
[/step]
[step:Check that the two homomorphisms are inverse]
For $\mu \in \Lambda$, the object $S_\mu$ is simple, so its only composition factor is itself. Hence
\begin{align*}
m_\mu(S_\mu) = 1.
\end{align*}
For every $\lambda \in \Lambda$ with $\lambda \ne \mu$, the representatives $S_\lambda$ and $S_\mu$ are not isomorphic, so
\begin{align*}
m_\lambda(S_\mu) = 0.
\end{align*}
Therefore
\begin{align*}
(\alpha \circ \beta)(e_\mu) = \alpha([S_\mu]) = e_\mu.
\end{align*}
Since the elements $e_\mu$ form a basis of $F$, this proves
\begin{align*}
\alpha \circ \beta = \operatorname{id}_F.
\end{align*}
It remains to prove that $\beta \circ \alpha=\operatorname{id}_{K_0(\mathcal A)}$. Let $M$ be an object of $\mathcal A$, and choose a composition series
\begin{align*}
0 = M_0 \subset M_1 \subset \cdots \subset M_n = M.
\end{align*}
For each $1 \le r \le n$, define the simple quotient
\begin{align*}
Q_r := M_r/M_{r-1}.
\end{align*}
The short exact sequence
\begin{align*}
0 \longrightarrow M_{r-1} \longrightarrow M_r \longrightarrow Q_r \longrightarrow 0
\end{align*}
gives the relation
\begin{align*}
[M_r] = [M_{r-1}] + [Q_r]
\end{align*}
in $K_0(\mathcal A)$. Inducting on $r$ yields
\begin{align*}
[M] = \sum_{r=1}^{n} [Q_r].
\end{align*}
Grouping the simple quotients $Q_r$ by their isomorphism classes gives
\begin{align*}
[M] = \sum_{\lambda \in \Lambda} m_\lambda(M)[S_\lambda].
\end{align*}
Thus
\begin{align*}
(\beta \circ \alpha)([M]) = \beta\left(\sum_{\lambda \in \Lambda} m_\lambda(M)e_\lambda\right) = \sum_{\lambda \in \Lambda} m_\lambda(M)[S_\lambda] = [M].
\end{align*}
The classes $[M]$ generate $K_0(\mathcal A)$, so
\begin{align*}
\beta \circ \alpha = \operatorname{id}_{K_0(\mathcal A)}.
\end{align*}
Hence $\alpha$ and $\beta$ are inverse isomorphisms. Under this isomorphism, the basis symbol $e_\lambda$ corresponds to the class $[S_\lambda]$, and every object $M$ satisfies
\begin{align*}
[M] = \sum_{\lambda \in \Lambda} m_\lambda(M)[S_\lambda].
\end{align*}
This is the desired Jordan-Hölder computation of $K_0(\mathcal A)$.
[/step]
