Proposition. $\mathrm{Aut}(K / F) \to F$-embeddings [2207]

Let $K / F$ be an algebraic field extension.

1. Fix an algebraic closure of $F$ with $F \subseteq K \subseteq \overline{F}$. (By (2) of Proposition 1606, one can simply take $\overline{F} = \overline{K}$). Then we have the following bijective map$$\begin{align*}\mathrm{Aut}(K / F) &\to \left\{ F\text{-embeddings }\varphi : K \to \overline{F} \text{ s.t. } \varphi(K) = K\right\}, \\ \sigma &\mapsto \varphi_{\sigma} \text{ defined as } \varphi_{\sigma}(\alpha) = \sigma(\alpha).\end{align*}$$
2. If $K / F$ is finite, then$$\lvert \mathrm{Aut}(K / F) \rvert \leq \# \{ F\text{-embeddings from } K \text{ to } \overline{F} \}$$and the equality holds if and only if $K / F$ is normal.