In stacks project, the ring map $R\rightarrow S$ is called smooth if it is of finite presentation and the naive cotangent complex $NL_{S/R}: I/I^2\xrightarrow{f}{\Omega}_{R[S]/R}\otimes_{R[S]}S$ is quasi-isomorphic to a finite projective $S$-module placed in degree $0$. So by looking at homology at dimension $0$ and $1$, this means $f$ is injective and $\text{coker}f$ is a finite projective $S$-module.
I want to learn the proof of lemma 10.136.4 which said that if $R\rightarrow S$ is smooth and $R'$ is a $R$ algebra, then $R'\rightarrow S'=R'\otimes S$ is smooth. At the bottom of the proof, I can't see why $NL(\alpha')$ is quasi-isomorphic to $S'\otimes_R\Omega_{S/R}$ from the commutative diagrm, I think this means an injectivity and $\Omega_{S'/R'}\cong S'\otimes_R\Omega_{S/R}$.
The injectivity is clear, right?
For the isomorphism, I think the coker of the upper horizontal map is $R'\otimes_R\Omega_{S/R}$, and the kernel of the lower horizontal map is $\Omega_{S'/R'}$, so this is a isomorphism of $R'$ module, tensor $S'$, we get a isomrophism of $S'$ module: $S'\otimes_R\Omega_{S/R}\rightarrow S'\otimes_{R'}\Omega_{S'/R'}$. I can't deduce $\Omega_{S'/R'}\cong S'\otimes_R\Omega_{S/R}$.
Where I am wrong?
Also, is this definition of smoothness of ring maps is standard? I haven't seen this definition anywhere else.
Thanks.
Regarding the injectivity: the injectivity of the horizontal map upstairs comes from the injectivity of $I/I^2 \rightarrow \Omega_{R[\underline{x}]/R}\otimes_{R[\underline{x}]} S$ upon noting that the injection is split, hence the injectvity remains even after the base change $R'\otimes_R -$. Using this, one deduces that both the vertical maps are isomorphisms, as in the proof. Then the injectivity downstairs follows from the injectivity upstairs.
Regarding the base-change computing part: You don't need to do an additional base change: The point is that already one has $$\Omega_{S'/R'} \simeq R'\otimes_R\Omega_{S/R} \simeq S'\otimes_S\Omega_{S/R}.$$
For the first isomorphism, see Tag 00RV (actually, it follows from the proof itself also). For the second, more generally one has for any $S$-module $M$ $$S'\otimes_S M= (R'\otimes_R S)\otimes_S M \simeq R'\otimes_R(S\otimes_S M) \simeq R'\otimes_RM.$$ The reason why $\Omega_{S'/R'}=S'\otimes_{S}\Omega_{S/R}$ is explicitely mentioned is that this isomorphism shows that the cokernel of the map downstairs, which is $\Omega_{S'/R'},$ is projective as an $S'$-module.
Regarding the standardness: Maybe it's not standard to talk about the naive cotangent complex, but note that the condition for $R \rightarrow S$ to be smooth can be also restated as
This is pretty close to saying "$R\rightarrow S$ is of finite presentation and formally smooth," which, in case this is still not the standard definition, it is at least standard characterization of smoothness.