mathlib documentation

field_theory.separable_degree

Separable degree #

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

Main results #

Tags #

separable degree, degree, polynomial

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

The condition of having a separable contration.

Equations

A choice of a separable contraction.

Equations

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

Equations

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

The separable degree divides the degree.

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

theorem polynomial.irreducible_has_separable_contraction {F : Type} [field F] (q : ) [hF : exp_char F 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 : char_p F q] (g g' : polynomial F) (m m' : ) (h_expand : (polynomial.expand F (q ^ m)) g = (polynomial.expand F (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)] [char_p F q] (g g' : polynomial F) (m m' : ) (h_expand : (polynomial.expand F (q ^ m)) g = (polynomial.expand F (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.

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