Separability of extensions of prime degree

An extension of fields of prime degree p is separable unless p = 0 in the base field. Indeed the separable degree divides the degree, so it is 1 or p; the value p is separability itself, while the value 1 makes the extension purely inseparable, hence of degree a power of the exponential characteristic — and the prime p is such a power only in characteristic p. In particular a quadratic extension away from characteristic two is separable.

The characteristic-p exception is genuine: over K = 𝔽_p(t) the extension K(t ^ (1 / p)) / K has degree p and is purely inseparable.

Conversely, an inseparable extension of prime degree p contains the p-th power of each of its elements in the base field. Consequently, if L is separable over some simple subextension K⟮t⟯, then L is inseparable of degree p over at most one intermediate field.

Main results

• TauCeti.Algebra.isSeparable_of_finrank_prime
• TauCeti.Algebra.isSeparable_of_finrank_eq_two
• TauCeti.Algebra.isPurelyInseparable_iff_not_isSeparable
• TauCeti.Algebra.pow_finrank_mem_range_algebraMap_of_not_isSeparable
• TauCeti.Algebra.finrank_eq_two_of_not_isSeparable
• TauCeti.IntermediateField.eq_of_finrank_eq_of_not_isSeparable

theorem TauCeti.Algebra.isPurelyInseparable_iff_not_isSeparable {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (hp : Nat.Prime (Module.finrank K L)) : IsPurelyInseparable K L ↔ ¬Algebra.IsSeparable K L

An extension of prime degree is purely inseparable exactly when it is not separable: its separable degree divides its degree, so it is either one or the whole degree.

theorem TauCeti.Algebra.finrank_eq_two_of_not_isSeparable {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (h : Module.finrank K L ≤ 2) (hs : ¬Algebra.IsSeparable K L) : Module.finrank K L = 2

A finite extension of degree at most two that is not separable has degree exactly two.

theorem TauCeti.Algebra.isSeparable_of_finrank_prime {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (hp : Nat.Prime (Module.finrank K L)) (hpK : ↑(Module.finrank K L) ≠ 0) : Algebra.IsSeparable K L

A field extension of prime degree p with p ≠ 0 in the base field is separable.

The hypothesis is the nonvanishing of p in the base field rather than a CharP assumption, so that it transfers along any field extension by injectivity of the structure map.

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) : Algebra.IsSeparable K L

A field extension of degree two with 2 ≠ 0 in the base field is separable.

theorem TauCeti.Algebra.pow_finrank_mem_range_algebraMap_of_not_isSeparable {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (hp : Nat.Prime (Module.finrank K L)) (hs : ¬Algebra.IsSeparable K L) (a : L) : a ^ Module.finrank K L ∈ (algebraMap K L).range

A field extension of prime degree p that is not separable contains the p-th power of each of its elements in the base field: it is purely inseparable of exponent one.

theorem TauCeti.IntermediateField.eq_of_finrank_eq_of_not_isSeparable {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] (t : L) [Algebra.IsSeparable (↥K⟮t⟯) L] {p : ℕ} (hp : Nat.Prime p) {E₁ E₂ : IntermediateField K L} (h₁ : Module.finrank (↥E₁) L = p) (hs₁ : ¬Algebra.IsSeparable (↥E₁) L) (h₂ : Module.finrank (↥E₂) L = p) (hs₂ : ¬Algebra.IsSeparable (↥E₂) L) : E₁ = E₂

Two intermediate fields of prime index p over which L is inseparable coincide, as soon as L is separable over K⟮t⟯ for some t.