I've been thinking about my previous question a bit more, and I'm afraid I still don't quite understand. See: Can the natural embedding $K\to K[X]/(f)$ be extended to form an isomorphism $L/K\to K[X]/(f)$?
The theorem I'm trying to prove is as follows: given a field $K$ and an irreducible polynomial $f\in K[X]$, there always exists a (finite) extension $L$ of $K$ such that $L$ contains at least one root of $f$.
Most proofs that I've seen on the internet and in algebra textbooks run like this: $K$ can be embedded in $L'=K[X]/(f)$, which is a field (because $(f)$ is a maximal ideal). So $L'$ is isomorphic to a field extension $L$ of $K$. Then define $\alpha=X\pmod{f}$, and substitute $\alpha$ in $f$. This gives you $0$, so $\alpha$ is a root of $f$.
I get the basic idea, sure enough. But when I try to write a fully rigorous proof, I get stuck.
First of all, literally substituting $\alpha$ in $f$ is impossible, because $\alpha$ is a coset, and not an element of $L$. So, we have to replace the coefficients $a_i$ of $f$ by the corresponding cosets $\overline{a_i}$. This works fine.
But how on Earth do we know for certain that this new polynomial $\sum_i\overline{a_i}X^i$ (which is in $L'[X]$) corresponds, as far as roots are concerned, to the old $f$ (which is in $K[X]$)?
It seems that all proofs I've seen so far implicitly assume that there is an isomorphism $L\to L'$ such that $a_i\mapsto\overline{a_i}$ for all $a_i\in K$. But this is highly non-trivial. Or am I missing something?
The field generated by the companion matrix of $f$ over $K$ gives you the desired extension.