\documentclass{lecture}

\begin{document}

\begin{theorem}
    Let $(k, \le )$ be an ordered field and
    $k^{r}$ be a real closure of $k$ that extends the ordering of $k$. Let $L$
    be a orderable real-closed extension of $k$. Then there exists a unique
    homomorphism of $k$-algebras $k^{r} \to L$.
    \label{thm:unique-hom-of-real-closure-in-real-closed}
\end{theorem}

\begin{proof}
    Uniqueness: Let $\varphi\colon k^{r} \to L$ be a homomorphism of $k$-algebras and
    $a \in k^{r}$. Since $a$ is algebraic over $k$, it has
    a minimal polynomial $P \in k[t]$ over $k$. Denote
    by $a_1 \le \ldots \le a_n$ the roots of $P$ in $k^{r}$. Since
    the characteristic of $k$ is $0$, $k$ is perfect, in particular
    the irreducible polynomial $P$ is separable and thus
    $a_1 < \ldots < a_n$. Now there exists a unique $1, \ldots, n$ such that
    $a = a_j$. By \ref{lemma:number-of-roots-in-real-closed-extension}, the polynomial
    $P$ also has $n$ distinct roots $b_1 < \ldots < b_n$ in the real-closed field $L$.
    Since $\varphi$ sends roots of $P$ in $k^{r}$ to roots of $P$ in $L$, there is a
    permutation $\sigma \in S_n$ such that
    $\varphi(a_i) = b_{\sigma(i)}$. By \ref{lemma:hom-real-closed-fields-respects-orderings},
    $\varphi$ respects the ordering of the roots and thus $\sigma = \text{id}$
    and $\varphi(a) = \varphi(a_j) = b_j$.

    Existence: Consider the set $\mathcal{F}$ of all pairs
    $(E, \psi)$ where $k \subseteq E \subseteq k^{r}$ is a subextension
    of $k^{r} / k$ and $\psi\colon E \to L$ is a homomorphism of $k$-algebras. Since
    $(k, k \xhookrightarrow{} L) \in \mathcal{F}$, $\mathcal{F} \neq \emptyset$. Define
    an inductive ordering on $\mathcal{F}$ by $(E, \psi) \le (E', \psi)$
    if there is a commutative diagram
    \[
    \begin{tikzcd}
        & E' \arrow{d}{\psi'} \\
        E \arrow[dashed]{ur} \arrow{r}{\psi} & L
    \end{tikzcd}
    \] in the category of $k$-algebras. Then by Zorn, the set
    $\mathcal{F}$ admits a maximal element $(E, \psi)$. $E$ is real-closed, otherwise
    it admits a finite real extension $E'$ of $E$. In particular $E' \subseteq k^{r}$.
    Since $L$ is real-closed, $\psi\colon E \to L$ admits a continuation
    $\psi'\colon E' \to L$ by \ref{lemma:continuation-in-real-closed}.
    Thus $(E, \psi) < (E', \psi')$ contradicting the
    maximality of $(E, \psi)$. Hence $E$ is real-closed
    and $k^{r} / E$ is real algebraic, thus $E = k^{r}$. So
    $\psi$ is a homomorphism of $k$-algebras from $k^{r}$ to $L$.
\end{proof}

\begin{korollar}
    Let $(k, \le )$ be an ordered field. If $k_1^{r}$ and $k_2^{r}$ are real closures
    of $k$ whose canonical orderings are compatible with that of $k$, then
    there exists a unique isomorphism of $k$-algebras
    $k_1^{r} \xrightarrow{\simeq} k_2^{r}$.
    \label{kor:unique-iso-of-real-closures}
\end{korollar}

\begin{proof}
    By \ref{thm:unique-hom-of-real-closure-in-real-closed} there exist
    unique homomorphisms of $k$-algebras $\varphi\colon k_1^{r} \to k_2^{r}$
    and $\psi\colon k_2^{r} \to k_1^{r}$. Then
    $\psi \circ \varphi$ and $\text{id}_{k_1^{r}}$ are
    homomorphisms $k_1^{r} \to k_1^{r}$ of $k$-algebras. By uniqueness in
    \ref{thm:unique-hom-of-real-closure-in-real-closed},
    $\psi \circ \varphi = \text{id}_{k_1^{r}}$. Similarly, $\varphi \circ \psi = \text{id}_{k_2^{r}}$.
\end{proof}

\begin{bem}
    Contrary to the situation of algebraic closures of a field $k$,
    for ordered fields $(k, \le)$ there is a well-defined notion
    of the real closure of $k$ whose canonical ordering is compatible with that of $k$.
    As shown by \ref{bsp:different-real-closures-depending-on-ordering},
    it is necessary to fix an ordering of the real field $k$ to get the
    existence of an isomorphism of fields between two orderable real closures of $k$.
\end{bem}

\begin{korollar}
    Let $(k, \le )$ be an ordered field and let $k^{r}$ be the real closure of $k$.
    Then $k^{r}$ has no non-trivial $k$-automorphism.
\end{korollar}

\begin{proof}
    Take $k_1^{r} = k_2^{r}$ in \ref{kor:unique-iso-of-real-closures}.
\end{proof}

\end{document}