Independence of the chosen algebraic closure

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

A geometric point of a scheme $S$ is a morphism $\mathrm{Spec}\mathrm{\Omega }\to S$ with $\mathrm{\Omega }$ algebraically closed. For a specified point $s\in S$, choose an algebraic closure $\mathrm{\Omega }\mathrm{/}\kappa (s)$, in the sense of def-algebraic-closure. In this page the geometric fibre at $s$ means $X_{\bar{s}}=X_s{\times }_{\mathrm{Spec}\kappa (s)}\mathrm{Spec}\mathrm{\Omega }\mathrm{.}$ Here $X_s$ is def-scheme-theoretic-fibre, and its affine charts extend as in lem-base-extension-field-coordinate-ring. The choice includes the embedding of $\kappa (s)$; no preferred algebraic closure or preferred isomorphism between choices is implied. (Geometric fibres and geometric points)

Assuming the Axiom of Choice, any two algebraic closures of a field $F$ are $F$-isomorphic. No uniqueness of the isomorphism is asserted. (Assuming Choice, any two algebraic closures are base-isomorphic)

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)