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.

• Field.finSepDegree F E: the (finite) separable degree $[E:F]_s$ of an 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 separable closure 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. If E / F is algebraic with infinite separable degree, we have #(Field.Emb F E) = 2 ^ Field.sepDegree F E instead. (See Field.Emb.cardinal_eq_two_pow_sepDegree in another file.) 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, whereas $ [E:F] $ is countable.

• 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 Module.finrank_mul_finrank).

• Field.infinite_emb_of_transcendental: Field.Emb is infinite for transcendental extensions.

• 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_isSeparable: F⟮x⟯ / F is a separable extension if and only if x is a separable element.

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

Tags

separable degree, degree, polynomial

@[reducible, inline]

abbrev 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 (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 (finSepDegree F E)

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) : Emb F E ≃ 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

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

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) : finSepDegree F E = 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] : 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)) : 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 = 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)) : 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] [Algebra.IsAlgebraic F E] [IsAlgClosed K] : 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 = 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] [Algebra.IsAlgebraic F E] [IsAlgClosed K] : 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] [Algebra.IsAlgebraic E K] : Emb F E × Emb E K ≃ 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.

instance Field.infinite_emb_of_transcendental (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [H : Algebra.Transcendental F E] : Infinite (Emb F E)

If the field extension E / F is transcendental, then Field.Emb F E is infinite.

theorem Field.finSepDegree_eq_zero_of_transcendental (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.Transcendental F E] : finSepDegree F E = 0

If the field extension E / F is transcendental, then Field.finSepDegree F E = 0, which actually means that Field.Emb F E is infinite (see Field.infinite_emb_of_transcendental).

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] [Algebra.IsAlgebraic E K] : finSepDegree F E * finSepDegree E K = 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 Module.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

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

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

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) : (X - C x).natSepDegree = 1

@[simp]

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

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

A constant polynomial has zero separable degree.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Polynomial.natSepDegree_eq_zero_iff {F : Type u} [Field F] (f : Polynomial F) : f.natSepDegree = 0 ↔ f.natDegree = 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) : f.natSepDegree ≠ 0 ↔ f.natDegree ≠ 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) : f.natSepDegree = f.natDegree ↔ f.Separable

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 : f.Separable) : f.natSepDegree = f.natDegree

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 : f.Separable) : f.natSepDegree = f.natDegree

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) [DecidableEq E] (h : Splits (algebraMap F E) f) : f.natSepDegree = (f.aroots E).toFinset.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) [DecidableEq E] [IsAlgClosed E] : f.natSepDegree = (f.aroots E).toFinset.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 {E : Type v} [Field E] (K : Type w) [Field K] (f : Polynomial E) (i : E →+* K) : (map i f).natSepDegree = f.natSepDegree

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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) : (X ^ q ^ n - C y).natSepDegree = 1

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

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 : HasSeparableContraction q f) : f.natSepDegree = hf.degree

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) : f.natSepDegree ∣ f.natDegree

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 : f.Monic) (hi : Irreducible f) : f.natSepDegree = 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 : f.Monic) (hi : Irreducible f) : f.natSepDegree = 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 : f.Monic) (hi : Irreducible f) : f.natSepDegree = 1 ↔ ∃ (n : ℕ) (y : F), f = (Polynomial.expand F (q ^ n)) (X - 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 : f.Monic) (hi : Irreducible f) : f.natSepDegree = 1 ↔ ∃ (n : ℕ) (y : F), f = X ^ q ^ n - 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 : f.Monic) (hs : Splits (RingHom.id F) f) (h : f.natSepDegree = 1) : ∃ (m : ℕ) (y : F), m ≠ 0 ∧ f = (X - 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 : f.Monic) (hi : Irreducible f) (h : f.natSepDegree = 1) : ∃ (n : ℕ) (y : F), (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = X ^ q ^ n - 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 : f.Monic) (h : f.natSepDegree = 1) : ∃ (m : ℕ) (n : ℕ) (y : F), m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - 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 : f.Monic) : f.natSepDegree = 1 ↔ ∃ (m : ℕ) (n : ℕ) (y : F), m ≠ 0 ∧ f = (X ^ q ^ n - 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] [Ring E] [IsDomain E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {x : E} : (minpoly F x).natSepDegree = 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] [Ring E] [IsDomain E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {x : E} : (minpoly F x).natSepDegree = 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] [Ring E] [IsDomain E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {x : E} : (minpoly F x).natSepDegree = 1 ↔ ∃ (n : ℕ), x ^ q ^ n ∈ (algebraMap F E).range

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] [Ring E] [IsDomain E] [Algebra F E] (q : ℕ) [hF : ExpChar F q] {x : E} : (minpoly F x).natSepDegree = 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⟮α⟯ = (minpoly F α).natSepDegree

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⟮α⟯ ≤ Module.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⟮α⟯ = Module.finrank F ↥F⟮α⟯ ↔ IsSeparable 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] : finSepDegree F E ∣ Module.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] : finSepDegree F E ≤ Module.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] [Algebra.IsSeparable F E] : finSepDegree F E = Module.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 Field.Algebra.IsSeparable.finSepDegree_eq (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] [Algebra.IsSeparable F E] : finSepDegree F E = Module.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] : finSepDegree F E = Module.finrank F E ↔ Algebra.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.isSeparable_of_mem_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {L : IntermediateField F E} [Algebra.IsSeparable F ↥L] {x : E} (h : x ∈ L) : IsSeparable F x

theorem IntermediateField.isSeparable_adjoin_simple_iff_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {x : E} : Algebra.IsSeparable F ↥F⟮x⟯ ↔ IsSeparable 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 IsSeparable.of_algebra_isSeparable_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] [Algebra.IsSeparable F E] {x : K} (hsep : IsSeparable E x) : IsSeparable 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 Algebra.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] [Algebra.IsSeparable F E] [Algebra.IsSeparable E K] : Algebra.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_isSeparable (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E] {x y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) : Algebra.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.isSeparable_algebraMap {F : Type u} (E : Type v) [Field F] [Field E] [Algebra F E] (x : F) : IsSeparable F ((algebraMap F E) x)

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

theorem Field.isSeparable_mul {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) : IsSeparable F (x * y)

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

theorem Field.isSeparable_add {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) : IsSeparable F (x + y)

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

theorem Field.isSeparable_neg {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} (hx : IsSeparable F x) : IsSeparable F (-x)

If x is a separable elements, then -x is also a separable element.

theorem Field.isSeparable_sub {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x y : E} (hx : IsSeparable F x) (hy : IsSeparable F y) : IsSeparable F (x - y)

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

theorem Field.isSeparable_inv {F : Type u} {E : Type v} [Field F] [Field E] [Algebra F E] {x : E} (hx : IsSeparable F x) : IsSeparable 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), f.natSepDegree = 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.

theorem PerfectField.splits_of_natSepDegree_eq_one {E : Type v} [Field E] {K : Type w} [Field K] [PerfectField K] {f : Polynomial E} (i : E →+* K) (hf : f.natSepDegree = 1) : Polynomial.Splits i f