Questions about proof of existence of roots of $f$ in $K[X]/(f)$

Question

Let $f \in K[X]$ with $deg(f)\geq 1$. Then there exists an algebraic field extension $L/K$, such that $f$ has a root in $L$.

Proof: WLOG we can assume that $f \in K[X]$ is irreducible. Since $L=K[X]/(f)$ is a field and $K[X]/(f)\cong K(a)$, where $a$ is a root of $f$, it is clear that $L/K$ is an algebraic field extension. It is apparent that $x=X+(f)$ is a root of $f$ in $L$.

The lemma showing $K[X]/(f)\cong K(a)$ was shown by assuming that $f=\mu_{a,K}$, and then showing that $(f)$ is the kernel of the evaluation map at $a$ and it is only cited in the proof, not explicitly written out.

This lemma is used in the proof of existence of algebraically closed fields and is proved before it.

1. Why can we assume that there exists a root of $f$? Does this assumption not already prove the lemma by itself? Is this not circular?
2. Is the class of $f$ not $0 \in L$, since $f \in (f)$? Why even look for roots if everything suffices?
3. Why would $x=X+(f)$ be proposed as the root?

Answer 1

Well, the situation is quite simple. Given the quotient ring $K(x)/\langle f(x)\rangle$, the residue class of $x$, $\bar x = x+\langle f(x)\rangle$, fulfills $f(\bar x)=f(x)+\langle f(x)\rangle = \bar 0$ and so $\bar x$ is a zero.

If $f(x)$ is irreducible over $K$, then $K[x]/\langle f(x)\rangle$ is a field extension of $K$ whose degree is given by the degree of $f(x)$, and $f(x)$ is the minimal polynomial of $\bar x$.