[proofplan] We use the projective-line form of Bass's fundamental theorem for algebraic $K$-theory, whose degree-one boundary computation gives the Laurent extension as the sum of the constant part, the Bott class coming from the Laurent unit $t$, and the two nil terms from the two affine charts. The statement has now fixed the four maps in the decomposition: constant Laurent polynomials, multiplication by $t$ on extended projectives, and the positive and negative polynomial inclusions. The projective-line theorem asserts that this specified map is an isomorphism, and its functoriality gives naturality in the ring $R$. [/proofplan]

[step:Define the nil summands from the two polynomial directions] Let \begin{align*} \operatorname{ev}_0^+:R[t]\to R \end{align*} be the unital ring homomorphism determined by $\operatorname{ev}_0^+(t)=0$ and $\operatorname{ev}_0^+(r)=r$ for $r\in R$. Define \begin{align*} NK_1^+(R):=\ker\bigl(K_1(\operatorname{ev}_0^+):K_1(R[t])\to K_1(R)\bigr). \end{align*} By the convention in the statement, $NK_1^+(R)=NK_1(R)$. Let $s$ be an independent polynomial variable, and let \begin{align*} \operatorname{ev}_0^-:R[s]\to R \end{align*} be the unital ring homomorphism determined by $\operatorname{ev}_0^-(s)=0$ and $\operatorname{ev}_0^-(r)=r$ for $r\in R$. Define \begin{align*} NK_1^-(R):=\ker\bigl(K_1(\operatorname{ev}_0^-):K_1(R[s])\to K_1(R)\bigr). \end{align*} The assignment $s\mapsto t^{-1}$ identifies the second polynomial direction with the negative Laurent direction, and after replacing $s$ by a standard polynomial variable, $NK_1^-(R)$ is another copy of $NK_1(R)$. [/step]

[step:Describe the four standard maps into $K_1(R[t,t^{-1}])$] Let \begin{align*} i:R\to R[t,t^{-1}] \end{align*} be the constant Laurent polynomial inclusion. It induces a [group homomorphism](/page/Group%20Homomorphism) \begin{align*} K_1(i):K_1(R)\to K_1(R[t,t^{-1}]). \end{align*} Next define the Bass suspension map \begin{align*} \beta_R:K_0(R)\to K_1(R[t,t^{-1}]) \end{align*} as follows. We use the standard automorphism model for $K_1$: an automorphism of a finitely generated projective module over a unital ring determines a class in $K_1$ of that ring, and direct sum of automorphisms corresponds to addition in $K_1$. If $P$ is a finitely generated projective left $R$-module, let \begin{align*} P[t,t^{-1}]:=R[t,t^{-1}]\otimes_R P. \end{align*} This is a finitely generated projective left $R[t,t^{-1}]$-module. Let \begin{align*} \tau_P:P[t,t^{-1}]\to P[t,t^{-1}] \end{align*} be the $R[t,t^{-1}]$-linear automorphism defined by multiplication by $t$ on the Laurent polynomial factor. The element $\beta_R([P])$ is the class of this automorphism in $K_1(R[t,t^{-1}])$. The additivity of automorphism classes under direct sum makes this assignment compatible with the defining direct-sum relation in $K_0(R)$: if $P$, $Q$, and $P\oplus Q$ are finitely generated projective left $R$-modules, then the automorphism $\tau_{P\oplus Q}$ identifies with $\tau_P\oplus\tau_Q$ under the natural isomorphism \begin{align*} (P\oplus Q)[t,t^{-1}]\cong P[t,t^{-1}]\oplus Q[t,t^{-1}]. \end{align*} Thus the relation $[P\oplus Q]=[P]+[Q]$ in $K_0(R)$, equivalently the additivity relation for finitely generated projectives [citetheorem:8641], is sent to addition in $K_1(R[t,t^{-1}])$. Hence the assignment descends to a group homomorphism on $K_0(R)$. Finally let \begin{align*} j_+:R[t]\to R[t,t^{-1}] \end{align*} be the localization homomorphism sending $t$ to $t$, and let \begin{align*} j_-:R[s]\to R[t,t^{-1}] \end{align*} be the homomorphism sending $s$ to $t^{-1}$. These induce homomorphisms \begin{align*} K_1(j_+)|_{NK_1^+(R)}:NK_1^+(R)\to K_1(R[t,t^{-1}]) \end{align*} and \begin{align*} K_1(j_-)|_{NK_1^-(R)}:NK_1^-(R)\to K_1(R[t,t^{-1}]). \end{align*} [/step]

[step:Apply the projective-line form of Bass's fundamental theorem]We use the projective-line form of Bass's fundamental theorem for Quillen algebraic $K$-theory in low degrees as the external input. In degree $1$, this theorem states the following precise result. For every unital ring $A$, let $A[t]$ and $A[s]$ be the two affine polynomial rings, let $A[t,t^{-1}]$ be their common Laurent localization under the identification $s=t^{-1}$, and let \begin{align*} N^+K_1(A):=\ker\bigl(K_1(A[t])\xrightarrow{K_1(\operatorname{ev}_{0,t})}K_1(A)\bigr) \end{align*} and \begin{align*} N^-K_1(A):=\ker\bigl(K_1(A[s])\xrightarrow{K_1(\operatorname{ev}_{0,s})}K_1(A)\bigr), \end{align*} where $\operatorname{ev}_{0,t}:A[t]\to A$ and $\operatorname{ev}_{0,s}:A[s]\to A$ are evaluation at the corresponding variable $0$. The theorem asserts that the direct sum of the four standard maps coming from the constant inclusion, the Bass suspension class of the Laurent unit, the inclusion $A[t]\to A[t,t^{-1}]$, and the inclusion $A[s]\to A[t,t^{-1}]$ is an isomorphism \begin{align*} K_1(A)\oplus K_0(A)\oplus N^+K_1(A)\oplus N^-K_1(A)\xrightarrow{\cong}K_1(A[t,t^{-1}]). \end{align*} This is the non-circular external input: it is the localization theorem for the projective line with the two affine charts, including its boundary computation in degree $1$, not merely the present displayed decomposition restated as a theorem. Apply this theorem with $A=R$. Its hypotheses are satisfied because $R$ is a unital ring, $R[t]$ and $R[s]$ are unital polynomial extensions, $R[t,t^{-1}]$ is the corresponding Laurent localization, and $NK_1^+(R)$ and $NK_1^-(R)$ are exactly the two evaluation kernels required in the theorem. Therefore the homomorphism \begin{align*} \Phi_R:K_1(R)\oplus K_0(R)\oplus NK_1^+(R)\oplus NK_1^-(R)\to K_1(R[t,t^{-1}]) \end{align*} defined by \begin{align*} \Phi_R(x,y,u,v)=K_1(i)(x)+\beta_R(y)+K_1(j_+)(u)+K_1(j_-)(v) \end{align*} is an isomorphism of abelian groups. Hence \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*}[/step]

[guided]The point of this step is to make the external theorem precise enough that the argument is not circular. We do not invoke the present theorem under a different name. Instead, we invoke the projective-line form of Bass's fundamental theorem for algebraic $K$-theory, whose input is the cover of the algebraic projective line by the two affine charts $\operatorname{Spec} R[t]$ and $\operatorname{Spec} R[s]$, with overlap $\operatorname{Spec} R[t,t^{-1}]$ after identifying $s=t^{-1}$. The degree-one statement of that theorem, for the same Quillen low algebraic $K$-groups used in the theorem statement, is as follows. For every unital ring $A$, define \begin{align*} N^+K_1(A):=\ker\bigl(K_1(A[t])\xrightarrow{K_1(\operatorname{ev}_{0,t})}K_1(A)\bigr), \end{align*} where $\operatorname{ev}_{0,t}:A[t]\to A$ is the unital ring homomorphism determined by $\operatorname{ev}_{0,t}(t)=0$ and $\operatorname{ev}_{0,t}(a)=a$ for $a\in A$. Define also \begin{align*} N^-K_1(A):=\ker\bigl(K_1(A[s])\xrightarrow{K_1(\operatorname{ev}_{0,s})}K_1(A)\bigr), \end{align*} where $\operatorname{ev}_{0,s}:A[s]\to A$ is the unital ring homomorphism determined by $\operatorname{ev}_{0,s}(s)=0$ and $\operatorname{ev}_{0,s}(a)=a$ for $a\in A$. Let $i_A:A\to A[t,t^{-1}]$ be the constant Laurent polynomial inclusion, let $j_{+,A}:A[t]\to A[t,t^{-1}]$ send $t$ to $t$, and let $j_{-,A}:A[s]\to A[t,t^{-1}]$ send $s$ to $t^{-1}$. For the $K_0(A)$ summand, the theorem uses the Bass suspension map. If $P$ is a finitely generated projective left $A$-module, define \begin{align*} P[t,t^{-1}]:=A[t,t^{-1}]\otimes_A P. \end{align*} Multiplication by the Laurent unit $t$ on the first tensor factor gives an $A[t,t^{-1}]$-linear automorphism \begin{align*} \tau_P:P[t,t^{-1}]\to P[t,t^{-1}]. \end{align*} The class of this automorphism defines the Bass suspension contribution of $[P]$ in $K_1(A[t,t^{-1}])$. Additivity under direct sum makes this construction descend to a homomorphism \begin{align*} \beta_A:K_0(A)\to K_1(A[t,t^{-1}]). \end{align*} With these definitions, the projective-line fundamental theorem says that the homomorphism \begin{align*} \Phi_A:K_1(A)\oplus K_0(A)\oplus N^+K_1(A)\oplus N^-K_1(A)\to K_1(A[t,t^{-1}]) \end{align*} given by \begin{align*} \Phi_A(x,y,u,v)=K_1(i_A)(x)+\beta_A(y)+K_1(j_{+,A})(u)+K_1(j_{-,A})(v) \end{align*} is an isomorphism of abelian groups. Its hypotheses are only that $A$ is unital and that the polynomial, Laurent polynomial, evaluation, and chart-inclusion maps are the ones just specified. Now take $A=R$. The ring $R$ is unital by hypothesis. The maps $i$, $j_+$, $j_-$, the Bass suspension $\beta_R$, and the groups $NK_1^+(R)$ and $NK_1^-(R)$ defined earlier are exactly the specializations of $i_A$, $j_{+,A}$, $j_{-,A}$, $\beta_A$, $N^+K_1(A)$, and $N^-K_1(A)$ at $A=R$. Therefore the theorem gives an isomorphism \begin{align*} \Phi_R:K_1(R)\oplus K_0(R)\oplus NK_1^+(R)\oplus NK_1^-(R)\xrightarrow{\cong}K_1(R[t,t^{-1}]), \end{align*} where \begin{align*} \Phi_R(x,y,u,v)=K_1(i)(x)+\beta_R(y)+K_1(j_+)(u)+K_1(j_-)(v). \end{align*} Equivalently, \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*}[/guided]

[step:Check naturality of the decomposition] Let $\varphi:R\to S$ be a unital ring homomorphism. By functoriality of the low algebraic $K$-groups [citetheorem:8627], the ring maps used below induce the corresponding homomorphisms on $K_0$ and $K_1$. The homomorphism $\varphi$ 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. These homomorphisms commute with the constant inclusions, with evaluation at $0$, with the maps $j_+$ and $j_-$, and with multiplication by the Laurent variable $t$ after extension of scalars. Consequently the induced maps on $K$-groups send the $K_1(R)$ summand to the $K_1(S)$ summand, the $K_0(R)$ summand to the $K_0(S)$ summand, and the two evaluation-kernel summands $NK_1(R)$ to the corresponding two summands $NK_1(S)$. This is the naturality assertion in the Bass-Heller-Swan theorem, so the isomorphisms $\Phi_R$ are natural in $R$. [/step]

[step:Identify the two nil terms with the notation in the statement] By definition, \begin{align*} NK_1^+(R)=NK_1(R). \end{align*} The assignment $s\mapsto t$ identifies the abstract [polynomial ring](/page/Polynomial%20Ring) $R[s]$ with $R[t]$, and under this identification the evaluation map $\operatorname{ev}_0^-:R[s]\to R$ becomes the usual evaluation map $R[t]\to R$ at $t=0$. Hence \begin{align*} NK_1^-(R)\cong NK_1(R). \end{align*} Substituting these identifications into the Bass-Heller-Swan isomorphism 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 desired natural decomposition. [/step]