Separably Closed Field

In this file we define the typeclass for separably closed fields and separable closures, and prove some of their properties.

Main Definitions

• IsSepClosed k is the typeclass saying k is a separably closed field, i.e. every separable polynomial in k splits.

• IsSepClosure k K is the typeclass saying K is a separable closure of k, where k is a field. This means that K is separably closed and separable over k.

• IsSepClosed.lift is a map from a separable extension L of K, into any separably closed extension M of K.

• IsSepClosure.equiv is a proof that any two separable closures of the same field are isomorphic.

• IsSepClosure.isAlgClosure_of_perfectField, IsSepClosure.of_isAlgClosure_of_perfectField: if k is a perfect field, then its separable closure coincides with its algebraic closure.

Tags

separable closure, separably closed

Related

• separableClosure: maximal separable subextension of K/k, consisting of all elements of K which are separable over k.

• separableClosure.isSepClosure: if K is a separably closed field containing k, then the maximal separable subextension of K/k is a separable closure of k.

• In particular, a separable closure (SeparableClosure) exists.

• Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed: an algebraic extension of a separably closed field is purely inseparable.

class IsSepClosed (k : Type u) [Field k] : Prop

Typeclass for separably closed fields.

To show Polynomial.Splits p f for an arbitrary ring homomorphism f, see IsSepClosed.splits_codomain and IsSepClosed.splits_domain.

• splits_of_separable (p : Polynomial k) : p.Separable → Polynomial.Splits (RingHom.id k) p

instance IsSepClosed.of_isAlgClosed (k : Type u) [Field k] [IsAlgClosed k] : IsSepClosed k

An algebraically closed field is also separably closed.

theorem IsSepClosed.splits_codomain {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed K] {f : k →+* K} (p : Polynomial k) (h : p.Separable) : Polynomial.Splits f p

Every separable polynomial splits in the field extension f : k →+* K if K is separably closed.

See also IsSepClosed.splits_domain for the case where k is separably closed.

theorem IsSepClosed.splits_domain {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed k] {f : k →+* K} (p : Polynomial k) (h : p.Separable) : Polynomial.Splits f p

Every separable polynomial splits in the field extension f : k →+* K if k is separably closed.

See also IsSepClosed.splits_codomain for the case where k is separably closed.

theorem IsSepClosed.exists_root {k : Type u} [Field k] [IsSepClosed k] (p : Polynomial k) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ (x : k), p.IsRoot x

theorem IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C {k : Type u} [Field k] [IsSepClosed k] {n : ℕ} (a b c : k) (hn : ↑n = 0) (hn' : 2 ≤ n) (hb : b ≠ 0) : ∃ (x : k), a * x ^ n + b * x + c = 0

If n ≥ 2 equals zero in a separably closed field k, b ≠ 0, then there exists x in k such that a * x ^ n + b * x + c = 0.

theorem IsSepClosed.exists_root_C_mul_X_pow_add_C_mul_X_add_C' {k : Type u} [Field k] [IsSepClosed k] (p n : ℕ) (a b c : k) [CharP k p] (hn : p ∣ n) (hn' : 2 ≤ n) (hb : b ≠ 0) : ∃ (x : k), a * x ^ n + b * x + c = 0

If a separably closed field k is of characteristic p, n ≥ 2 is such that p ∣ n, b ≠ 0, then there exists x in k such that a * x ^ n + b * x + c = 0.

@[instance 100]

instance IsSepClosed.isAlgClosed_of_perfectField (k : Type u) [Field k] [IsSepClosed k] [PerfectField k] : IsAlgClosed k

A separably closed perfect field is also algebraically closed.

theorem IsSepClosed.exists_pow_nat_eq {k : Type u} [Field k] [IsSepClosed k] (x : k) (n : ℕ) [hn : NeZero ↑n] : ∃ (z : k), z ^ n = x

theorem IsSepClosed.exists_eq_mul_self {k : Type u} [Field k] [IsSepClosed k] (x : k) [h2 : NeZero 2] : ∃ (z : k), x = z * z

theorem IsSepClosed.roots_eq_zero_iff {k : Type u} [Field k] [IsSepClosed k] {p : Polynomial k} (hsep : p.Separable) : p.roots = 0 ↔ p = Polynomial.C (p.coeff 0)

theorem IsSepClosed.exists_eval₂_eq_zero {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed K] (f : k →+* K) (p : Polynomial k) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ (x : K), Polynomial.eval₂ f x p = 0

theorem IsSepClosed.exists_aeval_eq_zero {k : Type u} [Field k] (K : Type v) [Field K] [IsSepClosed K] [Algebra k K] (p : Polynomial k) (hp : p.degree ≠ 0) (hsep : p.Separable) : ∃ (x : K), (Polynomial.aeval x) p = 0

theorem IsSepClosed.of_exists_root (k : Type u) [Field k] (H : ∀ (p : Polynomial k), p.Monic → Irreducible p → p.Separable → ∃ (x : k), Polynomial.eval x p = 0) : IsSepClosed k

theorem IsSepClosed.degree_eq_one_of_irreducible (k : Type u) [Field k] [IsSepClosed k] {p : Polynomial k} (hp : Irreducible p) (hsep : p.Separable) : p.degree = 1

theorem IsSepClosed.algebraMap_surjective (k : Type u) [Field k] (K : Type v) [Field K] [IsSepClosed k] [Algebra k K] [Algebra.IsSeparable k K] : Function.Surjective ⇑(algebraMap k K)

theorem IntermediateField.eq_bot_of_isSepClosed_of_isSeparable {k : Type u} [Field k] {K : Type v} [Field K] [IsSepClosed k] [Algebra k K] (L : IntermediateField k K) [Algebra.IsSeparable k ↥L] : L = ⊥

If k is separably closed, K / k is a field extension, L / k is an intermediate field which is separable, then L is equal to k. A corollary of IsSepClosed.algebraMap_surjective.

class IsSepClosure (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] : Prop

Typeclass for an extension being a separable closure.

• sep_closed : IsSepClosed K
• separable : Algebra.IsSeparable k K

instance IsSepClosure.self_of_isSepClosed (k : Type u) [Field k] [IsSepClosed k] : IsSepClosure k k

A separably closed field is its separable closure.

@[instance 100]

instance IsSepClosure.isAlgClosure_of_perfectField_top (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] [IsSepClosure k K] [PerfectField K] : IsAlgClosure k K

If K is perfect and is a separable closure of k, then it is also an algebraic closure of k.

@[instance 100]

instance IsSepClosure.isAlgClosure_of_perfectField (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] [IsSepClosure k K] [PerfectField k] : IsAlgClosure k K

If k is perfect, K is a separable closure of k, then it is also an algebraic closure of k.

@[instance 100]

instance IsSepClosure.of_isAlgClosure_of_perfectField (k : Type u) [Field k] (K : Type v) [Field K] [Algebra k K] [IsAlgClosure k K] [PerfectField k] : IsSepClosure k K

If k is perfect, K is an algebraic closure of k, then it is also a separable closure of k.

theorem isSepClosure_iff {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] : IsSepClosure k K ↔ IsSepClosed K ∧ Algebra.IsSeparable k K

instance IsSepClosure.isSeparable {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] [IsSepClosure k K] : Algebra.IsSeparable k K

@[instance 100]

instance IsSepClosure.isGalois {k : Type u} [Field k] {K : Type v} [Field K] [Algebra k K] [IsSepClosure k K] : IsGalois k K

theorem IsSepClosed.surjective_restrictDomain_of_isSeparable {K : Type u} (L : Type v) {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsSepClosed M] {E : Type u_1} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsSeparable L E] : Function.Surjective fun (φ : E →ₐ[K] M) => AlgHom.restrictDomain L φ

@[deprecated IsSepClosed.surjective_restrictDomain_of_isSeparable (since := "2024-11-15")]

theorem IsSepClosed.surjective_comp_algebraMap_of_isSeparable {K : Type u} (L : Type v) {M : Type w} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsSepClosed M] {E : Type u_1} [Field E] [Algebra K E] [Algebra L E] [IsScalarTower K L E] [Algebra.IsSeparable L E] : Function.Surjective fun (φ : E →ₐ[K] M) => AlgHom.restrictDomain L φ

Alias of IsSepClosed.surjective_restrictDomain_of_isSeparable.

theorem IsSepClosed.lift_def {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsSepClosed M] [Algebra.IsSeparable K L] : lift = Classical.choice ⋯

@[irreducible]

noncomputable def IsSepClosed.lift {K : Type u_1} {L : Type u_2} {M : Type u_3} [Field K] [Field L] [Algebra K L] [Field M] [Algebra K M] [IsSepClosed M] [Algebra.IsSeparable K L] : L →ₐ[K] M

A (random) homomorphism from a separable extension L of K into a separably closed extension M of K.

Equations

• IsSepClosed.lift = Classical.choice ⋯

noncomputable def IsSepClosure.equiv (K : Type u) [Field K] (L : Type v) (M : Type w) [Field L] [Field M] [Algebra K M] [IsSepClosure K M] [Algebra K L] [IsSepClosure K L] : L ≃ₐ[K] M

A (random) isomorphism between two separable closures of K.

Equations

• IsSepClosure.equiv K L M = AlgEquiv.ofBijective IsSepClosed.lift ⋯