Equivalent characterizations of a finite Galois extension

For the implication from condition 1 to condition 2, choose a finite generating family for $K\mathrm{/}F$. By [L2], normality makes $K$ the splitting field of the product of their distinct minimal polynomials; separability makes each factor separable, so their distinct product is separable. If $K=F$, the empty product $1$ has splitting field $F$.

For the implication from condition 2 to condition 3, let $K$ be the splitting field of the separable $f\in F[x]$. Then $K$ is generated over $F$ by the roots of $f$, and the minimal polynomial of each root divides $f$ and therefore has no repeated root, so every generator is separable over $F$; by [L3], $K\mathrm{/}F$ is separable and the full-degree criterion in the Given gives $[K:F{]}_s=[K:F]$. Every $F$-embedding of $K$ into an algebraic closure permutes the roots of $f$ and hence maps $K$ onto itself, so the $[K:F{]}_s$ embeddings are precisely the elements of $G$ and $\mathrm{\mid }G\mathrm{\mid }=[K:F]$.

For the implication from condition 3 to condition 4, [L1] gives $[K:K^G]=\mathrm{\mid }G\mathrm{\mid }=[K:F]$. Since $F\subseteq K^G\subseteq K$, the tower law forces $[K^G:F]=1$, hence $K^G=F$.

For the implication from condition 4 to condition 1, [L4] makes $G$ finite, so [L1] applies to $H=G$ and gives $[K:K^G]=\mathrm{\mid }G\mathrm{\mid }$; with $K^G=F$ this reads $\mathrm{\mid }G\mathrm{\mid }=[K:F]$. The bound in [L4] then gives $[K:F]=\mathrm{\mid }G\mathrm{\mid }\le [K:F{]}_s\le [K:F]$, so $[K:F{]}_s=[K:F]$ and the full-degree criterion in the Given makes $K\mathrm{/}F$ separable. For $\alpha \in K$, the orbit polynomial $q_{\alpha }(x)={\prod }_{\beta \in G\alpha }(x-\beta )$ has distinct roots in $K$ and coefficients fixed by $G$, hence in $K^G=F$. The minimal polynomial of $\alpha$ divides $q_{\alpha }$, while every orbit element is one of its roots; separability makes $q_{\alpha }$ divide that minimal polynomial. They are therefore equal, so every minimal polynomial over $F$ splits in $K$ and $K\mathrm{/}F$ is normal. This also covers $\alpha =0$ and the degree-one extension.