[proofplan]
We make the four canonical maps into $K_1(R[t,t^{-1}])$ explicit: constants give the $K_1(R)$ summand, multiplication by the Laurent variable gives the $K_0(R)$ summand, and the inclusions of the positive and negative polynomial subrings give the two nil summands. The Bass-Heller-Swan fundamental theorem for lower algebraic $K$-theory states that the direct sum of these four maps is an isomorphism. Naturality follows because each map is defined by functorial constructions: extension of scalars, evaluation, polynomial inclusion, and multiplication by $t$.
[/proofplan]
[step:Define the four canonical summand maps]
Let
\begin{align*}
L_R:=R[t,t^{-1}]
\end{align*}
denote the Laurent [polynomial ring](/page/Polynomial%20Ring) in one central variable. Let
\begin{align*}
c_R:R\to L_R
\end{align*}
be the constant-inclusion homomorphism. It induces a homomorphism
\begin{align*}
K_1(c_R):K_1(R)\to K_1(L_R).
\end{align*}
Next define the Bass suspension map
\begin{align*}
\beta_R:K_0(R)\to K_1(L_R)
\end{align*}
as follows. If $P$ is a finitely generated projective left $R$-module, then
\begin{align*}
L_R\otimes_R P
\end{align*}
is a finitely generated projective left $L_R$-module, and multiplication by $t$ defines an $L_R$-linear automorphism
\begin{align*}
m_{t,P}:L_R\otimes_R P\to L_R\otimes_R P.
\end{align*}
The class of this automorphism in $K_1(L_R)$ depends only on the class $[P]\in K_0(R)$ and is additive under direct sums, so it defines
\begin{align*}
\beta_R([P]):=[m_{t,P}]\in K_1(L_R).
\end{align*}
Let
\begin{align*}
\iota_{+,R}:R[t]\to L_R
\end{align*}
be the inclusion determined by $t\mapsto t$, and let
\begin{align*}
\iota_{-,R}:R[u]\to L_R
\end{align*}
be the inclusion determined by $u\mapsto t^{-1}$. Define
\begin{align*}
\operatorname{ev}_{0,+}:R[t]\to R
\end{align*}
by $t\mapsto 0$, and define
\begin{align*}
\operatorname{ev}_{0,-}:R[u]\to R
\end{align*}
by $u\mapsto 0$. The positive nil summand is
\begin{align*}
NK_1^+(R):=\ker K_1(\operatorname{ev}_{0,+}),
\end{align*}
and the negative nil summand is
\begin{align*}
NK_1^-(R):=\ker K_1(\operatorname{ev}_{0,-}).
\end{align*}
Both are canonically identified with $NK_1(R)$ by using $t$ as the polynomial variable in the first case and $u$ as the polynomial variable in the second case. The two nil maps are the restrictions
\begin{align*}
\nu_{+,R}:=K_1(\iota_{+,R})\big|_{NK_1^+(R)}:NK_1(R)\to K_1(L_R)
\end{align*}
and
\begin{align*}
\nu_{-,R}:=K_1(\iota_{-,R})\big|_{NK_1^-(R)}:NK_1(R)\to K_1(L_R).
\end{align*}
[guided]
The decomposition has four summands, so we first name the four maps that will realize them inside $K_1(R[t,t^{-1}])$.
The first map is the most direct one. The constant inclusion
\begin{align*}
c_R:R\to R[t,t^{-1}]
\end{align*}
sends an element of $R$ to the same element regarded as a Laurent polynomial. By functoriality of $K_1$, this gives
\begin{align*}
K_1(c_R):K_1(R)\to K_1(R[t,t^{-1}]).
\end{align*}
The second map is the source of the $K_0(R)$ summand. For every finitely generated projective left $R$-module $P$, extension of scalars gives the finitely generated projective left $R[t,t^{-1}]$-module
\begin{align*}
R[t,t^{-1}]\otimes_R P.
\end{align*}
Because $t$ is invertible in $R[t,t^{-1}]$, multiplication by $t$ defines an automorphism
\begin{align*}
m_{t,P}:R[t,t^{-1}]\otimes_R P\to R[t,t^{-1}]\otimes_R P.
\end{align*}
An automorphism of a finitely generated projective module determines a $K_1$-class, so we set
\begin{align*}
\beta_R([P]):=[m_{t,P}]\in K_1(R[t,t^{-1}]).
\end{align*}
If $P\oplus Q$ is a direct sum, then multiplication by $t$ on
\begin{align*}
R[t,t^{-1}]\otimes_R(P\oplus Q)
\end{align*}
is the direct sum of the automorphisms $m_{t,P}$ and $m_{t,Q}$. Hence the assignment is additive and descends to a homomorphism
\begin{align*}
\beta_R:K_0(R)\to K_1(R[t,t^{-1}]).
\end{align*}
The final two maps come from the two directions in a Laurent polynomial: positive powers of $t$ and negative powers of $t$. The positive polynomial inclusion is
\begin{align*}
\iota_{+,R}:R[t]\to R[t,t^{-1}],
\end{align*}
and the negative polynomial inclusion is
\begin{align*}
\iota_{-,R}:R[u]\to R[t,t^{-1}],
\end{align*}
where $\iota_{-,R}$ sends $u$ to $t^{-1}$. The nil group attached to a polynomial variable is the kernel of evaluation at zero:
\begin{align*}
NK_1(R)=\ker\bigl(K_1(R[t])\to K_1(R)\bigr).
\end{align*}
Using $u$ instead of $t$ gives an identical copy of this group. Restricting the two induced maps on $K_1$ to these kernels gives
\begin{align*}
\nu_{+,R}:NK_1(R)\to K_1(R[t,t^{-1}])
\end{align*}
and
\begin{align*}
\nu_{-,R}:NK_1(R)\to K_1(R[t,t^{-1}]).
\end{align*}
These are the positive and negative nil contributions.
[/guided]
[/step]
[step:Assemble the Bass-Heller-Swan homomorphism]
Define
\begin{align*}
\Phi_R:K_1(R)\oplus K_0(R)\oplus NK_1(R)\oplus NK_1(R)\to K_1(L_R)
\end{align*}
by
\begin{align*}
\Phi_R(x,y,z_+,z_-):=K_1(c_R)(x)+\beta_R(y)+\nu_{+,R}(z_+)+\nu_{-,R}(z_-).
\end{align*}
Here the addition is the abelian group operation on $K_1(L_R)$.
The Bass-Heller-Swan fundamental theorem for lower algebraic $K$-theory states precisely that, for every unital ring $R$, this homomorphism $\Phi_R$ is an isomorphism. Applying that theorem gives
\begin{align*}
K_1(R[t,t^{-1}])\cong K_1(R)\oplus K_0(R)\oplus NK_1(R)\oplus NK_1(R).
\end{align*}
This is the asserted decomposition.
[/step]
[step:Check naturality of the decomposition]
Let
\begin{align*}
\varphi:R\to S
\end{align*}
be a unital ring homomorphism. It induces homomorphisms
\begin{align*}
\varphi[t]:R[t]\to S[t]
\end{align*}
and
\begin{align*}
\varphi[t,t^{-1}]:R[t,t^{-1}]\to S[t,t^{-1}]
\end{align*}
by applying $\varphi$ to coefficients and fixing the central variable. The evaluation maps commute with $\varphi[t]$:
\begin{align*}
\operatorname{ev}_{0,S}\circ \varphi[t]=\varphi\circ \operatorname{ev}_{0,R}.
\end{align*}
Therefore functoriality of $K_1$ sends $\ker K_1(\operatorname{ev}_{0,R})$ into $\ker K_1(\operatorname{ev}_{0,S})$, giving the induced nil map
\begin{align*}
NK_1(\varphi):NK_1(R)\to NK_1(S).
\end{align*}
The constant inclusions, positive polynomial inclusions, negative polynomial inclusions, and multiplication-by-$t$ automorphisms are all compatible with applying $\varphi$ to coefficients. Hence the square
\begin{align*}
K_1(R)\oplus K_0(R)\oplus NK_1(R)\oplus NK_1(R)\to K_1(R[t,t^{-1}])
\end{align*}
commutes with the corresponding square for $S$, where the left vertical map is
\begin{align*}
K_1(\varphi)\oplus K_0(\varphi)\oplus NK_1(\varphi)\oplus NK_1(\varphi)
\end{align*}
and the right vertical map is $K_1(\varphi[t,t^{-1}])$. Thus the isomorphisms $\Phi_R$ are natural in $R$.
[guided]
Naturality means that the decomposition is not a choice made separately for each ring. If
\begin{align*}
\varphi:R\to S
\end{align*}
is a unital ring homomorphism, then the decomposition for $R$ must be carried to the decomposition for $S$ by the maps induced from $\varphi$.
The map $\varphi$ extends coefficientwise to
\begin{align*}
\varphi[t]:R[t]\to S[t]
\end{align*}
and to
\begin{align*}
\varphi[t,t^{-1}]:R[t,t^{-1}]\to S[t,t^{-1}].
\end{align*}
Both extensions fix the polynomial or Laurent variable. Because evaluation at zero only removes the variable and leaves coefficients unchanged, the identity
\begin{align*}
\operatorname{ev}_{0,S}\circ \varphi[t]=\varphi\circ \operatorname{ev}_{0,R}
\end{align*}
holds as an equality of ring homomorphisms $R[t]\to S$. Applying $K_1$ gives a commuting diagram, so an element of
\begin{align*}
NK_1(R)=\ker K_1(\operatorname{ev}_{0,R})
\end{align*}
is sent to an element of
\begin{align*}
NK_1(S)=\ker K_1(\operatorname{ev}_{0,S}).
\end{align*}
This defines the functorial nil map $NK_1(\varphi)$.
Now we compare the four summands. Constants are compatible because
\begin{align*}
\varphi[t,t^{-1}]\circ c_R=c_S\circ \varphi.
\end{align*}
The positive and negative polynomial inclusions are compatible because applying $\varphi$ to coefficients commutes with the inclusions into Laurent polynomials. Finally, the $K_0$ summand is compatible because extension of scalars sends the automorphism given by multiplication by $t$ on
\begin{align*}
R[t,t^{-1}]\otimes_R P
\end{align*}
to the automorphism given by multiplication by $t$ on
\begin{align*}
S[t,t^{-1}]\otimes_S(S\otimes_R P).
\end{align*}
Thus every summand map defining $\Phi_R$ is carried to the corresponding summand map defining $\Phi_S$. This proves the naturality of the Bass-Heller-Swan isomorphism.
[/guided]
[/step]
