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 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 : ℕ.

Equations

• Polynomial.IsSeparableContraction q f g = (g.Separable ∧ ∃ (m : ℕ), (Polynomial.expand F (q ^ m)) g = f)

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

The condition of having a separable contraction.

Equations

• Polynomial.HasSeparableContraction q f = ∃ (g : Polynomial F), Polynomial.IsSeparableContraction q f g

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

A choice of a separable contraction.

Equations

• hf.contraction = Classical.choose hf

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

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

Equations

• hf.degree = hf.contraction.natDegree

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

The HasSeparableContraction.contraction is indeed a separable contraction.

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

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 : HasSeparableContraction q f) : ∃ (m : ℕ), hf.degree * q ^ m = f.natDegree

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

The separable degree divides the degree.

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

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

theorem 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.

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

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 : HasSeparableContraction q f) [hF : ExpChar F q] (g : Polynomial F) (hg : IsSeparableContraction q f g) : g.natDegree = hf.degree

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