Endliche Körpererweiterung/Separables Erzeugendensystem/Separabel/Fakt/Beweis

Wir führen Induktion über den Grad der Körpererweiterung, wobei der Grad ${\displaystyle {}1}$ trivial ist. Es sei ${\displaystyle {}x\in L}$, ${\displaystyle {}x\not \in K}$, mit Minimalpolynom ${\displaystyle {}F\in K[X]}$. Wir betrachten den zugehörigen Zwischenkörper

${\displaystyle {}K\subseteq K[x]\cong K[X]/(F)\subseteq L\,,}$

wobei die Grade mit ${\displaystyle {}d_{1}=\operatorname {grad} _{K}K[x]}$, ${\displaystyle {}d_{2}=\operatorname {grad} _{K[x]}L}$ und mit ${\displaystyle {}d=d_{1}d_{2}=\operatorname {grad} _{K}L}$ bezeichnet seien. Es sei ${\displaystyle {}K\subseteq M}$ ein Körper, über dem ${\displaystyle {}F}$ und die ${\displaystyle {}F_{i}}$ in Linearfaktoren zerfallen. Wir betrachten die Abbildung

${\displaystyle \Psi \colon \operatorname {Hom} _{K}{\left(L,M\right)}\longrightarrow \operatorname {Hom} _{K}{\left(K[x],M\right)},}$

wobei einfach der Definitionsbereich eingeschränkt wird. Nach Fakt gibt es ${\displaystyle {}d}$ verschiedene ${\displaystyle {}K}$-Algebrahomomorphismen von ${\displaystyle {}L}$ nach ${\displaystyle {}M}$. Nach Induktionsvoraussetzung ist ${\displaystyle {}K[x]\subseteq L}$ eine separable Körpererweiterung vom Grad ${\displaystyle {}d_{2}}$ und daher gibt es nach Fakt zu jedem fixierten ${\displaystyle {}K}$-Algebrahomomorphismus von ${\displaystyle {}K[x]}$ nach ${\displaystyle {}M}$ genau ${\displaystyle {}d_{2}}$ ${\displaystyle {}K}$-Algebrahomomorphismen von ${\displaystyle {}L}$ nach ${\displaystyle {}M}$, die diesen Homomorphismus fortsetzen. Die Anzahl der Elemente in den Fasern von ${\displaystyle {}\Psi }$ ist also stets gleich ${\displaystyle {}d_{2}}$ und somit besitzt das Bild ${\displaystyle {}\operatorname {Hom} _{K}{\left(K[x],M\right)}}$ genau ${\displaystyle {}d_{1}}$ Elemente. Also gibt es ${\displaystyle {}d_{1}}$ ${\displaystyle {}K}$-Algebrahomomorphismen von ${\displaystyle {}K[x]\cong K[X]/(F)}$ nach ${\displaystyle {}M}$ und somit ist ${\displaystyle {}F}$, wiederum nach Fakt, ein separables Polynom.