Proposition. uniqueness of algebraic closures up to isomorphisms [1607]

    Let $F$ be a field.

    1. $F$ has an algebraic closure.
    2. If $L, L'$ are both algebraic closure of $F$, then there exists a field isomorphism $\varphi : L \to L'$ such that $\varphi|_{F} = \operatorname{id}_{F}$.

    Proof. sketch (TODO) [1607A]

      1. TODO
      2. Apply Proposition 1603 to $L / F$ and the natural field embedding $F \to L'$, then there exists a field embedding $\varphi : L \to L'$ such that $\varphi |_{F} = \operatorname{id}_{F}$. By Proposition 1605, $L$ and $L'$ are both algebraically closed. Then $L$ is algebraically closed $\implies$ $\varphi(L)$ is algebraically closed since $L \cong \varphi(L)$ (recall that a field homomorphism is either $0$ or its kernel is $0$). By Proposition 14012, $L' / F$ is algebraic $\implies$ $L' / \varphi(L)$ is algebraic. By part 4 of Proposition 1601, $L' = \varphi(L)$ since $L'$ is algebraically closed.