Explicit description of boundary map in algebraic K-theory Recall that for a DVR A with fraction field F and residue field k, there is a "localization" fiber sequence in algebraic K-theory,
$$K(k) \rightarrow K(A) \rightarrow K(F).$$
In Remark 5.17 of his "Higher Algebraic K-theory: I" paper, Quillen gives an explicit description of the corresponding boundary map $\partial:\Omega K(F) \rightarrow K(k)$, saying the proof will be in a later paper.  My question is, has a proof appeared in the literature?  I'd also be happy with proofs in the literature of any similar descriptions, e.g. involving the S-dot construction.
Thank you for reading!
 A: Apparently there is no proof in the literature.  Let me provide a proof here, in case it's helpful.  Actually, first let's give the set-up, then a precise statement, then the proof.  To tell the truth, the set-up takes the most time.  So this fact is harder to state than to prove, which may be why it's not so useful in practice.  But I think it does give valuable intuition for the boundary map.
The set-up: for a noetherian commutative ring R, let $mod_R$ denote its abelian category of finitely-generated modules.  Then for a DVR $A$ with residue field $k=A/\mathfrak{m}$ and fraction field F, the composite
$$mod_k \hookrightarrow mod_A \rightarrow mod_F$$
has a canonical trivialization ($0\simeq M\otimes_A F$ whenever $\mathfrak{m}\cdot M=0$), and Quillen's devissage and localization theorems combine to show that the induced map on classifying space of Q-constructions
$$|Q(mod_k)|\rightarrow |Q(mod_A)| \rightarrow |Q(mod_F)|$$
is a fiber sequence (of pointed spaces -- or of spectra after group-completing w.r.t. $\oplus$).  The goal is to describe the "boundary", or "monodromy" map
$$\partial: \Omega |Q(mod_F)|\rightarrow |Q(mod_k)|$$
associated to this fibration.
The description will use a different model for the left-hand side $\Omega |Q(mod_F)|$.  Namely, let $\mathcal{C}$ denote the following symmetric monoidal category:


*

*Objects of $\mathcal{C}$ are tuples $(L_0,L_1,V)$ where $V$ is a finite-dimensional $F$-vector space and $L_0,L_1$ are spanning f.g. $A$-submodules of $V$ such that $ L_0\subset L_1$ and $\mathfrak{m}\cdot L_1 \subset L_0$.

*Morphisms in $\mathcal{C}$ from $(L_0,L_1,V)$ to $(L_0',L_1',V')$ are isomorphisms $\alpha:V\simeq V'$ such that $\alpha(L_0)\supset L_0'$ and $\alpha(L_1)\subset L_1'$ (so $\alpha$ realizes $L_1/L_0$ as a subquotient of $L_1'/L_0'$).

*The symmetric monoidal structure is $\oplus$.
Now consider the composition
$$|\mathcal{C}|\rightarrow |(mod_F)^{\simeq}|\rightarrow \Omega |Q(mod_F)|.$$
(By $(-)^{\simeq}$ we mean underlying groupoid.)  Here the first map is induced by the forgetful functor $\mathcal{C}\rightarrow (mod_F)^{\simeq}$, and the second map is the usual inclusion of objects of an exact category as loops in the Q-construction.  Then on the one hand it is easy to check that the first map is an equivalence (fixing $V$, the space of choices for $L_0$ is contractible because it filters down to zero; and fixing $V$ and $L_0$, the space of choices for $L_1$ is contractible because it has a maximal element $\mathfrak{m}\cdot L_0$); but on the other hand by the comparison of the group-completion and Q-construction approaches to K-theory (see Algebraic K-theory: II) the second map is a group-completion.  Thus the composition is a group-completion, so one way to produce maps $\Omega |Q(mod_F)|\rightarrow |Q(mod_k)|$ (such as our desired $\partial$) is to produce a symmetric monoidal functor $\mathcal{C}\rightarrow Q(mod_k)$, then apply geometric realization and group-complete.
This leads us to the precise statement: let $f:\mathcal{C}\rightarrow Q(mod_k)$ denote the symmetric monoidal functor
$$f(L_0,L_1,V) = L_1/L_0.$$
Then the group-completion of $|f|$, identified via the above with a map $\Omega |Q(mod_F)|\rightarrow |Q(mod_k)|$, gives the boundary map in the localization sequence.
Now for the proof.  We will use the following characterization of boundary maps in general.  Given a fiber sequence $F\rightarrow E\rightarrow B$ and a map $f:\Omega B\rightarrow F$, to give a homotopy from $f$ to the boundary map is equivalent to giving a nullhomotopy of the composite $\Omega B\overset{f}{\longrightarrow} F\rightarrow E$, plus a homotopy between $id_{\Omega B}$ and the map $\Omega B\rightarrow \Omega B$ gotten by combining the two different nullhomotopies of the composition $\Omega B\overset{f}{\longrightarrow} F\rightarrow E\rightarrow B$. (I'm being careless with signs.)
So let us provide this data in our case.  The whole time we will be considering maps of spectra out of the group completion of $|\mathcal{C}|$, so we can and will specify all our data just at the level of $\mathcal{C}$.  There are two pieces of data:


*

*We need a nullhomotopy of the composite $\mathcal{C}\overset{f}{\longrightarrow} Q(mod_k)\rightarrow Q(mod_A)$ after geometric realization.  This is provided by a composite of two natural transformations, one of which goes the wrong way.  The first is the obvious identification of $L_1/L_0$ with a subquotient of $L_1$; the second is the obvious identification of $0$ with a subquotient of $L_1$.

*We need a homotopy of the resulting map $|\mathcal{C}|\rightarrow \Omega |Q(mod_F)|$ (gotten by combining the nullhomotopy of 1. with the nullhomotopy provided by our fiber sequence) with the canonical map considered above.  This is clear: when we tensor the null-homotopy of 1. with $F$ over $A$ and use $0\simeq (L_1/L_0)\otimes_A F$ and $L_1\otimes_A F\simeq V$, we see exactly the usual way of mapping $|(mod_F)^\simeq|$ to $\Omega |Q(mod_F)|$, the one used to compare group-completion to Q-construction.
That gives the proof.
