[proofplan] This is a direct application of the Extension of Embeddings to Algebraic Closures theorem. We take the inclusion $\iota: k \hookrightarrow \overline{k}$ as the base embedding, note that $\overline{k}$ is algebraically closed, and apply the extension theorem to obtain an embedding $\tau: K \to \overline{k}$ extending $\iota$, which is by definition a $k$-embedding. [/proofplan] [step:Set up the inclusion embedding and verify the hypotheses of the extension theorem] Let $\overline{k}$ denote the algebraic closure of $k$. Consider the inclusion map \begin{align*} \iota: k &\hookrightarrow \overline{k} \\ a &\mapsto a. \end{align*} This is a field embedding (an injective ring homomorphism). The target $\overline{k}$ is algebraically closed by definition of the algebraic closure. The extension $K/k$ is algebraic by hypothesis. [/step] [step:Apply the Extension of Embeddings to Algebraic Closures] We apply the [Extension of Embeddings to Algebraic Closures](/theorems/3322) with $\sigma = \iota: k \hookrightarrow \overline{k}$, $\Omega = \overline{k}$ (which is algebraically closed), and $K/k$ (which is algebraic). The theorem's hypotheses are satisfied: - $\sigma = \iota$ is a field embedding from $k$ into $\Omega = \overline{k}$, - $\Omega = \overline{k}$ is algebraically closed, - $K/k$ is an algebraic extension. The theorem yields a field embedding $\tau: K \to \overline{k}$ satisfying $\tau|_k = \iota$. Since $\iota$ is the inclusion, the condition $\tau|_k = \iota$ means $\tau(a) = a$ for all $a \in k$, i.e., $\tau$ fixes $k$ pointwise. Therefore $\tau$ is a $k$-embedding $K \hookrightarrow \overline{k}$. [guided] The statement of this theorem is essentially a special case of the [Extension of Embeddings to Algebraic Closures](/theorems/3322), so let us verify carefully that the hypotheses match. The Extension of Embeddings theorem states: given a field embedding $\sigma: k \to \Omega$ where $\Omega$ is algebraically closed and $K/k$ is an algebraic extension, there exists a field embedding $\tau: K \to \Omega$ extending $\sigma$ (i.e., $\tau|_k = \sigma$). We instantiate the theorem as follows: - The field embedding $\sigma$ is taken to be the inclusion $\iota: k \hookrightarrow \overline{k}$, sending each element of $k$ to itself inside $\overline{k}$. This is a valid field embedding because $k \subset \overline{k}$. - The algebraically closed field $\Omega$ is $\overline{k}$. By definition, $\overline{k}$ is an algebraic extension of $k$ in which every non-constant polynomial over $\overline{k}$ has a root. In particular, $\overline{k}$ is algebraically closed. - The algebraic extension $K/k$ is given by hypothesis. All three hypotheses are satisfied. The conclusion gives a field embedding $\tau: K \to \overline{k}$ with $\tau|_k = \iota$. What does $\tau|_k = \iota$ mean concretely? For every $a \in k$, $\tau(a) = \iota(a) = a$. So $\tau$ fixes every element of $k$. A field embedding that fixes the base field $k$ pointwise is called a $k$-embedding. Therefore $\tau: K \hookrightarrow \overline{k}$ is the desired $k$-embedding. [/guided] [/step]