Purely inseparable extension and relative perfect closure

This file contains basics about purely inseparable extensions and the relative perfect closure of fields.

Main definitions

• IsPurelyInseparable: typeclass for purely inseparable field extensions: an algebraic extension E / F is purely inseparable if and only if the minimal polynomial of every element of E ∖ F is not separable.

• perfectClosure: the relative perfect closure of F in E, it consists of the elements x of E such that there exists a natural number n such that x ^ (ringExpChar F) ^ n is contained in F, where ringExpChar F is the exponential characteristic of F. It is also the maximal purely inseparable subextension of E / F (le_perfectClosure_iff).

Main results

• IsPurelyInseparable.surjective_algebraMap_of_isSeparable, IsPurelyInseparable.bijective_algebraMap_of_isSeparable, IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable: if E / F is both purely inseparable and separable, then algebraMap F E is surjective (hence bijective). In particular, if an intermediate field of E / F is both purely inseparable and separable, then it is equal to F.

• isPurelyInseparable_iff_pow_mem: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, there exists a natural number n such that x ^ (q ^ n) is contained in F.

• IsPurelyInseparable.trans: if E / F and K / E are both purely inseparable extensions, then K / F is also purely inseparable.

• isPurelyInseparable_iff_natSepDegree_eq_one: E / F is purely inseparable if and only if for every element x of E, its minimal polynomial has separable degree one.

• isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form X ^ (q ^ n) - y for some natural number n and some element y of F.

• isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow: a field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form (X - x) ^ (q ^ n) for some natural number n.

• isPurelyInseparable_iff_finSepDegree_eq_one: an algebraic extension is purely inseparable if and only if it has finite separable degree (Field.finSepDegree) one.

  TODO: remove the algebraic assumption.

• IsPurelyInseparable.normal: a purely inseparable extension is normal.

• separableClosure.isPurelyInseparable: if E / F is algebraic, then E is purely inseparable over the separable closure of F in E.

• separableClosure_le_iff: if E / F is algebraic, then an intermediate field of E / F contains the separable closure of F in E if and only if E is purely inseparable over it.

• eq_separableClosure_iff: if E / F is algebraic, then an intermediate field of E / F is equal to the separable closure of F in E if and only if it is separable over F, and E is purely inseparable over it.

• le_perfectClosure_iff: an intermediate field of E / F is contained in the relative perfect closure of F in E if and only if it is purely inseparable over F.

• perfectClosure.perfectRing, perfectClosure.perfectField: if E is a perfect field, then the (relative) perfect closure perfectClosure F E is perfect.

• IsPurelyInseparable.injective_comp_algebraMap: if E / F is purely inseparable, then for any reduced ring L, the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective. In particular, a purely inseparable field extension is an epimorphism in the category of fields.

• IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem: if F is of exponential characteristic q, then F(S) / F is a purely inseparable extension if and only if for any x ∈ S, x ^ (q ^ n) is contained in F for some n : ℕ.

• Field.finSepDegree_eq: if E / F is algebraic, then the Field.finSepDegree F E is equal to Field.sepDegree F E as a natural number. This means that the cardinality of Field.Emb F E and the degree of (separableClosure F E) / F are both finite or infinite, and when they are finite, they coincide.

• Field.finSepDegree_mul_finInsepDegree: the finite separable degree multiply by the finite inseparable degree is equal to the (finite) field extension degree.

• Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic: the separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$.

• IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable, IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable': if K / E / F is a field extension tower, such that E / F is purely inseparable, then for any subset S of K such that F(S) / F is algebraic, the E(S) / E and F(S) / F have the same separable degree. In particular, if S is an intermediate field of K / F such that S / F is algebraic, the E(S) / E and S / F have the same separable degree.

• minpoly.map_eq_of_separable_of_isPurelyInseparable: if K / E / F is a field extension tower, such that E / F is purely inseparable, then for any element x of K separable over F, it has the same minimal polynomials over F and over E.

• Polynomial.Separable.map_irreducible_of_isPurelyInseparable: if E / F is purely inseparable, f is a separable irreducible polynomial over F, then it is also irreducible over E.

Tags

separable degree, degree, separable closure, purely inseparable

TODO

• IsPurelyInseparable.of_injective_comp_algebraMap: if L is an algebraically closed field containing E, such that the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective, then E / F is purely inseparable. As a corollary, epimorphisms in the category of fields must be purely inseparable extensions. Need to use the fact that Emb F E is infinite (or just not a singleton) when E / F is (purely) transcendental.

• Restate some intermediate result in terms of linearly disjointness.

• Prove that the inseparable degrees satisfy the tower law: $[E:F]_i [K:E]_i = [K:F]_i$. Probably an argument using linearly disjointness is needed.

class IsPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Prop

Typeclass for purely inseparable field extensions: an algebraic extension E / F is purely inseparable if and only if the minimal polynomial of every element of E ∖ F is not separable.

• isIntegral' : ∀ (x : E), IsIntegral F x
• inseparable' : ∀ (x : E), Polynomial.Separable (minpoly F x) → x ∈ RingHom.range (algebraMap F E)

theorem IsPurelyInseparable.isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Algebra.IsAlgebraic F E

theorem IsPurelyInseparable.isIntegral (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Algebra.IsIntegral F E

theorem IsPurelyInseparable.inseparable (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (x : E) : Polynomial.Separable (minpoly F x) → x ∈ RingHom.range (algebraMap F E)

theorem isPurelyInseparable_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F E ↔ ∀ (x : E), IsIntegral F x ∧ (Polynomial.Separable (minpoly F x) → x ∈ RingHom.range (algebraMap F E))

theorem AlgEquiv.isPurelyInseparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (e : K ≃ₐ[F] E) [IsPurelyInseparable F K] : IsPurelyInseparable F E

Transfer IsPurelyInseparable across an AlgEquiv.

theorem AlgEquiv.isPurelyInseparable_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (e : K ≃ₐ[F] E) : IsPurelyInseparable F K ↔ IsPurelyInseparable F E

theorem Algebra.IsAlgebraic.isPurelyInseparable_of_isSepClosed {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) [IsSepClosed F] : IsPurelyInseparable F E

If E / F is an algebraic extension, F is separably closed, then E / F is purely inseparable.

theorem IsPurelyInseparable.surjective_algebraMap_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] [IsSeparable F E] : Function.Surjective ⇑(algebraMap F E)

If E / F is both purely inseparable and separable, then algebraMap F E is surjective.

theorem IsPurelyInseparable.bijective_algebraMap_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] [IsSeparable F E] : Function.Bijective ⇑(algebraMap F E)

If E / F is both purely inseparable and separable, then algebraMap F E is bijective.

theorem IntermediateField.eq_bot_of_isPurelyInseparable_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [IsPurelyInseparable F ↥L] [IsSeparable F ↥L] : L = ⊥

If an intermediate field of E / F is both purely inseparable and separable, then it is equal to F.

theorem separableClosure.eq_bot_of_isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : separableClosure F E = ⊥

If E / F is purely inseparable, then the separable closure of F in E is equal to F.

theorem separableClosure.eq_bot_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) : separableClosure F E = ⊥ ↔ IsPurelyInseparable F E

If E / F is an algebraic extension, then the separable closure of F in E is equal to F if and only if E / F is purely inseparable.

instance isPurelyInseparable_self (F : Type u) [Field F] : IsPurelyInseparable F F

Equations

• ⋯ = ⋯

theorem isPurelyInseparable_iff_pow_mem (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] : IsPurelyInseparable F E ↔ ∀ (x : E), ∃ (n : ℕ), x ^ q ^ n ∈ RingHom.range (algebraMap F E)

A field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, there exists a natural number n such that x ^ (q ^ n) is contained in F.

theorem IsPurelyInseparable.pow_mem (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] (x : E) : ∃ (n : ℕ), x ^ q ^ n ∈ RingHom.range (algebraMap F E)

def perfectClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : IntermediateField F E

The relative perfect closure of F in E, consists of the elements x of E such that there exists a natural number n such that x ^ (ringExpChar F) ^ n is contained in F, where ringExpChar F is the exponential characteristic of F. It is also the maximal purely inseparable subextension of E / F (le_perfectClosure_iff).

Equations

• One or more equations did not get rendered due to their size.

theorem mem_perfectClosure_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} : x ∈ perfectClosure F E ↔ ∃ (n : ℕ), x ^ ringExpChar F ^ n ∈ RingHom.range (algebraMap F E)

theorem mem_perfectClosure_iff_pow_mem {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] {x : E} : x ∈ perfectClosure F E ↔ ∃ (n : ℕ), x ^ q ^ n ∈ RingHom.range (algebraMap F E)

theorem mem_perfectClosure_iff_natSepDegree_eq_one {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} : x ∈ perfectClosure F E ↔ Polynomial.natSepDegree (minpoly F x) = 1

An element is contained in the relative perfect closure if and only if its mininal polynomial has separable degree one.

theorem isPurelyInseparable_iff_perfectClosure_eq_top {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F E ↔ perfectClosure F E = ⊤

A field extension E / F is purely inseparable if and only if the relative perfect closure of F in E is equal to E.

instance perfectClosure.isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F ↥(perfectClosure F E)

The relative perfect closure of F in E is purely inseparable over F.

Equations

• ⋯ = ⋯

theorem perfectClosure.isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Algebra.IsAlgebraic F ↥(perfectClosure F E)

The relative perfect closure of F in E is algebraic over F.

theorem perfectClosure.eq_bot_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSeparable F E] : perfectClosure F E = ⊥

If E / F is separable, then the perfect closure of F in E is equal to F. Note that the converse is not necessarily true (see https://math.stackexchange.com/a/3009197) even when E / F is algebraic.

theorem le_perfectClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [h : IsPurelyInseparable F ↥L] : L ≤ perfectClosure F E

An intermediate field of E / F is contained in the relative perfect closure of F in E if it is purely inseparable over F.

theorem le_perfectClosure_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) : L ≤ perfectClosure F E ↔ IsPurelyInseparable F ↥L

An intermediate field of E / F is contained in the relative perfect closure of F in E if and only if it is purely inseparable over F.

theorem separableClosure_inf_perfectClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : separableClosure F E ⊓ perfectClosure F E = ⊥

theorem map_mem_perfectClosure_iff {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) {x : E} : i x ∈ perfectClosure F K ↔ x ∈ perfectClosure F E

If i is an F-algebra homomorphism from E to K, then i x is contained in perfectClosure F K if and only if x is contained in perfectClosure F E.

theorem perfectClosure.comap_eq_of_algHom {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) : IntermediateField.comap i (perfectClosure F K) = perfectClosure F E

If i is an F-algebra homomorphism from E to K, then the preimage of perfectClosure F K under the map i is equal to perfectClosure F E.

theorem perfectClosure.map_le_of_algHom {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E →ₐ[F] K) : IntermediateField.map i (perfectClosure F E) ≤ perfectClosure F K

If i is an F-algebra homomorphism from E to K, then the image of perfectClosure F E under the map i is contained in perfectClosure F K.

theorem perfectClosure.map_eq_of_algEquiv {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) : IntermediateField.map (↑i) (perfectClosure F E) = perfectClosure F K

If i is an F-algebra isomorphism of E and K, then the image of perfectClosure F E under the map i is equal to in perfectClosure F K.

def perfectClosure.algEquivOfAlgEquiv {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) : ↥(perfectClosure F E) ≃ₐ[F] ↥(perfectClosure F K)

If E and K are isomorphic as F-algebras, then perfectClosure F E and perfectClosure F K are also isomorphic as F-algebras.

Equations

• perfectClosure.algEquivOfAlgEquiv i = AlgEquiv.trans (IntermediateField.intermediateFieldMap i (perfectClosure F E)) (IntermediateField.equivOfEq ⋯)

def AlgEquiv.perfectClosure {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] (i : E ≃ₐ[F] K) : ↥(perfectClosure F E) ≃ₐ[F] ↥(perfectClosure F K)

Alias of perfectClosure.algEquivOfAlgEquiv.

---

If E and K are isomorphic as F-algebras, then perfectClosure F E and perfectClosure F K are also isomorphic as F-algebras.

Equations

• @AlgEquiv.perfectClosure = @perfectClosure.algEquivOfAlgEquiv

instance perfectClosure.perfectRing (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (p : ℕ) [ExpChar E p] [PerfectRing E p] : PerfectRing (↥(perfectClosure F E)) p

If E is a perfect field of exponential characteristic p, then the (relative) perfect closure perfectClosure F E is perfect.

Equations

• ⋯ = ⋯

instance perfectClosure.perfectField (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [PerfectField E] : PerfectField ↥(perfectClosure F E)

If E is a perfect field, then the (relative) perfect closure perfectClosure F E is perfect.

Equations

• ⋯ = ⋯

theorem IsPurelyInseparable.tower_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F K] : IsPurelyInseparable F E

If K / E / F is a field extension tower such that K / F is purely inseparable, then E / F is also purely inseparable.

theorem IsPurelyInseparable.tower_top (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [h : IsPurelyInseparable F K] : IsPurelyInseparable E K

If K / E / F is a field extension tower such that K / F is purely inseparable, then K / E is also purely inseparable.

theorem IsPurelyInseparable.trans (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [h1 : IsPurelyInseparable F E] [h2 : IsPurelyInseparable E K] : IsPurelyInseparable F K

If E / F and K / E are both purely inseparable extensions, then K / F is also purely inseparable.

theorem isPurelyInseparable_iff_natSepDegree_eq_one (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F E ↔ ∀ (x : E), Polynomial.natSepDegree (minpoly F x) = 1

A field extension E / F is purely inseparable if and only if for every element x of E, its minimal polynomial has separable degree one.

theorem IsPurelyInseparable.natSepDegree_eq_one (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (x : E) : Polynomial.natSepDegree (minpoly F x) = 1

theorem isPurelyInseparable_iff_minpoly_eq_X_pow_sub_C (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] : IsPurelyInseparable F E ↔ ∀ (x : E), ∃ (n : ℕ) (y : F), minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y

A field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form X ^ (q ^ n) - y for some natural number n and some element y of F.

theorem IsPurelyInseparable.minpoly_eq_X_pow_sub_C (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] (x : E) : ∃ (n : ℕ) (y : F), minpoly F x = Polynomial.X ^ q ^ n - Polynomial.C y

theorem isPurelyInseparable_iff_minpoly_eq_X_sub_C_pow (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] : IsPurelyInseparable F E ↔ ∀ (x : E), ∃ (n : ℕ), Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n

A field extension E / F of exponential characteristic q is purely inseparable if and only if for every element x of E, the minimal polynomial of x over F is of form (X - x) ^ (q ^ n) for some natural number n.

theorem IsPurelyInseparable.minpoly_eq_X_sub_C_pow (F : Type u) {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [ExpChar F q] [IsPurelyInseparable F E] (x : E) : ∃ (n : ℕ), Polynomial.map (algebraMap F E) (minpoly F x) = (Polynomial.X - Polynomial.C x) ^ q ^ n

theorem isPurelyInseparable_of_finSepDegree_eq_one {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) (hdeg : Field.finSepDegree F E = 1) : IsPurelyInseparable F E

If an algebraic extension has finite separable degree one, then it is purely inseparable.

theorem IsPurelyInseparable.injective_comp_algebraMap (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type w) [CommRing L] [IsReduced L] : Function.Injective fun (f : E →+* L) => RingHom.comp f (algebraMap F E)

If E / F is purely inseparable, then for any reduced ring L, the map (E →+* L) → (F →+* L) induced by algebraMap F E is injective. In particular, a purely inseparable field extension is an epimorphism in the category of fields.

instance instSubsingletonAlgHomOfIsPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type w) [CommRing L] [IsReduced L] [Algebra F L] : Subsingleton (E →ₐ[F] L)

If E / F is purely inseparable, then for any reduced F-algebra L, there exists at most one F-algebra homomorphism from E to L.

Equations

• ⋯ = ⋯

instance instUniqueAlgHomOfIsPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] (L : Type w) [CommRing L] [IsReduced L] [Algebra F L] [Algebra E L] [IsScalarTower F E L] : Unique (E →ₐ[F] L)

Equations

• instUniqueAlgHomOfIsPurelyInseparable F E L = uniqueOfSubsingleton (IsScalarTower.toAlgHom F E L)

instance instUniqueEmbOfIsPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Unique (Field.Emb F E)

If E / F is purely inseparable, then Field.Emb F E has exactly one element.

Equations

• instUniqueEmbOfIsPurelyInseparable F E = instUniqueAlgHomOfIsPurelyInseparable F E (AlgebraicClosure E)

theorem IsPurelyInseparable.finSepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.finSepDegree F E = 1

A purely inseparable extension has finite separable degree one.

theorem IsPurelyInseparable.sepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.sepDegree F E = 1

A purely inseparable extension has separable degree one.

theorem IsPurelyInseparable.insepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.insepDegree F E = Module.rank F E

A purely inseparable extension has inseparable degree equal to degree.

theorem IsPurelyInseparable.finInsepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Field.finInsepDegree F E = FiniteDimensional.finrank F E

A purely inseparable extension has finite inseparable degree equal to degree.

theorem isPurelyInseparable_iff_finSepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) : IsPurelyInseparable F E ↔ Field.finSepDegree F E = 1

An algebraic extension is purely inseparable if and only if it has finite separable degree one.

theorem isPurelyInseparable_iff_fd_isPurelyInseparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) : IsPurelyInseparable F E ↔ ∀ (L : IntermediateField F E), FiniteDimensional F ↥L → IsPurelyInseparable F ↥L

An algebraic extension is purely inseparable if and only if all of its finite dimensional subextensions are purely inseparable.

instance IsPurelyInseparable.normal (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsPurelyInseparable F E] : Normal F E

A purely inseparable extension is normal.

Equations

• ⋯ = ⋯

theorem separableClosure.isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) : IsPurelyInseparable (↥(separableClosure F E)) E

If E / F is algebraic, then E is purely inseparable over the separable closure of F in E.

theorem separableClosure_le (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [h : IsPurelyInseparable (↥L) E] : separableClosure F E ≤ L

An intermediate field of E / F contains the separable closure of F in E if E is purely inseparable over it.

theorem separableClosure_le_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) (L : IntermediateField F E) : separableClosure F E ≤ L ↔ IsPurelyInseparable (↥L) E

If E / F is algebraic, then an intermediate field of E / F contains the separable closure of F in E if and only if E is purely inseparable over it.

theorem eq_separableClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L : IntermediateField F E) [IsSeparable F ↥L] [IsPurelyInseparable (↥L) E] : L = separableClosure F E

If an intermediate field of E / F is separable over F, and E is purely inseparable over it, then it is equal to the separable closure of F in E.

theorem eq_separableClosure_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) (L : IntermediateField F E) : L = separableClosure F E ↔ IsSeparable F ↥L ∧ IsPurelyInseparable (↥L) E

If E / F is algebraic, then an intermediate field of E / F is equal to the separable closure of F in E if and only if it is separable over F, and E is purely inseparable over it.

instance IntermediateField.isPurelyInseparable_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : IsPurelyInseparable F ↥⊥

Equations

• ⋯ = ⋯

theorem IntermediateField.isPurelyInseparable_adjoin_simple_iff_natSepDegree_eq_one (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {x : E} : IsPurelyInseparable F ↥F⟮x⟯ ↔ Polynomial.natSepDegree (minpoly F x) = 1

F⟮x⟯ / F is a purely inseparable extension if and only if the mininal polynomial of x has separable degree one.

theorem IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {x : E} : IsPurelyInseparable F ↥F⟮x⟯ ↔ ∃ (n : ℕ), x ^ q ^ n ∈ RingHom.range (algebraMap F E)

If F is of exponential characteristic q, then F⟮x⟯ / F is a purely inseparable extension if and only if x ^ (q ^ n) is contained in F for some n : ℕ.

theorem IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {S : Set E} : IsPurelyInseparable F ↥(IntermediateField.adjoin F S) ↔ ∀ x ∈ S, ∃ (n : ℕ), x ^ q ^ n ∈ RingHom.range (algebraMap F E)

If F is of exponential characteristic q, then F(S) / F is a purely inseparable extension if and only if for any x ∈ S, x ^ (q ^ n) is contained in F for some n : ℕ.

instance IntermediateField.isPurelyInseparable_sup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (L1 : IntermediateField F E) (L2 : IntermediateField F E) [h1 : IsPurelyInseparable F ↥L1] [h2 : IsPurelyInseparable F ↥L2] : IsPurelyInseparable F ↥(L1 ⊔ L2)

A compositum of two purely inseparable extensions is purely inseparable.

Equations

• ⋯ = ⋯

instance IntermediateField.isPurelyInseparable_iSup (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {ι : Sort u_1} {t : ι → IntermediateField F E} [h : ∀ (i : ι), IsPurelyInseparable F ↥(t i)] : IsPurelyInseparable F ↥(⨆ (i : ι), t i)

A compositum of purely inseparable extensions is purely inseparable.

Equations

• ⋯ = ⋯

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (S : Set E) [IsSeparable F ↥(IntermediateField.adjoin F S)] (q : ℕ) [ExpChar F q] (n : ℕ) : IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun (x : E) => x ^ q ^ n) '' S)

If F is a field of exponential characteristic q, F(S) / F is separable, then F(S) = F(S ^ (q ^ n)) for any natural number n.

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_pow_of_isSeparable' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSeparable F E] (S : Set E) (q : ℕ) [ExpChar F q] (n : ℕ) : IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun (x : E) => x ^ q ^ n) '' S)

If E / F is a separable field extension of exponential characteristic q, then F(S) = F(S ^ (q ^ n)) for any subset S of E and any natural number n.

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (S : Set E) [IsSeparable F ↥(IntermediateField.adjoin F S)] (q : ℕ) [ExpChar F q] : IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun (x : E) => x ^ q) '' S)

If F is a field of exponential characteristic q, F(S) / F is separable, then F(S) = F(S ^ q).

theorem IntermediateField.adjoin_eq_adjoin_pow_expChar_of_isSeparable' (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSeparable F E] (S : Set E) (q : ℕ) [ExpChar F q] : IntermediateField.adjoin F S = IntermediateField.adjoin F ((fun (x : E) => x ^ q) '' S)

If E / F is a separable field extension of exponential characteristic q, then F(S) = F(S ^ q) for any subset S of E.

theorem Field.span_map_pow_expChar_pow_eq_top_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) (n : ℕ) [hF : ExpChar F q] {ι : Type u_1} {v : ι → E} [IsSeparable F E] (h : Submodule.span F (Set.range v) = ⊤) : Submodule.span F (Set.range fun (x : ι) => v x ^ q ^ n) = ⊤

If E / F is a separable extension of exponential characteristic q, if { u_i } is a family of elements of E which F-linearly spans E, then { u_i ^ (q ^ n) } also F-linearly spans E for any natural number n.

theorem LinearIndependent.map_pow_expChar_pow_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) (n : ℕ) [hF : ExpChar F q] {ι : Type u_1} {v : ι → E} [IsSeparable F E] (h : LinearIndependent F v) : LinearIndependent F fun (x : ι) => v x ^ q ^ n

If E / F is a separable extension of exponential characteristic q, if { u_i } is a family of elements of E which is F-linearly independent, then { u_i ^ (q ^ n) } is also F-linearly independent for any natural number n.

theorem LinearIndependent.map_pow_expChar_pow_of_separable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) (n : ℕ) [hF : ExpChar F q] {ι : Type u_1} {v : ι → E} (hsep : ∀ (i : ι), Polynomial.Separable (minpoly F (v i))) (h : LinearIndependent F v) : LinearIndependent F fun (x : ι) => v x ^ q ^ n

If E / F is a field extension of exponential characteristic q, if { u_i } is a family of separable elements of E which is F-linearly independent, then { u_i ^ (q ^ n) } is also F-linearly independent for any natural number n.

def Basis.mapPowExpCharPowOfIsSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) (n : ℕ) [hF : ExpChar F q] {ι : Type u_1} [IsSeparable F E] (b : Basis ι F E) : Basis ι F E

If E / F is a separable extension of exponential characteristic q, if { u_i } is an F-basis of E, then { u_i ^ (q ^ n) } is also an F-basis of E for any natural number n.

Equations

• Basis.mapPowExpCharPowOfIsSeparable q n b = Basis.mk ⋯ ⋯

theorem isSepClosed_iff_isPurelyInseparable_algebraicClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsAlgClosure F E] : IsSepClosed F ↔ IsPurelyInseparable F E

If E is an algebraic closure of F, then F is separably closed if and only if E / F is purely inseparable.

theorem Algebra.IsAlgebraic.isSepClosed {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) [IsSepClosed F] : IsSepClosed E

If E / F is an algebraic extension, F is separably closed, then E is also separably closed.

theorem perfectField_of_perfectClosure_eq_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [h : PerfectField E] (eq : perfectClosure F E = ⊥) : PerfectField F

theorem perfectField_of_isSeparable_of_perfectField_top (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSeparable F E] [PerfectField E] : PerfectField F

If E / F is a separable extension, E is perfect, then F is also prefect.

theorem perfectField_iff_isSeparable_algebraicClosure (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsAlgClosure F E] : PerfectField F ↔ IsSeparable F E

If E is an algebraic closure of F, then F is perfect if and only if E / F is separable.

theorem Field.finSepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (halg : Algebra.IsAlgebraic F E) : Field.finSepDegree F E = Cardinal.toNat (Field.sepDegree F E)

If E / F is algebraic, then the Field.finSepDegree F E is equal to Field.sepDegree F E as a natural number. This means that the cardinality of Field.Emb F E and the degree of (separableClosure F E) / F are both finite or infinite, and when they are finite, they coincide.

theorem Field.finSepDegree_mul_finInsepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Field.finSepDegree F E * Field.finInsepDegree F E = FiniteDimensional.finrank F E

The finite separable degree multiply by the finite inseparable degree is equal to the (finite) field extension degree.

theorem separableClosure.adjoin_eq_of_isAlgebraic_of_isSeparable {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (halg : Algebra.IsAlgebraic F E) [IsSeparable E K] : IntermediateField.adjoin E ↑(separableClosure F K) = ⊤

If K / E / F is a field extension tower, such that E / F is algebraic and K / E is separable, then E adjoin separableClosure F K is equal to K. It is a special case of separableClosure.adjoin_eq_of_isAlgebraic, and is an intermediate result used to prove it.

theorem separableClosure.adjoin_eq_of_isAlgebraic {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (halg : Algebra.IsAlgebraic F E) : IntermediateField.adjoin E ↑(separableClosure F K) = separableClosure E K

If K / E / F is a field extension tower, such that E / F is algebraic, then E adjoin separableClosure F K is equal to separableClosure E K.

theorem LinearIndependent.map_of_isPurelyInseparable_of_separable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E] {ι : Type u_1} {v : ι → K} (hsep : ∀ (i : ι), Polynomial.Separable (minpoly F (v i))) (h : LinearIndependent F v) : LinearIndependent E v

If K / E / F is a field extension tower such that E / F is purely inseparable, if { u_i } is a family of separable elements of K which is F-linearly independent, then it is also E-linearly independent.

theorem Field.sepDegree_eq_of_isPurelyInseparable_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E] [IsSeparable E K] : Field.sepDegree F K = Module.rank E K

If K / E / F is a field extension tower, such that E / F is purely inseparable and K / E is separable, then the separable degree of K / F is equal to the degree of K / E. It is a special case of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, and is an intermediate result used to prove it.

theorem Field.lift_rank_mul_lift_sepDegree_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsSeparable F E] : Cardinal.lift.{w, v} (Module.rank F E) * Cardinal.lift.{v, w} (Field.sepDegree E K) = Cardinal.lift.{v, w} (Field.sepDegree F K)

If K / E / F is a field extension tower, such that E / F is separable, then $[E:F] [K:E]_s = [K:F]_s$. It is a special case of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, and is an intermediate result used to prove it.

theorem Field.rank_mul_sepDegree_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsSeparable F E] : Module.rank F E * Field.sepDegree E K = Field.sepDegree F K

The same-universe version of Field.lift_rank_mul_lift_sepDegree_of_isSeparable.

theorem Field.sepDegree_eq_of_isPurelyInseparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E] : Field.sepDegree F K = Field.sepDegree E K

If K / E / F is a field extension tower, such that E / F is purely inseparable, then $[K:F]_s = [K:E]_s$. It is a special case of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, and is an intermediate result used to prove it.

theorem Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (halg : Algebra.IsAlgebraic F E) : Cardinal.lift.{w, v} (Field.sepDegree F E) * Cardinal.lift.{v, w} (Field.sepDegree E K) = Cardinal.lift.{v, w} (Field.sepDegree F K)

If K / E / F is a field extension tower, such that E / F is algebraic, then their separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$.

theorem Field.sepDegree_mul_sepDegree_of_isAlgebraic (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type v) [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (halg : Algebra.IsAlgebraic F E) : Field.sepDegree F E * Field.sepDegree E K = Field.sepDegree F K

The same-universe version of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic.

theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (S : Set K) (halg : Algebra.IsAlgebraic F ↥(IntermediateField.adjoin F S)) [IsPurelyInseparable F E] : Field.sepDegree E ↥(IntermediateField.adjoin E S) = Field.sepDegree F ↥(IntermediateField.adjoin F S)

If K / E / F is a field extension tower, such that E / F is purely inseparable, then for any subset S of K such that F(S) / F is algebraic, the E(S) / E and F(S) / F have the same separable degree.

theorem IntermediateField.sepDegree_adjoin_eq_of_isAlgebraic_of_isPurelyInseparable' {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (S : IntermediateField F K) (halg : Algebra.IsAlgebraic F ↥S) [IsPurelyInseparable F E] : Field.sepDegree E ↥(IntermediateField.adjoin E ↑S) = Field.sepDegree F ↥S

If K / E / F is a field extension tower, such that E / F is purely inseparable, then for any intermediate field S of K / F such that S / F is algebraic, the E(S) / E and S / F have the same separable degree.

theorem minpoly.map_eq_of_separable_of_isPurelyInseparable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {K : Type w} [Field K] [Algebra F K] [Algebra E K] [IsScalarTower F E K] (x : K) (hsep : Polynomial.Separable (minpoly F x)) [IsPurelyInseparable F E] : Polynomial.map (algebraMap F E) (minpoly F x) = minpoly E x

If K / E / F is a field extension tower, such that E / F is purely inseparable, then for any element x of K separable over F, it has the same minimal polynomials over F and over E.

theorem Polynomial.Separable.map_irreducible_of_isPurelyInseparable {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] {f : Polynomial F} (hsep : Polynomial.Separable f) (hirr : Irreducible f) [IsPurelyInseparable F E] : Irreducible (Polynomial.map (algebraMap F E) f)

If E / F is a purely inseparable field extension, f is a separable irreducible polynomial over F, then it is also irreducible over E.