# 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} [] (q : ) (f : ) (g : ) :

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

Equations
Instances For
def Polynomial.HasSeparableContraction {F : Type u_1} [] (q : ) (f : ) :

The condition of having a separable contraction.

Equations
• = ∃ (g : ),
Instances For
def Polynomial.HasSeparableContraction.contraction {F : Type u_1} [] {q : } {f : } (hf : ) :

A choice of a separable contraction.

Equations
• hf.contraction =
Instances For
def Polynomial.HasSeparableContraction.degree {F : Type u_1} [] {q : } {f : } (hf : ) :

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

Equations
• hf.degree = hf.contraction.natDegree
Instances For
theorem Polynomial.HasSeparableContraction.isSeparableContraction {F : Type u_1} [] {q : } {f : } (hf : ) :

The HasSeparableContraction.contraction is indeed a separable contraction.

theorem Polynomial.IsSeparableContraction.dvd_degree' {F : Type u_1} [] {q : } {f : } (hf : ) {g : } (hf : ) :
∃ (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} [] {q : } {f : } (hf : ) :
∃ (m : ), hf.degree * q ^ m = f.natDegree
theorem Polynomial.HasSeparableContraction.dvd_degree {F : Type u_1} [] {q : } {f : } (hf : ) :
hf.degree f.natDegree

The separable degree divides the degree.

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

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

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

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} [] (q : ) [hq : ] [CharP F q] (g : ) (g' : ) (m : ) (m' : ) (h_expand : (Polynomial.expand F (q ^ m)) g = (Polynomial.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} [] (q : ) {f : } (hf : ) [hF : ExpChar F q] (g : ) (hg : ) :
g.natDegree = hf.degree

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