Formal base change properties of group schemes Let $S$ be an arbitrary scheme, and let $X,Y,S'$ be $S$-schemes. EGA 1, Chap 1, 3.3, gives nice properties for products of schemes with respect to base change $S'\to S$. For example (3.3.10): There exists a canonical isomorphism $$\varphi:(X\times_SY)_{S'}\cong X_{S'}\times_{S'}Y_{S'}$$
of $S'$-schemes.
Suppose now that $X$ and $Y$ are $S$-group schemes. Then $X\times_S Y$ has the structure of an $S$-group scheme, and $X_{S'}$ has the structure of an $S'$-group scheme.
Question: Ist the canonical isomorphism $\varphi$ of $S'$-schemes in addition a morphism of $S'$-group schemes? If yes, is there a precise reference for this statement (or more generally for versions of EGA 1, Chap 1, 3.3, for $S$-group schemes)?
 A: To show that the scheme isomorphism is an isomorphism of group schemes, it suffices to check that the multiplication maps coincide, i.e., $$m_{(X \times_S Y)_{S'}} = \phi^{-1} \circ (m_{X_{S'}} \times_{S'} m_{Y_{S'}}) \circ \tau_{23} \circ (\phi \times_{S'} \phi),$$
where $\tau_{23}: X_{S'} \times_{S'} Y_{S'} \times_{S'} X_{S'} \times_{S'} Y_{S'} \to X_{S'} \times_{S'} X_{S'} \times_{S'} Y_{S'} \times_{S'} Y_{S'}$ is the canonical switch isomorphism.  The result follows from how we define multiplication on base-changed group schemes (i.e., $m_{(X \times_S Y)_{S'}} = (m_{X \times_S Y} \times_S id_{S'}) \circ \tau_{23}$), and the multiplication law on a direct product of groups (i.e., $m_{X \times_S Y} = (m_X \times_S m_Y) \circ \tau_{23}$).
You're unlikely to find a reference that spells out the full network of canonical isomorphisms and checks all compatibilities between fiber product objects.  However, the universal property of fiber products makes all of the relevant maps uniquely determined, so we can just abuse equal signs (and someday, automate such checks and/or redefine equality).  Some hints at compatibilities can be found in EGA1 Chap. 1 section 3.4 and SGA3 Exp. 1 sections 2.1 and 2.2.
