Separably closed fields

Supplements to Mathlib's IsSepClosed and IsSepClosure for domain algebras, quadratics, and towers of field extensions.

Separable elements in domain algebras

A separable element of an algebra over a separably closed field belongs to the image of that field when the ambient algebra is a domain. The algebra can be noncommutative, and no algebraicity or separability assumption is needed on its other elements.

Quadratics over a separably closed field

A separably closed field solves every quadratic except the inseparable ones. A quadratic a X² + b X + c with a ≠ 0 is inseparable exactly when its derivative 2a X + b vanishes, that is when 2 = 0 and b = 0; away from that case the equation has a root in the field itself.

Both halves are already available. Where 2 ≠ 0 the quadratic formula applies as soon as the discriminant is a square, and a separably closed field supplies square roots (IsSepClosed.exists_eq_mul_self). Where 2 = 0 the polynomial a X² + b X + c with b ≠ 0 is separable, and IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C is exactly that case.

The excluded case is genuinely excluded: over an imperfect separably closed field of characteristic 2, such as the separable closure of 𝔽₂(t), the equation X² = t has no solution.

Separable closures in a tower

A separable closure of K is a separable closure of every intermediate extension L of the tower K ⊆ L ⊆ E: separable closedness is a property of the field E alone, and an element separable over K is separable over L. Mathlib records IsSepClosure only for the base of a tower, so this file supplies the step up the tower.

The statement is a theorem rather than an instance because the base field K does not appear in its conclusion, so instance search could not find it.

Main results

• IsSeparable.mem_bot_of_isSepClosed: a separable element of a domain algebra belongs to the bottom subalgebra.
• TauCeti.exists_quadratic_eq_zero_of_isSepClosed
• TauCeti.isSepClosure_tower_top: IsSepClosure K E implies IsSepClosure L E for every intermediate extension L.

theorem IsSeparable.mem_bot_of_isSepClosed {K : Type u_1} {A : Type u_2} [Field K] [IsSepClosed K] [Ring A] [IsDomain A] [Algebra K A] {x : A} (hx : IsSeparable K x) : x ∈ ⊥

A separable element of a domain algebra over a separably closed field belongs to the image of the base field.

theorem TauCeti.exists_quadratic_eq_zero_of_isSepClosed {K : Type u_1} [Field K] [IsSepClosed K] {a : K} (ha : a ≠ 0) (b c : K) (h : 2 ≠ 0 ∨ b ≠ 0) : ∃ (x : K), a * (x * x) + b * x + c = 0

A quadratic with a nonvanishing derivative has a root in a separably closed field. The derivative of a X² + b X + c is 2a X + b, so the hypothesis 2 ≠ 0 ∨ b ≠ 0 says exactly that the quadratic is separable; without it the equation can be X² = t for a non-square t, which has no solution over an imperfect separably closed field of characteristic 2.

theorem TauCeti.isSepClosure_tower_top (K : Type u_1) (L : Type u_2) (E : Type u_3) [Field K] [Field L] [Field E] [Algebra K L] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [IsSepClosure K E] : IsSepClosure L E

A separable closure of K is a separable closure of every intermediate extension L: separable closedness is a property of the field alone, and separability over K implies separability over L.