When all exact sequences split in $C$, we have $\Omega B C \simeq K(C):=\Omega Q(C)$. Heuristically, this is because the space of upper-triangular matrices is contractible. Can this be made precise? I don't quite see how the standard proof comes down to this idea.

Let me elaborate. Let $C$ be a Quillen exact category. We may perform two constructions:

• On the one hand, $C$, and hence also the groupoid $\iota C$ of isomorphisms in $C$, is symmetric monoidal under $\oplus$. We may deloop $\iota C$ with respect to obtain $BC$, and then the "symmetric monoidal K-theory" of $C$ is $\Omega B C$.

• On the other hand, we may take the $Q$ construction or the $S_\bullet$ construction of $C$, and the "exact sequences K-theory" of $C$ is $K(C) = \Omega QC$ or $K(C) = \Omega S_\bullet C$.

The theorem (found in Grayson, Higher Algebraic K-Theory II) is that when every exact sequence splits, these two constructions are equivalent: $\Omega BC \simeq \Omega Q C$.

It seems to me the idea of the comparison should be as follows. In the bar construction $BC$, an $n$-simplex consists of an object $c \in C$ equipped with a decomposition as the direct sum of $n$ objects $c = c_{0,1} \oplus c_{1,2} \dots \oplus c_{n-1,n}$. Whereas in $S_\bullet C$, an $n$-simplex consists of an object $c \in C$ equipped with the structure of an $n$-step filtration in $C$ $c_{0,1} \hookrightarrow c_{0,2} \dots \hookrightarrow c_{0,n} = c$ (the indices here are chosen to agree with the $S_\bullet$ construction). In fact, there's a natural map $S_\bullet C \to B C$ sending a filtration to its associated graded. The point should be that the fiber of this map is contractible when every exact sequence splits. Assuming exact sequences split, the fiber over a given "associated graded" is connected, and its automorphisms are automorphisms maps $c \to c$ which are "upper triangular" (with $1$'s on the diagonal) with respect to the direct sum decomposition. Hence the heuristic.

Question:

This heuristic argument seems compelling to me, but again, I don't quite see how to read Grayson's proof as a formalization of this line of thinking. Is there somewhere where this heuristic argument is made precise?

(Note: it may appear from the structure of the paper that Grayson's argument relies on a homology computation and comparison to the plus construction, but this is not the case -- the comparison to the plus construction separates out cleanly in the logic of the paper, and the comparison I'm talking about is in fact reasonably direct, just not quite as conceptually clear as I would dream it could be.)