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.eq_degreespecialize the statement of
is_separable_contraction.degree_eq: the separable degree is well-defined, implemented as the statement that the degree of any separable contraction equals
separable degree, degree, polynomial
A separable contraction of a polynomial
f is a separable polynomial
g such that
g(x^(q^m)) = f(x) for some
m : ℕ.
The separable degree divides the degree, in function of the exponential characteristic of F.
Every irreducible polynomial can be contracted to a separable polynomial. https://stacks.math.columbia.edu/tag/09H0
A helper lemma: if two expansions (along the positive characteristic) of two polynomials
g' agree, and the one with the larger degree is separable, then their degrees are the same.
If two expansions (along the positive characteristic) of two separable polynomials
g' agree, then they have the same degree.
The separable degree equals the degree of any separable contraction, i.e., it is unique.