A quadratic extension away from characteristic two is separable #
An extension of fields of degree 2 is separable unless 2 = 0 in the base field. Indeed the
separable degree divides the degree, so it is 1 or 2; the value 2 is separability itself,
while the value 1 makes the extension purely inseparable, hence of degree a power of the
exponential characteristic — and 2 is a power of the exponential characteristic only in
characteristic two.
The characteristic-two exception is genuine: over K = 𝔽₂(t) the extension K(√t) / K has
degree 2 and is purely inseparable.
Main results #
theorem
TauCeti.Algebra.isSeparable_of_finrank_eq_two
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
(h2 : 2 ≠ 0)
(h : Module.finrank K L = 2)
:
A field extension of degree two with 2 ≠ 0 in the base field is separable.
The hypothesis is the nonvanishing of 2 in the base field rather than a CharP assumption, so
that it transfers along any field extension by injectivity of the structure map.