Separable degree

This file contains basics about the separable degree of a polynomial.

Main results

• IsSeparableContraction: is the condition that, for g a separable polynomial, we have that g(x^(q^m)) = f(x) for some m : ℕ.
• HasSeparableContraction: the condition of having a separable contraction
• HasSeparableContraction.degree: the separable degree, defined as the degree of some separable contraction
• Irreducible.HasSeparableContraction: any irreducible polynomial can be contracted to a separable polynomial
• HasSeparableContraction.dvd_degree': the degree of a separable contraction divides the degree, in function of the exponential characteristic of the field
• HasSeparableContraction.dvd_degree and HasSeparableContraction.eq_degree specialize the statement of separable_degree_dvd_degree
• IsSeparableContraction.degree_eq: the separable degree is well-defined, implemented as the statement that the degree of any separable contraction equals HasSeparableContraction.degree

Tags

separable degree, degree, polynomial

def Polynomial.IsSeparableContraction {F : Type u_1} [CommSemiring F] (q : ℕ) (f : Polynomial F) (g : Polynomial F) : Prop

A separable contraction of a polynomial f is a separable polynomial g such that g(x^(q^m)) = f(x) for some m : ℕ.

def Polynomial.HasSeparableContraction {F : Type u_1} [CommSemiring F] (q : ℕ) (f : Polynomial F) : Prop

The condition of having a separable contraction.

def Polynomial.HasSeparableContraction.contraction {F : Type u_1} [CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) : Polynomial F

A choice of a separable contraction.

def Polynomial.HasSeparableContraction.degree {F : Type u_1} [CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) : ℕ

The separable degree of a polynomial is the degree of a given separable contraction.

theorem Polynomial.IsSeparableContraction.dvd_degree' {F : Type u_1} [CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) {g : Polynomial F} (hf : Polynomial.IsSeparableContraction q f g) : ∃ m, Polynomial.natDegree g * q ^ m = Polynomial.natDegree f

The separable degree divides the degree, in function of the exponential characteristic of F.

theorem Polynomial.HasSeparableContraction.dvd_degree' {F : Type u_1} [CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) : ∃ m, Polynomial.HasSeparableContraction.degree hf * q ^ m = Polynomial.natDegree f

theorem Polynomial.HasSeparableContraction.dvd_degree {F : Type u_1} [CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) : Polynomial.HasSeparableContraction.degree hf ∣ Polynomial.natDegree f

The separable degree divides the degree.

theorem Polynomial.HasSeparableContraction.eq_degree {F : Type u_1} [CommSemiring F] {f : Polynomial F} (hf : Polynomial.HasSeparableContraction 1 f) : Polynomial.HasSeparableContraction.degree hf = Polynomial.natDegree f

In exponential characteristic one, the separable degree equals the degree.

theorem Polynomial.Irreducible.hasSeparableContraction {F : Type u_1} [Field F] (q : ℕ) [hF : ExpChar F q] (f : Polynomial F) (irred : Irreducible f) : Polynomial.HasSeparableContraction q f

Every irreducible polynomial can be contracted to a separable polynomial. https://stacks.math.columbia.edu/tag/09H0

theorem Polynomial.contraction_degree_eq_or_insep {F : Type u_1} [Field F] (q : ℕ) [hq : NeZero q] [CharP F q] (g : Polynomial F) (g' : Polynomial F) (m : ℕ) (m' : ℕ) (h_expand : ↑(Polynomial.expand F (q ^ m)) g = ↑(Polynomial.expand F (q ^ m')) g') (hg : Polynomial.Separable g) (hg' : Polynomial.Separable g') : Polynomial.natDegree g = Polynomial.natDegree g'

If two expansions (along the positive characteristic) of two separable polynomials g and g' agree, then they have the same degree.

theorem Polynomial.IsSeparableContraction.degree_eq {F : Type u_1} [Field F] (q : ℕ) {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) [hF : ExpChar F q] (g : Polynomial F) (hg : Polynomial.IsSeparableContraction q f g) : Polynomial.natDegree g = Polynomial.HasSeparableContraction.degree hf

The separable degree equals the degree of any separable contraction, i.e., it is unique.