Field extension over a fixed field has smaller or equal degree than the size of the automorphism group
问题内容
Let $F/K$ be a finite field extension, $G=\text{Aut}_K(F)$ be the group of automorphisms of $F$ that fix elements of $K$, and $F^G$ be the fixed field of $G$. We then have $$[F:F^G]\le |G|.$$
This is proven in Hungerford Chapter V, Lemma 2.9. Hungerford used this lemma to prove "$F^G=K$ iff $[F:K]=|G|$" in Galois theory. This lemma has a long and hard proof, in my opinion. Indeed, we have the following tower of inequalities:
$$[F:F^G] \le |G| \le [F:K]_s \le [F:K],$$ where $[F:K]_s$ means seperable defree of $F$ over $K$. The hardest part of this tower to prove is $[F:F^G] \le |G|$.
To prove Galois theory or Galois correspondence, some other authors like Lang take a different approach that does not involve such a lemma or inequality. Now, I am wondering whether we can conclude $[F:F^G] \le |G|$ from Galois theory.
If we know the Galois correspondence and the fact that $F^G=K$ iff $[F:K]=|G|$, then can we conclude $[F:F^G] \le |G|$ in general for finite extensions, or do we again require a similar proof of Lemma 2.9 in Hungerford?
Added Later
Let me elaborate more. How do you prove $[F:F^{\text{Aut}_K(F)}]<|\text{Aut}_K(F)|$ when $K^{\text{Aut}_K(F)}\ne K$? In this situation, it is easy to show $$[F:F^{\text{Aut}_K(F)}]<[F:K]$$ because $K \subset\text{Aut}_K(F)$, but how do you show $$[F:F^{\text{Aut}_K(F)}]<|\text{Aut}_K(F)|<[F:K]?$$
回答 (1)
The fact about Galois correspondence that you want to assume is
Fact. Let $F/L$ be a finite field extension, $\DeclareMathOperator\aut{Aut}G=\aut_L(F)$ be the group of automorphisms of $F$ that fix elements of $L$, and $F^G$ be the fixed field of $G$. Then $$F^G=L\iff[F:L]=|G|.$$
(I have deliberately renamed $K$ to $L$ to avoid confusion.)
The conclusion you want to prove is
Let $F/K$ be a finite field extension, and $G=\aut_K(F)$. Then $$[F:F^G]\le|G|.$$
This follows immediately from the Fact by taking the same $F$ and $G$, and $L=F^G$. The assumptions are satisfied as $F/L$ is a finite extension and $$G=\aut_L(F):$$ we have $G\subseteq\aut_L(F)$ as all elements of $G$ fix $L=F^G$ by the definition of $F^G$, and $G=\aut_K(F)\supseteq\aut_L(F)$ as $K\subseteq L$. Thus, the Fact gives $$[F:F^G]=[F:L]=|G|.$$