I'm studying for an abstract algebra exam (covering commutative rings and Galois theory). As an exercise, I'm trying to work out on my own a proof of the theorem that, given a field $K$ and a polynomial $f\in K[X]$, there exists a finite extension $L/K$ such that $L$ contains a root of $f$. Of course it suffices to prove this for $f$ irreducible.
The textbook's author simply says something like:
Because $f$ is irreducible, $K[X]/(f)$ is a field, $(f)$ being a maximal ideal. Now, $X\pmod f$ is an obvious zero.
Nothing further.
This is a bit too terse for my taste, so I've decided to devise a nicer proof (using the same basic idea, however).
But now I'm stuck on the following question:
Let $K$ be a field and $f\in K[X]$ irreducible. Then $K[X]/(f)$ is a field. Also, there exists a natural injective homomorphism (i.e., an embedding) $\phi:K\to K[X]/(f)$ given by $a\mapsto a\pmod f$. So, $K[X]/(f)$ is isomorphic to a field extension $L$ of $K$. But does this necessarily entail that there exists an isomorphism $\psi:K[X]/(f)\to L$ such that $\psi^{-1}$ restricted to $K$ equals $\phi$?
I would like to know because if the answer is affirmative, then the following calculation (with $\alpha=X+(f)$ and $f(X)=a_nX^n+\cdots+a_0$) becomes completely straightforward:
$$f(\psi(\alpha)) = \sum_{j=0}^{n}a_{j}\big(\psi(X+(f))\big)^{j}=\sum_{j=0}^{n}a_{j}\psi\big((X+(f))^{j}\big)=\sum_{j=0}^{n}a_{j}\psi\big(X^{j}+(f)\big) = \sum_{j=0}^{n}\psi(\psi^{-1}(a_{j}))\psi\big(X^{j}+(f)\big)=\sum_{j=0}^{n}\psi\big(\psi^{-1}(a_{j})[X^{j}+(f)]\big) = \sum_{j=0}^{n}\psi\big([a_{j}+(f)][X^{j}+(f)]\big)=\sum_{j=0}^{n}\psi\big(a_{j}X^{j}+(f)\big) = \psi\left(\sum_{j=0}^{n}a_{j}X_{j}+(f)\right)=\psi(f+(f))=\psi(0+(f)))=0. $$
Many thanks in advance.
$L$ is viewed as an extension $L/K$ but the fact is that $L$ just contains an isomorphic copy $K'$ (as field) of $K$ which we identify with $K$ then we think of $K'$ as $K$ (since they are isomorphic as fields) and say $L/K$ and not $L/K'$.
So when you write about the restriction to $K$ it is important to note what this theorem gives you - $L:=K[x]/\langle f\rangle$ and $K$ is not a subset of $L$ - but the constant polynomials in the quotient are isomorphic copy of $K$
Regarding the root $\alpha$ of $f$ in $L$ : let $$\alpha=\bar{x}\in L= K[x]/\langle f\rangle$$ then $$f(\alpha)=\sum_{i=0}^{n}a_{i}\bar{x}^{i}=\bar{f}\equiv_{\langle f\rangle}0$$