[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*}[/step]

[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: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$.[/step]

[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]