mathlib3 documentation

field_theory.separable_degree

Separable degree #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 u_1} [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 u_1} [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.

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} [field F] (q : ) [hq : ne_zero 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.