I'm reading the proof the Bass-Heller-Swan Theorem in Rosenberg's book *Algebraic K-Theory and Applications* (Theorem 3.2.22), which asserts
$$K_1(R[t,t^{-1}]) \cong K_0(R) \oplus K_1(R) \oplus NK^+_1(R) \oplus NK_1^-(R).$$
First it is shown that there are homomorphisms

$K_0(R) \oplus K_1(R) \xrightarrow{\Phi} K_1(R[t,t^{-1}]) \xrightarrow{\Psi} K_0(R) \oplus K_1(R)$

such that $\Psi \circ \Phi = \mathrm{id}$. If necessary, I will include their definitions here. There is a canonical map $$\alpha : NK^+_1(R) \oplus NK_1^-(R) \to \mathrm{coker}(\Phi)$$ mapping $([1+Nt],[1+Mt^{-1}]) \mapsto [(1 + Nt)(1+Mt^{-1})]$ for nilpotent $N,M$, and it is left to prove that this is an isomorphism. As for this step, Rosenberg isn't really precise.

Higman's trick shows that every element in the cokernel has the form $[1+(P+N)(t-1)]$ for commuting matrices $N,P$, where $N$ is nilpotent and $P$ is idempotent. Now Rosenberg seems to allude that $([1+PN t],[1+(1-P)N t^{-1}])$ is a preimage. But this is wrong, I think that $([1+(1-PN)^{-1} PN t],[1-(1+(1-P)N)^{-1} (1-P)N t^{-1}])$ is a preimage. So $\alpha$ is surjective. Anyway:

**Why is $\alpha$ injective?**

It is tempting to define a map in the other direction by the rule above, but then we have to show that this is well-defined, which is basically the same as to prove that $\alpha$ is injective. I've tried to use the isomorphism $\mathrm{coker}(\Phi) \cong \mathrm{ker}(\Psi)$ induced by $\mathrm{id} - \Phi \Psi$, according to which we "only" have to prove that a certain homomorphism $NK^+_1(R) \oplus NK_1^-(R) \to K_1(R[t,t^{-1}])$ is injective, but this didn't simplify the problem either.

I've already looked at the original sources: Bass-Heller-Swan (*The Whitehead group of a polynomial extension*) prove their Theorem only for regular rings. The first appearance of the Theorem with Nil terms seems to be in Bass' *Algebraic K-Theory*. But his treatment is rather abstract and more machinery is developed in order to optain the Theorem. Instead, I would like to know if it is possible to fix / complete Rosenberg's proof.