Improve proof of a cursed lemma

Thanks to Brian Conrad
http://stacks.math.columbia.edu/tag/08JZ#comment-1951

algebra.tex

@@ -33229,16 +33229,16 @@ \section{The naive cotangent complex}
 \item $J/J^2 = (I/I^2)_g \oplus B_g (f x - 1)$,
 \item $\Omega_{P[x]/A} \otimes_{P[x]} B_g =
 \Omega_{P/A} \otimes_P B_g \oplus B_g \text{d}x$,
-\item $\NL(\beta) = \NL(\alpha) \otimes_B B_g \oplus (B_g \xrightarrow{g} B_g)$
+\item $\NL(\beta) \cong
+\NL(\alpha) \otimes_B B_g \oplus (B_g \xrightarrow{g} B_g)$
 \end{enumerate}
 Hence the canonical map $\NL_{B/A} \otimes_B B_g \to \NL_{B_g/A}$
 is a homotopy equivalence.
 \end{lemma}
 
 \begin{proof}
 Since $P[x]/(I, fx - 1) = B[x]/(gx - 1) = B_g$ we get the statement about
-$I$ and $fx - 1$ generating $J$. To prove the other statements one can
-use the commutative diagram
+$I$ and $fx - 1$ generating $J$. Consider the commutative diagram
 $$
 \xymatrix{
 0 \ar[r] &
@@ -33249,18 +33249,51 @@ \section{The naive cotangent complex}
 &
 (I/I^2)_g \ar[r] \ar[u] &
 J/J^2 \ar[r] \ar[u] &
-(fx - 1)/(fx - 1)^2 \ar[r] \ar[u] &
+(gx - 1)/(gx - 1)^2 \ar[r] \ar[u] &
 0
 }
 $$
-with exact rows of Lemma \ref{lemma-exact-sequence-NL}. Then the only
-question left over is: why is $(I/I^2)_g \to J/J^2$ injective?
-It is enough to show that $\alpha ( I \cap J^2)=0$ where
-$\alpha : I \to I_f/I_f^2$ is the canonical map.
-So consider the extension of $\alpha$ to the $P$-algebra map
-$\pi : P[x] \to P_f/I_f^2$ given by $\pi(x) = 1/f$, and
-note that $\pi(J^2) = \pi(J)^2 = \pi(I[x])^2 = 0$, since
-$\pi(fx - 1) = 0$ implies $\pi(J) = \pi(I[x])$.
+with exact rows of Lemma \ref{lemma-exact-sequence-NL}.
+The $B_g$-module $\Omega_{B[x]/B} \otimes B_g$ is free of
+rank $1$ on $\text{d}x$. The element $\text{d}x$ in the
+$B_g$-module $\Omega_{P[x]/A} \otimes B_g$ provides
+a splitting for the top row. The element $gx - 1 \in (gx - 1)/(gx - 1)^2$
+is mapped to $g\text{d}x$ in $\Omega_{B[x]/B} \otimes B_g$
+and hence $(gx - 1)/(gx - 1)^2$ is free of rank $1$ over $B_g$.
+(This can also be seen by arguing that $gx - 1$ is a nonzerodivisor
+in $B[x]$ because it is a polynomial with invertible constant term
+and any nonzerodivisor gives a quasi-regular sequence of length $1$
+by Lemma \ref{lemma-regular-quasi-regular}.)
+
+\medskip\noindent
+Let us prove $(I/I^2)_g \to J/J^2$ injective. Consider the $P$-algebra map
+$$
+\pi : P[x] \to (P/I^2)_f = P_f/I_f^2
+$$
+sending $x$ to $1/f$. Since $J$ is generated by $I$ and $fx - 1$
+we see that $\pi(J) \subset (I/I^2)_f = (I/I^2)_g$. Since this
+is an ideal of square zero we see that $\pi(J^2) = 0$.
+If $a \in I$ maps to an element of $J^2$ in $J$, then
+$\pi(a) = 0$, which implies that $a$ maps to zero in $I_f/I_f^2$.
+This proves the desired injectivity.
+
+\medskip\noindent
+Thus we have a short exact sequence of two term complexes
+$$
+0 \to \NL(\alpha) \otimes_B B_g \to \NL(\beta)
+\to (B_g \xrightarrow{g} B_g) \to 0
+$$
+Such a short exact sequence can always be split in the category of
+complexes. In our particular case we can take as splittings
+$$
+J/J^2 = (I/I^2)_g \oplus B_g (fx - 1)\quad\text{and}\quad
+\Omega_{P[x]/A} \otimes B_g = \Omega_{P/A} \otimes B_g \oplus
+B_g (g^{-2}\text{d}f + \text{d}x)
+$$
+This works because
+$\text{d}(fx - 1) = x\text{d}f + f \text{d}x =
+g(g^{-2}\text{d}f + \text{d}x)$
+in $\Omega_{P[x]/A} \otimes B_g$.
 \end{proof}
 
 \begin{lemma}