Lemma 9.14.6. Let $E/F$ be an algebraic field extension. There exists a unique subextension $E/E_{sep}/F$ such that $E_{sep}/F$ is separable and $E/E_{sep}$ is purely inseparable.
Any algebraic field extension is uniquely a separable field extension followed by a purely inseparable one.
Proof. If the characteristic is zero we set $E_{sep} = E$. Assume the characteristic is $p > 0$. Let $E_{sep}$ be the set of elements of $E$ which are separable over $F$. This is a subextension by Lemma 9.12.13 and of course $E_{sep}$ is separable over $F$. Given an $\alpha $ in $E$ there exists a $p$-power $q$ such that $\alpha ^ q$ is separable over $F$. Namely, $q$ is that power of $p$ such that the minimal polynomial of $\alpha $ is of the form $P(x^ q)$ with $P$ separable algebraic, see Lemma 9.12.1. Hence $E/E_{sep}$ is purely inseparable. Uniqueness is clear. $\square$
Comments (3)
Comment #826 by Johan Commelin on
Comment #5488 by Théo de Oliveira Santos on
Comment #5697 by Johan on
There are also: