# mathlibdocumentation

field_theory.separable_degree

# Separable degree #

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

## Main results #

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

## Tags #

separable degree, degree, polynomial

def polynomial.is_separable_contraction {F : Type} (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
def polynomial.has_separable_contraction {F : Type} (q : ) (f : polynomial F) :
Prop

The condition of having a separable contration.

Equations
• = ∃ (g : ,
def polynomial.has_separable_contraction.contraction {F : Type} {q : } {f : polynomial F} (hf : f) :

A choice of a separable contraction.

Equations
def polynomial.has_separable_contraction.degree {F : Type} {q : } {f : polynomial F} (hf : f) :

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

Equations
theorem polynomial.is_separable_contraction.dvd_degree' {F : Type} {q : } {f g : polynomial F} (hf : g) :
∃ (m : ), (g.nat_degree) * q ^ m = f.nat_degree

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

theorem polynomial.has_separable_contraction.dvd_degree' {F : Type} {q : } {f : polynomial F} (hf : f) :
∃ (m : ), (hf.degree) * q ^ m = f.nat_degree
theorem polynomial.has_separable_contraction.dvd_degree {F : Type} {q : } {f : polynomial F} (hf : f) :

The separable degree divides the degree.

theorem polynomial.has_separable_contraction.eq_degree {F : Type} {f : polynomial F} (hf : f) :

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

theorem polynomial.irreducible_has_separable_contraction {F : Type} [field F] (q : ) [hF : q] (f : polynomial F) [irred : irreducible f] (fn : f 0) :

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

theorem polynomial.contraction_degree_eq_aux {F : Type} [field F] (q : ) [hq : fact (nat.prime q)] [hF : q] (g g' : polynomial F) (m m' : ) (h_expand : (q ^ m)) g = (q ^ m')) g') (h : m < m') (hg : g.separable) :

A helper lemma: if two expansions (along the positive characteristic) of two polynomials g and g' agree, and the one with the larger degree is separable, then their degrees are the same.

theorem polynomial.contraction_degree_eq_or_insep {F : Type} [field F] (q : ) [hq : fact (nat.prime q)] [ q] (g g' : polynomial F) (m m' : ) (h_expand : (q ^ m)) g = (q ^ m')) g') (hg : g.separable) (hg' : g'.separable) :

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

theorem polynomial.is_separable_contraction.degree_eq {F : Type} [field F] (q : ) {f : polynomial F} (hf : f) [hF : q] (g : polynomial F) (hg : g) :

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