The diagonal commutes with base change

Given: The objects, hypotheses and conventions in the statement above.

For $X\to S$, the diagonal morphism is the unique ${\mathrm{\Delta }}_{X\mathrm{/}S}:X\to X{\times }_{S}X$ satisfying ${\mathrm{pr}}_1{\mathrm{\Delta }}_{X\mathrm{/}S}={\mathrm{id}}_X={\mathrm{pr}}_2{\mathrm{\Delta }}_{X\mathrm{/}S}$. It exists by thm-fibre-products-of-schemes-exist. For any test scheme $T$, it takes an $S$-morphism $a:T\to X$ to the compatible pair $(a,a)$. (The diagonal morphism)

For $S^{\mathrm{\prime }\mathrm{\prime }}\stackrel{k}{\to }{S}^{\mathrm{\prime }}\stackrel{h}{\to }S$ and an $S$-scheme $X$, there is a canonical isomorphism $(X{\times }_S{S}^{\mathrm{\prime }}){\times }_{S^{\mathrm{\prime }}}{S}^{\mathrm{\prime }\mathrm{\prime }}\cong X{\times }_S{S}^{\mathrm{\prime }\mathrm{\prime }}\mathrm{.}$ It is functorial in $X$ and compatible with the induced maps of $S$-schemes. (Iterated base change)

For $S$-schemes $X,Y,Z$ there are natural projection-compatible isomorphisms $X{\times }_{S}Y\cong Y{\times }_{S}X,(X{\times }_{S}Y){\times }_{S}Z\cong X{\times }_S(Y{\times }_{S}Z),X{\times }_{S}S\cong X\cong S{\times }_{S}X\mathrm{.}$ Any coherence identity between these identifications holds whenever both sides induce the same ordered projections to the original factors. (Symmetry, associativity and units)