The extension is Galois iff E is a splitting field of a separable polynomial of F[x]

[mathmari]

Hey!

Let $E/F$ be a finite extension.
I want to show that this extension is Galois if and only if $E$ is a splitting field of a separable polynomial of $F[x]$. I have done the folllowing:

$\Rightarrow$ :
We suppose that $E/F$ is Galois. So, we have that the extension is normal and separable.
Since the extension is normal we have that $E$ is a splitting field of a polynomial $f\in F[x]$.
Let $p(x)$ be an irreducible factor of $f(x)$.
Let $a$ be a root of $p(x)$ then $a$ is also a root of $f(x)$, so $a\in E$.
We have that $p(x)=\lambda \text{Irr}(a,F), \lambda\in F$.
Since the extension $E/F$ is separable we have that for each element $e\in E$ the $\text{Irr}(e,F)$ is separable, so it has only simple roots.
So, $\text{Irr}(a,F)$ has only simple roots, so also $p(x)$, so $p(x)$ is separable.
We have that a polynomial is separable if each irreducible factor is separable. So, $f(x)$ is separable.
So, $E$ is a splitting field of a separable polynomial $f(x)$.

Is this direction correct? (Wondering) $\Leftarrow$ :
We suppose that $E$ is a splitting field of a separable polynomial of $F[x]$, say $f(x)$.
From that we conclude that the extension $E/F$ is normal. So, each irreducible polynomial of $F[x]$ that has a root in $E$, has all the roots in $E$.
Let $a\in E$ be a root of $f(x)$.
$\text{Irr}(a,F)$ is an irreducible factor of $f(x)$. Since $f(x)$ is separable, we have that $\text{Irr}(a,F)$ is also separable.
To show that the extension $E/F$ is separable we have to show that for each $e\in E$ the $\text{Irr}(e,F)$ is separable, right?
From what I have shown so far, we have that this holds only for those elements of $E$ that are a root of $f(x)$, or not? (Wondering)

 

[mathmari]

Let $a\in E$ be a root of $f(x)$.
$\text{Irr}(a,F)$ is an irreducible factor of $f(x)$. Since $f(x)$ is separable, we have that $\text{Irr}(a,F)$ is also separable.
To show that the extension $E/F$ is separable we have to show that for each $e\in E$ the $\text{Irr}(e,F)$ is separable, right?
From what I have shown so far, we have that this holds only for those elements of $E$ that are a root of $f(x)$, or not? (Wondering)

I changed this part... Let $a_1,a_2,\ldots,a_n\in E$ be all the roots of $f(X)$. Then $E=F(a_1,a_2,\ldots,a_n)=F(a_1)(a_2)(a_3)\ldots(a_n)$.
We have that when $a$ is separable $/F$, then the extension $F(a)$ is separable $/F$.
Let $a_i\in \{a_1, a_2, \ldots , a_n\}$ with $1\leq i \leq n$.
We will show that the extension $F(a_1, a_2, \ldots , a_n)$ is separable $/F$ by induction on $i$.

Base case: For $i=1$ we have that $m(a_1, F)$ is an irreducible factor of $f(X)$. Since $f(X)$ is separable, we have that $m(a_1, F)$ is separable. So, $a_1$ is separable $/F$. Then the extension $F(a_1)$ is separable $/F$.
Inductive Hypothesis: We suppose that it holds for $i=k$, i.e., the extsnion $F(a_1, \ldots , a_k)$ is separable $/F$.
Inductive step: We will show that it holds for $i=k+1$, i.e., that the extension $F(a_1, \ldots , a_{k+1})$ is separable $/F$. We have that $F(a_1, \ldots , a_{k+1})=F(a_1, \ldots , a_k)(a_{k+1})$. We have the extensions $$F\leq F(a_1, \ldots , a_k)\leq F(a_1, \ldots , a_k)(a_{k+1})$$
We have that $m(a_{k+1}, F(a_1, \ldots , a_k))$ is an irreducible factor of $f(X)\in F[X]\leq F(a_1, \ldots , a_k)[X]$. Since $f(X)$ is separable, we have that $m(a_{k+1}, F(a_1, \ldots , a_k))$is also separable. So, $a_{k+1}$ is separable $/F(a_1, \ldots , a_k)$. Then the extension $F(a_1, \ldots , a_k)(a_{k+1})$is separable $/F(a_1, \ldots , a_k)$.
From the inductive hypothesis we have that the extension $F(a_1, \ldots , a_k)$ is separable $/F$.
Therefore, the extension $F(a_1, \ldots , a_k)( a_{k+1})$ is separable $/F$.

So, the extension $E/F=F(a_1, a_2, \ldots , a_n)/F$ is separable.
Therefore, the extension $E/F$ is Galois. Is it correct now? Could I improve something? (Wondering)

Is the induction correct? (Wondering)