Separable degree

This file contains basics about the separable degree of a field extension.

Main definitions

• Field.Emb F E: the type of F-algebra homomorphisms from E to the algebraic closure of E (the algebraic closure of F is usually used in the literature, but our definition has the advantage that Field.Emb F E lies in the same universe as E rather than the maximum over F and E). Usually denoted by $\operatorname{Emb}_F(E)$ in textbooks.

  Remark: if E / F is not algebraic, then this definition makes no mathematical sense, and if it is infinite, then its cardinality doesn't behave as expected (namely, not equal to the field extension degree of separableClosure F E / F). For example, if $F = \mathbb{Q}$ and $E = \mathbb{Q}( \mu_{p^\infty} )$, then $\operatorname{Emb}_F (E)$ is in bijection with $\operatorname{Gal}(E/F)$, which is isomorphic to $\mathbb{Z}_p^\times$, which is uncountable, while $[E:F]$ is countable.

  TODO: prove or disprove that if E / F is algebraic and Emb F E is infinite, then Field.Emb F E has cardinality 2 ^ Module.rank F (separableClosure F E).

• Field.finSepDegree F E: the (finite) separable degree $[E:F]_s$ of an algebraic extension E / F of fields, defined to be the number of F-algebra homomorphisms from E to the algebraic closure of E, as a natural number. It is zero if Field.Emb F E is not finite. Note that if E / F is not algebraic, then this definition makes no mathematical sense.

  Remark: the Cardinal-valued, potentially infinite separable degree Field.sepDegree F E for a general algebraic extension E / F is defined to be the degree of L / F, where L is the (relative) separable closure separableClosure F E of F in E, which is not defined in this file yet. Later we will show that (Field.finSepDegree_eq), if Field.Emb F E is finite, then these two definitions coincide.

• Polynomial.natSepDegree: the separable degree of a polynomial is a natural number, defined to be the number of distinct roots of it over its splitting field.

Main results

• Field.embEquivOfEquiv, Field.finSepDegree_eq_of_equiv: a random bijection between Field.Emb F E and Field.Emb F K when E and K are isomorphic as F-algebras. In particular, they have the same cardinality (so their Field.finSepDegree are equal).

• Field.embEquivOfAdjoinSplits, Field.finSepDegree_eq_of_adjoin_splits: a random bijection between Field.Emb F E and E →ₐ[F] K if E = F(S) such that every element s of S is integral (= algebraic) over F and whose minimal polynomial splits in K. In particular, they have the same cardinality.

• Field.embEquivOfIsAlgClosed, Field.finSepDegree_eq_of_isAlgClosed: a random bijection between Field.Emb F E and E →ₐ[F] K when E / F is algebraic and K / F is algebraically closed. In particular, they have the same cardinality.

• Field.embProdEmbOfIsAlgebraic, Field.finSepDegree_mul_finSepDegree_of_isAlgebraic: if K / E / F is a field extension tower, such that K / E is algebraic, then there is a non-canonical bijection Field.Emb F E × Field.Emb E K ≃ Field.Emb F K. In particular, the separable degrees satisfy the tower law: $[E:F]_s [K:E]_s = [K:F]_s$ (see also FiniteDimensional.finrank_mul_finrank).

• Polynomial.natSepDegree_le_natDegree: the separable degree of a polynomial is smaller than its degree.

• Polynomial.natSepDegree_eq_natDegree_iff: the separable degree of a non-zero polynomial is equal to its degree if and only if it is separable.

• Polynomial.natSepDegree_eq_of_splits: if a polynomial splits over E, then its separable degree is equal to the number of distinct roots of it over E.

• Polynomial.natSepDegree_eq_of_isAlgClosed: the separable degree of a polynomial is equal to the number of distinct roots of it over any algebraically closed field.

• Polynomial.natSepDegree_expand: if a field F is of exponential characteristic q, then Polynomial.expand F (q ^ n) f and f have the same separable degree.

• Polynomial.HasSeparableContraction.natSepDegree_eq: if a polynomial has separable contraction, then its separable degree is equal to its separable contraction degree.

• Irreducible.natSepDegree_dvd_natDegree: the separable degree of an irreducible polynomial divides its degree.

• IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree: the separable degree of F⟮α⟯ / F is equal to the separable degree of the minimal polynomial of α over F.

• IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff: if α is algebraic over F, then the separable degree of F⟮α⟯ / F is equal to the degree of F⟮α⟯ / F if and only if α is a separable element.

• Field.finSepDegree_dvd_finrank: the separable degree of any field extension E / F divides the degree of E / F.

• Field.finSepDegree_le_finrank: the separable degree of a finite extension E / F is smaller than the degree of E / F.

• Field.finSepDegree_eq_finrank_iff: if E / F is a finite extension, then its separable degree is equal to its degree if and only if it is a separable extension.

• IntermediateField.isSeparable_adjoin_simple_iff_separable: F⟮x⟯ / F is a separable extension if and only if x is a separable element.

• IsSeparable.trans: if E / F and K / E are both separable, then K / F is also separable.

Tags

separable degree, degree, polynomial

def Field.Emb (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Type v

Field.Emb F E is the type of F-algebra homomorphisms from E to the algebraic closure of E.

Equations

• Field.Emb F E = (E →ₐ[F] AlgebraicClosure E)

def Field.finSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : ℕ

If E / F is an algebraic extension, then the (finite) separable degree of E / F is the number of F-algebra homomorphisms from E to the algebraic closure of E, as a natural number. It is defined to be zero if there are infinitely many of them. Note that if E / F is not algebraic, then this definition makes no mathematical sense.

Equations

• Field.finSepDegree F E = Nat.card (Field.Emb F E)

instance Field.instInhabitedEmb (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Inhabited (Field.Emb F E)

Equations

• Field.instInhabitedEmb F E = { default := IsScalarTower.toAlgHom F E (AlgebraicClosure E) }

instance Field.instNeZeroFinSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] : NeZero (Field.finSepDegree F E)

Equations

• ⋯ = ⋯

def Field.embEquivOfEquiv (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) : Field.Emb F E ≃ Field.Emb F K

A random bijection between Field.Emb F E and Field.Emb F K when E and K are isomorphic as F-algebras.

Equations

• Field.embEquivOfEquiv F E K i = AlgEquiv.arrowCongr i (AlgEquiv.symm (AlgEquiv.restrictScalars F (IsAlgClosure.equivOfAlgebraic E K (AlgebraicClosure K) (AlgebraicClosure E) ⋯)))

theorem Field.finSepDegree_eq_of_equiv (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) : Field.finSepDegree F E = Field.finSepDegree F K

If E and K are isomorphic as F-algebras, then they have the same Field.finSepDegree over F.

@[simp]

theorem Field.finSepDegree_self (F : Type u) [Field F] : Field.finSepDegree F F = 1

@[simp]

theorem IntermediateField.finSepDegree_bot (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Field.finSepDegree F ↥⊥ = 1

@[simp]

theorem IntermediateField.finSepDegree_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] : Field.finSepDegree F ↥⊥ = Field.finSepDegree F E

@[simp]

theorem IntermediateField.finSepDegree_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] : Field.finSepDegree F ↥⊤ = Field.finSepDegree F K

def Field.embEquivOfAdjoinSplits (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] {S : Set E} (hS : IntermediateField.adjoin F S = ⊤) (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) : Field.Emb F E ≃ (E →ₐ[F] K)

A random bijection between Field.Emb F E and E →ₐ[F] K if E = F(S) such that every element s of S is integral (= algebraic) over F and whose minimal polynomial splits in K. Combined with Field.instInhabitedEmb, it can be viewed as a stronger version of IntermediateField.nonempty_algHom_of_adjoin_splits.

Equations

• Field.embEquivOfAdjoinSplits F E K hS hK = let_fun halg := ⋯; Classical.choice ⋯

theorem Field.finSepDegree_eq_of_adjoin_splits (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] {S : Set E} (hS : IntermediateField.adjoin F S = ⊤) (hK : ∀ s ∈ S, IsIntegral F s ∧ Polynomial.Splits (algebraMap F K) (minpoly F s)) : Field.finSepDegree F E = Nat.card (E →ₐ[F] K)

The Field.finSepDegree F E is equal to the cardinality of E →ₐ[F] K if E = F(S) such that every element s of S is integral (= algebraic) over F and whose minimal polynomial splits in K.

def Field.embEquivOfIsAlgClosed (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] (halg : Algebra.IsAlgebraic F E) [IsAlgClosed K] : Field.Emb F E ≃ (E →ₐ[F] K)

A random bijection between Field.Emb F E and E →ₐ[F] K when E / F is algebraic and K / F is algebraically closed.

Equations

• Field.embEquivOfIsAlgClosed F E K halg = Field.embEquivOfAdjoinSplits F E K ⋯ ⋯

theorem Field.finSepDegree_eq_of_isAlgClosed (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (K : Type w) [Field K] [Algebra F K] (halg : Algebra.IsAlgebraic F E) [IsAlgClosed K] : Field.finSepDegree F E = Nat.card (E →ₐ[F] K)

The Field.finSepDegree F E is equal to the cardinality of E →ₐ[F] K as a natural number, when E / F is algebraic and K / F is algebraically closed.

def Field.embProdEmbOfIsAlgebraic (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 E K) : Field.Emb F E × Field.Emb E K ≃ Field.Emb F K

If K / E / F is a field extension tower, such that K / E is algebraic, then there is a non-canonical bijection Field.Emb F E × Field.Emb E K ≃ Field.Emb F K. A corollary of algHomEquivSigma.

Equations

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

theorem Field.finSepDegree_mul_finSepDegree_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 E K) : Field.finSepDegree F E * Field.finSepDegree E K = Field.finSepDegree F K

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

def Polynomial.natSepDegree {F : Type u} [Field F] (f : Polynomial F) : ℕ

The separable degree Polynomial.natSepDegree of a polynomial is a natural number, defined to be the number of distinct roots of it over its splitting field. This is similar to Polynomial.natDegree but not to Polynomial.degree, namely, the separable degree of 0 is 0, not negative infinity.

Equations

• Polynomial.natSepDegree f = (Multiset.toFinset (Polynomial.aroots f (Polynomial.SplittingField f))).card

theorem Polynomial.natSepDegree_le_natDegree {F : Type u} [Field F] (f : Polynomial F) : Polynomial.natSepDegree f ≤ Polynomial.natDegree f

The separable degree of a polynomial is smaller than its degree.

@[simp]

theorem Polynomial.natSepDegree_X_sub_C {F : Type u} [Field F] (x : F) : Polynomial.natSepDegree (Polynomial.X - Polynomial.C x) = 1

@[simp]

theorem Polynomial.natSepDegree_X {F : Type u} [Field F] : Polynomial.natSepDegree Polynomial.X = 1

theorem Polynomial.natSepDegree_eq_zero {F : Type u} [Field F] (f : Polynomial F) (h : Polynomial.natDegree f = 0) : Polynomial.natSepDegree f = 0

A constant polynomial has zero separable degree.

@[simp]

theorem Polynomial.natSepDegree_C {F : Type u} [Field F] (x : F) : Polynomial.natSepDegree (Polynomial.C x) = 0

@[simp]

theorem Polynomial.natSepDegree_zero {F : Type u} [Field F] : Polynomial.natSepDegree 0 = 0

@[simp]

theorem Polynomial.natSepDegree_one {F : Type u} [Field F] : Polynomial.natSepDegree 1 = 0

theorem Polynomial.natSepDegree_ne_zero {F : Type u} [Field F] (f : Polynomial F) (h : Polynomial.natDegree f ≠ 0) : Polynomial.natSepDegree f ≠ 0

A non-constant polynomial has non-zero separable degree.

theorem Polynomial.natSepDegree_eq_zero_iff {F : Type u} [Field F] (f : Polynomial F) : Polynomial.natSepDegree f = 0 ↔ Polynomial.natDegree f = 0

A polynomial has zero separable degree if and only if it is constant.

theorem Polynomial.natSepDegree_ne_zero_iff {F : Type u} [Field F] (f : Polynomial F) : Polynomial.natSepDegree f ≠ 0 ↔ Polynomial.natDegree f ≠ 0

A polynomial has non-zero separable degree if and only if it is non-constant.

theorem Polynomial.natSepDegree_eq_natDegree_iff {F : Type u} [Field F] (f : Polynomial F) (hf : f ≠ 0) : Polynomial.natSepDegree f = Polynomial.natDegree f ↔ Polynomial.Separable f

The separable degree of a non-zero polynomial is equal to its degree if and only if it is separable.

theorem Polynomial.natSepDegree_eq_natDegree_of_separable {F : Type u} [Field F] (f : Polynomial F) (h : Polynomial.Separable f) : Polynomial.natSepDegree f = Polynomial.natDegree f

If a polynomial is separable, then its separable degree is equal to its degree.

theorem Polynomial.Separable.natSepDegree_eq_natDegree {F : Type u} [Field F] {f : Polynomial F} (h : Polynomial.Separable f) : Polynomial.natSepDegree f = Polynomial.natDegree f

Same as Polynomial.natSepDegree_eq_natDegree_of_separable, but enables the use of dot notation.

theorem Polynomial.natSepDegree_eq_of_splits {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (f : Polynomial F) (h : Polynomial.Splits (algebraMap F E) f) : Polynomial.natSepDegree f = (Multiset.toFinset (Polynomial.aroots f E)).card

If a polynomial splits over E, then its separable degree is equal to the number of distinct roots of it over E.

theorem Polynomial.natSepDegree_eq_of_isAlgClosed {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (f : Polynomial F) [IsAlgClosed E] : Polynomial.natSepDegree f = (Multiset.toFinset (Polynomial.aroots f E)).card

The separable degree of a polynomial is equal to the number of distinct roots of it over any algebraically closed field.

theorem Polynomial.natSepDegree_map {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (f : Polynomial F) : Polynomial.natSepDegree (Polynomial.map (algebraMap F E) f) = Polynomial.natSepDegree f

@[simp]

theorem Polynomial.natSepDegree_C_mul {F : Type u} [Field F] (f : Polynomial F) {x : F} (hx : x ≠ 0) : Polynomial.natSepDegree (Polynomial.C x * f) = Polynomial.natSepDegree f

@[simp]

theorem Polynomial.natSepDegree_smul_nonzero {F : Type u} [Field F] (f : Polynomial F) {x : F} (hx : x ≠ 0) : Polynomial.natSepDegree (x • f) = Polynomial.natSepDegree f

@[simp]

theorem Polynomial.natSepDegree_pow {F : Type u} [Field F] (f : Polynomial F) {n : ℕ} : Polynomial.natSepDegree (f ^ n) = if n = 0 then 0 else Polynomial.natSepDegree f

theorem Polynomial.natSepDegree_pow_of_ne_zero {F : Type u} [Field F] (f : Polynomial F) {n : ℕ} (hn : n ≠ 0) : Polynomial.natSepDegree (f ^ n) = Polynomial.natSepDegree f

theorem Polynomial.natSepDegree_X_pow {F : Type u} [Field F] {n : ℕ} : Polynomial.natSepDegree (Polynomial.X ^ n) = if n = 0 then 0 else 1

theorem Polynomial.natSepDegree_X_sub_C_pow {F : Type u} [Field F] {x : F} {n : ℕ} : Polynomial.natSepDegree ((Polynomial.X - Polynomial.C x) ^ n) = if n = 0 then 0 else 1

theorem Polynomial.natSepDegree_C_mul_X_sub_C_pow {F : Type u} [Field F] {x : F} {y : F} {n : ℕ} (hx : x ≠ 0) : Polynomial.natSepDegree (Polynomial.C x * (Polynomial.X - Polynomial.C y) ^ n) = if n = 0 then 0 else 1

theorem Polynomial.natSepDegree_mul {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) : Polynomial.natSepDegree (f * g) ≤ Polynomial.natSepDegree f + Polynomial.natSepDegree g

theorem Polynomial.natSepDegree_mul_eq_iff {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) : Polynomial.natSepDegree (f * g) = Polynomial.natSepDegree f + Polynomial.natSepDegree g ↔ f = 0 ∧ g = 0 ∨ IsCoprime f g

theorem Polynomial.natSepDegree_mul_of_isCoprime {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) (hc : IsCoprime f g) : Polynomial.natSepDegree (f * g) = Polynomial.natSepDegree f + Polynomial.natSepDegree g

theorem Polynomial.natSepDegree_le_of_dvd {F : Type u} [Field F] (f : Polynomial F) (g : Polynomial F) (h1 : f ∣ g) (h2 : g ≠ 0) : Polynomial.natSepDegree f ≤ Polynomial.natSepDegree g

theorem Polynomial.natSepDegree_expand {F : Type u} [Field F] (f : Polynomial F) (q : ℕ) [hF : ExpChar F q] {n : ℕ} : Polynomial.natSepDegree ((Polynomial.expand F (q ^ n)) f) = Polynomial.natSepDegree f

If a field F is of exponential characteristic q, then Polynomial.expand F (q ^ n) f and f have the same separable degree.

theorem Polynomial.natSepDegree_X_pow_char_pow_sub_C {F : Type u} [Field F] (q : ℕ) [ExpChar F q] (n : ℕ) (y : F) : Polynomial.natSepDegree (Polynomial.X ^ q ^ n - Polynomial.C y) = 1

theorem Polynomial.IsSeparableContraction.natSepDegree_eq {F : Type u} [Field F] {f : Polynomial F} {g : Polynomial F} {q : ℕ} [ExpChar F q] (h : Polynomial.IsSeparableContraction q f g) : Polynomial.natSepDegree f = Polynomial.natDegree g

If g is a separable contraction of f, then the separable degree of f is equal to the degree of g.

theorem Polynomial.HasSeparableContraction.natSepDegree_eq {F : Type u} [Field F] {f : Polynomial F} {q : ℕ} [ExpChar F q] (hf : Polynomial.HasSeparableContraction q f) : Polynomial.natSepDegree f = Polynomial.HasSeparableContraction.degree hf

If a polynomial has separable contraction, then its separable degree is equal to the degree of the given separable contraction.

theorem Irreducible.natSepDegree_dvd_natDegree {F : Type u} [Field F] {f : Polynomial F} (h : Irreducible f) : Polynomial.natSepDegree f ∣ Polynomial.natDegree f

The separable degree of an irreducible polynomial divides its degree.

theorem Irreducible.natSepDegree_eq_one_iff_of_monic' {F : Type u} [Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q] (hm : Polynomial.Monic f) (hi : Irreducible f) : Polynomial.natSepDegree f = 1 ↔ ∃ (n : ℕ) (y : F), f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)

A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form Polynomial.expand F (q ^ n) (X - C y) for some n : ℕ and y : F.

theorem Irreducible.natSepDegree_eq_one_iff_of_monic {F : Type u} [Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q] (hm : Polynomial.Monic f) (hi : Irreducible f) : Polynomial.natSepDegree f = 1 ↔ ∃ (n : ℕ) (y : F), f = Polynomial.X ^ q ^ n - Polynomial.C y

A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form X ^ (q ^ n) - C y for some n : ℕ and y : F.

theorem Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible' {F : Type u} [Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q] (hm : Polynomial.Monic f) (hi : Irreducible f) : Polynomial.natSepDegree f = 1 ↔ ∃ (n : ℕ) (y : F), f = (Polynomial.expand F (q ^ n)) (Polynomial.X - Polynomial.C y)

Alias of Irreducible.natSepDegree_eq_one_iff_of_monic'.

---

A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form Polynomial.expand F (q ^ n) (X - C y) for some n : ℕ and y : F.

theorem Polynomial.Monic.natSepDegree_eq_one_iff_of_irreducible {F : Type u} [Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q] (hm : Polynomial.Monic f) (hi : Irreducible f) : Polynomial.natSepDegree f = 1 ↔ ∃ (n : ℕ) (y : F), f = Polynomial.X ^ q ^ n - Polynomial.C y

Alias of Irreducible.natSepDegree_eq_one_iff_of_monic.

---

A monic irreducible polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form X ^ (q ^ n) - C y for some n : ℕ and y : F.

theorem Polynomial.Monic.eq_X_sub_C_pow_of_natSepDegree_eq_one_of_splits {F : Type u} [Field F] {f : Polynomial F} (hm : Polynomial.Monic f) (hs : Polynomial.Splits (RingHom.id F) f) (h : Polynomial.natSepDegree f = 1) : ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = (Polynomial.X - Polynomial.C y) ^ m

If a monic polynomial of separable degree one splits, then it is of form (X - C y) ^ m for some non-zero natural number m and some element y of F.

theorem Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible {F : Type u} [Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q] (hm : Polynomial.Monic f) (hi : Irreducible f) (h : Polynomial.natSepDegree f = 1) : ∃ (n : ℕ) (y : F), (n = 0 ∨ y ∉ RingHom.range (frobenius F q)) ∧ f = Polynomial.X ^ q ^ n - Polynomial.C y

If a monic irreducible polynomial over a field F of exponential characteristic q has separable degree one, then it is of the form X ^ (q ^ n) - C y for some natural number n, and some element y of F, such that either n = 0 or y has no q-th root in F.

theorem Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one {F : Type u} [Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q] (hm : Polynomial.Monic f) (h : Polynomial.natSepDegree f = 1) : ∃ (m : ℕ) (n : ℕ) (y : F), m ≠ 0 ∧ (n = 0 ∨ y ∉ RingHom.range (frobenius F q)) ∧ f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m

If a monic polynomial over a field F of exponential characteristic q has separable degree one, then it is of the form (X ^ (q ^ n) - C y) ^ m for some non-zero natural number m, some natural number n, and some element y of F, such that either n = 0 or y has no q-th root in F.

theorem Polynomial.Monic.natSepDegree_eq_one_iff {F : Type u} [Field F] {f : Polynomial F} (q : ℕ) [ExpChar F q] (hm : Polynomial.Monic f) : Polynomial.natSepDegree f = 1 ↔ ∃ (m : ℕ) (n : ℕ) (y : F), m ≠ 0 ∧ f = (Polynomial.X ^ q ^ n - Polynomial.C y) ^ m

A monic polynomial over a field F of exponential characteristic q has separable degree one if and only if it is of the form (X ^ (q ^ n) - C y) ^ m for some non-zero natural number m, some natural number n, and some element y of F.

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

The minimal polynomial of an element of E / F of exponential characteristic q has separable degree one if and only if the minimal polynomial is of the form Polynomial.expand F (q ^ n) (X - C y) for some n : ℕ and y : F.

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

The minimal polynomial of an element of E / F of exponential characteristic q has separable degree one if and only if the minimal polynomial is of the form X ^ (q ^ n) - C y for some n : ℕ and y : F.

theorem minpoly.natSepDegree_eq_one_iff_pow_mem {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {x : E} : Polynomial.natSepDegree (minpoly F x) = 1 ↔ ∃ (n : ℕ), x ^ q ^ n ∈ RingHom.range (algebraMap F E)

The minimal polynomial of an element x of E / F of exponential characteristic q has separable degree one if and only if x ^ (q ^ n) ∈ F for some n : ℕ.

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

The minimal polynomial of an element x of E / F of exponential characteristic q has separable degree one if and only if the minimal polynomial is of the form (X - x) ^ (q ^ n) for some n : ℕ.

theorem IntermediateField.finSepDegree_adjoin_simple_eq_natSepDegree (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {α : E} (halg : IsAlgebraic F α) : Field.finSepDegree F ↥F⟮α⟯ = Polynomial.natSepDegree (minpoly F α)

The separable degree of F⟮α⟯ / F is equal to the separable degree of the minimal polynomial of α over F.

theorem IntermediateField.finSepDegree_adjoin_simple_le_finrank (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (α : E) (halg : IsAlgebraic F α) : Field.finSepDegree F ↥F⟮α⟯ ≤ FiniteDimensional.finrank F ↥F⟮α⟯

The separable degree of F⟮α⟯ / F is smaller than the degree of F⟮α⟯ / F if α is algebraic over F.

theorem IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] (α : E) (halg : IsAlgebraic F α) : Field.finSepDegree F ↥F⟮α⟯ = FiniteDimensional.finrank F ↥F⟮α⟯ ↔ Polynomial.Separable (minpoly F α)

If α is algebraic over F, then the separable degree of F⟮α⟯ / F is equal to the degree of F⟮α⟯ / F if and only if α is a separable element.

theorem Field.finSepDegree_dvd_finrank (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] : Field.finSepDegree F E ∣ FiniteDimensional.finrank F E

The separable degree of any field extension E / F divides the degree of E / F.

theorem Field.finSepDegree_le_finrank (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] : Field.finSepDegree F E ≤ FiniteDimensional.finrank F E

The separable degree of a finite extension E / F is smaller than the degree of E / F.

theorem Field.finSepDegree_eq_finrank_of_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSeparable F E] : Field.finSepDegree F E = FiniteDimensional.finrank F E

If E / F is a separable extension, then its separable degree is equal to its degree. When E / F is infinite, it means that Field.Emb F E has infinitely many elements. (But the cardinality of Field.Emb F E is not equal to Module.rank F E in general!)

theorem IsSeparable.finSepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [IsSeparable F E] : Field.finSepDegree F E = FiniteDimensional.finrank F E

Alias of Field.finSepDegree_eq_finrank_of_isSeparable.

---

If E / F is a separable extension, then its separable degree is equal to its degree. When E / F is infinite, it means that Field.Emb F E has infinitely many elements. (But the cardinality of Field.Emb F E is not equal to Module.rank F E in general!)

theorem Field.finSepDegree_eq_finrank_iff (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [FiniteDimensional F E] : Field.finSepDegree F E = FiniteDimensional.finrank F E ↔ IsSeparable F E

If E / F is a finite extension, then its separable degree is equal to its degree if and only if it is a separable extension.

theorem IntermediateField.separable_of_mem_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} [IsSeparable F ↥L] {x : E} (h : x ∈ L) : Polynomial.Separable (minpoly F x)

theorem IntermediateField.isSeparable_adjoin_simple_iff_separable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {x : E} : IsSeparable F ↥F⟮x⟯ ↔ Polynomial.Separable (minpoly F x)

F⟮x⟯ / F is a separable extension if and only if x is a separable element. As a consequence, any rational function of x is also a separable element.

theorem Polynomial.Separable.comap_minpoly_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] {x : K} (hsep : Polynomial.Separable (minpoly E x)) : Polynomial.Separable (minpoly F x)

If K / E / F is an extension tower such that E / F is separable, x : K is separable over E, then it's also separable over F.

theorem IsSeparable.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] [IsSeparable F E] [IsSeparable E K] : IsSeparable F K

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

theorem IntermediateField.isSeparable_adjoin_pair_of_separable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {x : E} {y : E} (hx : Polynomial.Separable (minpoly F x)) (hy : Polynomial.Separable (minpoly F y)) : IsSeparable F ↥F⟮x, y⟯

If x and y are both separable elements, then F⟮x, y⟯ / F is a separable extension. As a consequence, any rational function of x and y is also a separable element.

theorem Field.separable_algebraMap {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (x : F) : Polynomial.Separable (minpoly F ((algebraMap F E) x))

Any element x of F is a separable element of E / F when embedded into E.

theorem Field.separable_mul {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} {y : E} (hx : Polynomial.Separable (minpoly F x)) (hy : Polynomial.Separable (minpoly F y)) : Polynomial.Separable (minpoly F (x * y))

If x and y are both separable elements, then x * y is also a separable element.

theorem Field.separable_add {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} {y : E} (hx : Polynomial.Separable (minpoly F x)) (hy : Polynomial.Separable (minpoly F y)) : Polynomial.Separable (minpoly F (x + y))

If x and y are both separable elements, then x + y is also a separable element.

theorem Field.separable_inv {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] (x : E) (hx : Polynomial.Separable (minpoly F x)) : Polynomial.Separable (minpoly F x⁻¹)

If x is a separable element, then x⁻¹ is also a separable element.

theorem perfectField_iff_splits_of_natSepDegree_eq_one (F : Type u_1) [Field F] : PerfectField F ↔ ∀ (f : Polynomial F), Polynomial.natSepDegree f = 1 → Polynomial.Splits (RingHom.id F) f

A field is a perfect field (which means that any irreducible polynomial is separable) if and only if every separable degree one polynomial splits.