The Stacks project

Proof. Assume $|\text{Aut}(E/F)| = [E : F]$. By Lemma 9.15.9 this implies that $E/F$ is separable and normal, hence Galois. Conversely, if $E/F$ is separable then $[E : F] = [E : F]_ s$ and if $E/F$ is in addition normal, then Lemma 9.15.9 implies that $|\text{Aut}(E/F)| = [E : F]$. $\square$

Proof. Combine Lemmas 9.15.2 and 9.12.3. $\square$

Proof. The subextension $M/M_{sep}/K$ of Lemma 9.14.6 is normal by Lemma 9.15.4. Since $L/K$ is separable we have $L \subset M_{sep}$. By minimality $M = M_{sep}$ and the proof is done. $\square$

Proof. Given $\alpha \in K$ consider the orbit $G \cdot \alpha \subset K$ of $\alpha $ under the group action. Consider the polynomial

The key to the whole lemma is that this polynomial is invariant under the action of $G$ and hence has coefficients in $K^ G$. Namely, for $\tau \in G$ we have

because the map $\beta \mapsto \tau (\beta )$ is a permutation of the orbit $G \cdot \alpha $. Thus $P \in K^ G[x]$. Since also $P(\alpha ) = 0$ as $\alpha $ is an element of its orbit we conclude that the extension $K/K^ G$ is algebraic. Moreover, the minimal polynomial $Q$ of $\alpha $ over $K^ G$ divides the polynomial $P$ just constructed. Hence $Q$ is separable (by Lemma 9.12.4 for example) and we conclude that $K/K^ G$ is separable. Thus $K/K^ G$ is Galois. To finish the proof it suffices to show that $[K : K^ G] = |G|$ since then $G$ will be the Galois group by Lemma 9.21.2.

Pick finitely many elements $\alpha _ i \in K$, $i = 1, \ldots , n$ such that $\sigma (\alpha _ i) = \alpha _ i$ for $i = 1, \ldots , n$ implies $\sigma $ is the neutral element of $G$. Set

and observe that the action of $G$ on $K$ induces an action of $G$ on $L$. We will show that $L$ has degree $|G|$ over $K^ G$. This will finish the proof, since if $L \subset K$ is proper, then we can add an element $\alpha \in K$, $\alpha \not\in L$ to our list of elements $\alpha _1, \ldots , \alpha _ n$ without increasing $L$ which is absurd. This reduces us to the case that $K/K^ G$ is finite which is treated in the next paragraph.

Assume $K/K^ G$ is finite. By Lemma 9.19.1 we can find $\alpha \in K$ such that $K = K^ G(\alpha )$. By the construction in the first paragraph of this proof we see that $\alpha $ has degree at most $|G|$ over $K$. However, the degree cannot be less than $|G|$ as $G$ acts faithfully on $K^ G(\alpha ) = L$ by construction and the inequality of Lemma 9.15.9. $\square$

Proof. By Lemma 9.21.4 given a subextension $L/M/K$ the extension $L/M$ is Galois. Of course $L/M$ is also finite (Lemma 9.7.3). Thus $|\text{Gal}(L/M)| = [L : M]$ by Lemma 9.21.2. Conversely, if $H \subset G$ is a finite subgroup, then $[L : L^ H] = |H|$ by Lemma 9.21.6. It follows formally from these two observations that we obtain a bijective correspondence as in the theorem.

If $H \subset G$ is normal, then $L^ H$ is fixed by the action of $G$ and we obtain a canonical map $G/H \to \text{Aut}(L^ H/K)$. This map has to be injective as $\text{Gal}(L/L^ H) = H$. Hence $|G/H| = [L^ H : K]$ and $L^ H$ is Galois by Lemma 9.21.2.

Conversely, assume that $K \subset M \subset L$ with $M/K$ Galois. By Lemma 9.15.7 we see that every element $\tau \in \text{Gal}(L/K)$ induces an element $\tau |_ M \in \text{Gal}(M/K)$. This induces a homomorphism of Galois groups $\text{Gal}(L/K) \to \text{Gal}(M/K)$ whose kernel is $H$. Thus $H$ is a normal subgroup. $\square$

Proof. Namely, by Lemma 9.15.7 we see that every element $\tau \in \text{Gal}(L/K)$ induces an element $\tau |_ M \in \text{Gal}(M/K)$ which gives us the homomorphism on the right. The map on the left identifies the left group with the kernel of the right arrow. The sequence is exact because the sizes of the groups work out correctly by multiplicativity of degrees in towers of finite extensions (Lemma 9.7.7). One can also use Lemma 9.15.7 directly to see that the map on the right is surjective. $\square$