# Documentation

Mathlib.FieldTheory.SeparableDegree

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

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

The condition of having a separable contraction.

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

A choice of a separable 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.

Instances For
theorem Polynomial.IsSeparableContraction.dvd_degree' {F : Type u_1} [] {q : } {f : } (hf : ) {g : } (hf : ) :
m,

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,
theorem Polynomial.HasSeparableContraction.dvd_degree {F : Type u_1} [] {q : } {f : } (hf : ) :

The separable degree divides the degree.

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

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

theorem Polynomial.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 : ) (hg' : ) :

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 : ) :

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