[proofplan] We use the central idempotents $e_R=(1_R,0_S)$ and $e_S=(0_R,1_S)$ in $R\times S$ to decompose modules over the product ring into their $R$- and $S$-parts. This decomposition identifies finitely generated projective $(R\times S)$-modules with pairs consisting of a finitely generated projective $R$-module and a finitely generated projective $S$-module, compatibly with direct sums. Hence it gives an isomorphism of the commutative monoids $V(R\times S)\cong V(R)\times V(S)$, and applying the universal property of group completion gives the asserted isomorphism on $K_0$. [/proofplan]

[step:Decompose modules over $R\times S$ using the two product idempotents] Let $A:=R\times S$, and let \begin{align*} e_R:=(1_R,0_S)\in A \end{align*} and \begin{align*} e_S:=(0_R,1_S)\in A. \end{align*} Then $e_R^2=e_R$, $e_S^2=e_S$, $e_Re_S=0$, and $e_R+e_S=1_A$. Let $P$ be a left $A$-module. Define $e_RP:=\{e_Rp:p\in P\}$ and $e_SP:=\{e_Sp:p\in P\}$. The set $e_RP$ is a left $R$-module by \begin{align*} r\cdot x := (r,0_S)x \end{align*} for $r\in R$ and $x\in e_RP$. Similarly, $e_SP$ is a left $S$-module by \begin{align*} s\cdot y := (0_R,s)y \end{align*} for $s\in S$ and $y\in e_SP$. For every $p\in P$ one has \begin{align*} p=1_Ap=(e_R+e_S)p=e_Rp+e_Sp. \end{align*} If $x\in e_RP\cap e_SP$, then $x=e_Rx$ and $x=e_Sx$, so \begin{align*} x=e_Rx=e_Re_Sx=0. \end{align*} Therefore \begin{align*} P=e_RP\oplus e_SP \end{align*} as abelian groups, and this decomposition is compatible with the $A$-module structure. [/step]

[step:Identify the module category of the product with a product category]Define a functor \begin{align*} \Phi:A\operatorname{-Mod}\to R\operatorname{-Mod}\times S\operatorname{-Mod} \end{align*} by \begin{align*} \Phi(P):=(e_RP,e_SP) \end{align*} on objects and, for an $A$-[linear map](/page/Linear%20Map) $f:P\to Q$, by \begin{align*} \Phi(f):=(f|_{e_RP},f|_{e_SP}). \end{align*} The restrictions are well-defined because, for $x\in e_RP$, \begin{align*} f(x)=f(e_Rx)=e_Rf(x)\in e_RQ, \end{align*} and the same argument applies to $e_SP$. Conversely, define a functor \begin{align*} \Psi:R\operatorname{-Mod}\times S\operatorname{-Mod}\to A\operatorname{-Mod} \end{align*} by \begin{align*} \Psi(M,N):=M\oplus N \end{align*} with $A$-action \begin{align*} (r,s)\cdot(m,n):=(rm,sn) \end{align*} for $(r,s)\in A$ and $(m,n)\in M\oplus N$. On morphisms, $\Psi$ sends a pair $(g,h)$, where $g:M\to M'$ is $R$-linear and $h:N\to N'$ is $S$-linear, to the $A$-linear map \begin{align*} g\oplus h:M\oplus N\to M'\oplus N' \end{align*} given by \begin{align*} (g\oplus h)(m,n):=(g(m),h(n)). \end{align*} The decomposition in the previous step gives a natural $A$-linear isomorphism \begin{align*} P\to \Psi\Phi(P) \end{align*} sending $p\mapsto(e_Rp,e_Sp)$. Its inverse sends $(x,y)\mapsto x+y$. Also $\Phi\Psi(M,N)=(M,N)$ with the evident identifications. Thus this is the product-ring module equivalence described in [Projectives over a Product Ring][citetheorem:8635].[/step]

[guided]The purpose of this step is to turn the algebra of the product ring into a categorical statement about modules. We define \begin{align*} \Phi:A\operatorname{-Mod}\to R\operatorname{-Mod}\times S\operatorname{-Mod} \end{align*} by \begin{align*} \Phi(P):=(e_RP,e_SP). \end{align*} If $f:P\to Q$ is $A$-linear, then $f$ respects the two summands because $A$-linearity gives \begin{align*} f(e_Rx)=e_Rf(x) \end{align*} for every $x\in P$, and similarly with $e_S$. Hence $\Phi(f)$ is the pair of restrictions \begin{align*} \Phi(f):=(f|_{e_RP},f|_{e_SP}). \end{align*} Now we construct the inverse direction. Given a left $R$-module $M$ and a left $S$-module $N$, define \begin{align*} \Psi(M,N):=M\oplus N \end{align*} as an abelian group, with left $A=R\times S$ action \begin{align*} (r,s)\cdot(m,n):=(rm,sn). \end{align*} This is an $A$-module because multiplication in $R\times S$ is componentwise. If $(r,s),(r',s')\in A$ and $(m,n)\in M\oplus N$, then \begin{align*} (r,s)\cdot((r',s')\cdot(m,n))=(r,s)\cdot(r'm,s'n)=(rr'm,ss'n). \end{align*} This equals \begin{align*} ((r,s)(r',s'))\cdot(m,n), \end{align*} and the identity element $(1_R,1_S)$ acts as the identity. For a module $P$ over $A$, the map \begin{align*} P\to e_RP\oplus e_SP \end{align*} defined by \begin{align*} p\mapsto(e_Rp,e_Sp) \end{align*} is $A$-linear. Its inverse is \begin{align*} e_RP\oplus e_SP\to P \end{align*} given by \begin{align*} (x,y)\mapsto x+y. \end{align*} The inverse property follows from $p=e_Rp+e_Sp$ and from the fact that $x=e_Rx$ and $y=e_Sy$ for $x\in e_RP$ and $y\in e_SP$. Thus the two constructions are mutually inverse up to natural isomorphism. This is precisely the equivalence stated in [Projectives over a Product Ring][citetheorem:8635].[/guided]

[step:Restrict the equivalence to finitely generated projective modules] We verify that the preceding equivalence restricts to finitely generated projective modules. First, suppose $P$ is a finitely generated projective left $A$-module. Since $P$ is finitely generated, there is an integer $n\ge 0$ and a surjective $A$-linear map \begin{align*} A^n\to P. \end{align*} Applying $\Phi$ gives surjective maps \begin{align*} R^n\to e_RP \end{align*} and \begin{align*} S^n\to e_SP, \end{align*} so $e_RP$ and $e_SP$ are finitely generated. Since $P$ is projective, the surjection $A^n\to P$ splits. Hence there exists a left $A$-module $Q$ such that \begin{align*} A^n\cong P\oplus Q. \end{align*} Set $m:=n$. Applying $\Phi$ gives \begin{align*} e_RP\oplus e_RQ\cong R^m \end{align*} and \begin{align*} e_SP\oplus e_SQ\cong S^m. \end{align*} Thus $e_RP$ is projective over $R$ and $e_SP$ is projective over $S$. Conversely, suppose $M$ is a finitely generated projective left $R$-module and $N$ is a finitely generated projective left $S$-module. Choose integers $m,n\ge 0$ and modules $M'$ over $R$ and $N'$ over $S$ such that \begin{align*} M\oplus M'\cong R^m \end{align*} and \begin{align*} N\oplus N'\cong S^n. \end{align*} Let $k:=\max(m,n)$. Replacing $M'$ by $M'\oplus R^{k-m}$ and $N'$ by $N'\oplus S^{k-n}$, we obtain isomorphisms \begin{align*} M\oplus M'\cong R^k \end{align*} and \begin{align*} N\oplus N'\cong S^k. \end{align*} Therefore \begin{align*} (M\oplus N)\oplus(M'\oplus N')\cong R^k\oplus S^k\cong A^k \end{align*} as left $A$-modules. Hence $\Psi(M,N)=M\oplus N$ is projective over $A$. It is finitely generated because finite generating sets for $M$ and $N$ together generate $M\oplus N$ over $A$. [/step]

[step:Construct the monoid isomorphism on $V$] For a unital ring $T$, let $V(T)$ denote the commutative monoid of isomorphism classes $[P]$ of finitely generated projective left $T$-modules, with operation \begin{align*} [P]+[Q]:=[P\oplus Q]. \end{align*} The operation is a commutative monoid operation by [V Is A Commutative Monoid][citetheorem:8629]. Define a map of commutative monoids \begin{align*} \theta:V(A)\to V(R)\times V(S) \end{align*} by \begin{align*} \theta([P]):=([e_RP],[e_SP]). \end{align*} This is well-defined because isomorphic $A$-modules have isomorphic $R$- and $S$-components under $\Phi$. It is a monoid homomorphism because $\Phi$ preserves direct sums: \begin{align*} e_R(P\oplus Q)=e_RP\oplus e_RQ \end{align*} and \begin{align*} e_S(P\oplus Q)=e_SP\oplus e_SQ. \end{align*} Define \begin{align*} \eta:V(R)\times V(S)\to V(A) \end{align*} by \begin{align*} \eta([M],[N]):=[M\oplus N], \end{align*} where $M\oplus N$ is regarded as an $A$-module through $\Psi$. The equivalence above shows that $\theta\eta$ and $\eta\theta$ are identity maps. Therefore \begin{align*} V(R\times S)\cong V(R)\times V(S) \end{align*} as commutative monoids. [/step]

[step:Apply group completion and identify the resulting product] For any commutative monoid $M$, let $G(M)$ denote its group completion with universal monoid homomorphism \begin{align*} \iota_M:M\to G(M). \end{align*} By the defining convention for $K_0$, \begin{align*} K_0(T):=G(V(T)) \end{align*} for every unital ring $T$. The monoid isomorphism $\theta:V(A)\to V(R)\times V(S)$ induces an isomorphism \begin{align*} G(V(A))\cong G(V(R)\times V(S)). \end{align*} It remains to identify the group completion of the product monoid. By the [Universal Property of Group Completion][citetheorem:8633], for every abelian group $B$ and every monoid homomorphism \begin{align*} f:V(R)\times V(S)\to B, \end{align*} there is a unique [group homomorphism](/page/Group%20Homomorphism) from $G(V(R)\times V(S))$ to $B$ extending $f$. The product group $G(V(R))\times G(V(S))$, together with the monoid homomorphism \begin{align*} ([M],[N])\mapsto(\iota_{V(R)}([M]),\iota_{V(S)}([N])), \end{align*} has the same universal property. Indeed, if $f:V(R)\times V(S)\to B$ is a monoid homomorphism, then \begin{align*} f(x,y)=f(x,0)+f(0,y) \end{align*} for all $x\in V(R)$ and $y\in V(S)$. Thus $f$ is determined by the two restricted monoid homomorphisms $x\mapsto f(x,0)$ and $y\mapsto f(0,y)$. These uniquely extend to group homomorphisms $u:G(V(R))\to B$ and $v:G(V(S))\to B$, and the corresponding group homomorphism $G(V(R))\times G(V(S))\to B$ is \begin{align*} (a,b)\mapsto u(a)+v(b). \end{align*} Therefore \begin{align*} G(V(R)\times V(S))\cong G(V(R))\times G(V(S)). \end{align*} Combining the displayed isomorphisms gives \begin{align*} K_0(R\times S)\cong K_0(R)\times K_0(S). \end{align*} Let $e_{R'}:=(1_{R'},0_{S'})\in R'\times S'$ and $e_{S'}:=(0_{R'},1_{S'})\in R'\times S'$. Naturality follows because for unital ring homomorphisms $\alpha:R\to R'$ and $\beta:S\to S'$, the induced homomorphism \begin{align*} \alpha\times\beta:R\times S\to R'\times S' \end{align*} sends $e_R$ to $e_{R'}$ and $e_S$ to $e_{S'}$. Under the product-ring equivalence, extension of scalars admits the componentwise comparison isomorphism \begin{align*} (R'\times S')\otimes_{R\times S}P \cong (R'\otimes_R e_RP)\oplus(S'\otimes_S e_SP) \end{align*} given on pure tensors by \begin{align*} (r',s')\otimes p \mapsto (r'\otimes e_Rp, s'\otimes e_Sp). \end{align*} Its inverse sends $(r'\otimes x,s'\otimes y)$ to $(r',0_{S'})\otimes x+(0_{R'},s')\otimes y$. These formulas are balanced over $R\times S$ because $e_R$ and $e_S$ project onto the two factors, and they identify the $e_{R'}$- and $e_{S'}$-summands of the scalar extension with $R'\otimes_R e_RP$ and $S'\otimes_S e_SP$. Hence the product decomposition on $K_0$ commutes with the induced maps. [/step]