Documentation

Mathlib.FieldTheory.SeparableDegree

Separable degree #

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

Main results #

Tags #

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

Instances For

    The condition of having a separable contraction.

    Instances For

      A choice of a separable contraction.

      Instances For

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

        Instances For

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

          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 : NeZero q] [CharP F q] (g : Polynomial F) (g' : Polynomial F) (m : ) (m' : ) (h_expand : ↑(Polynomial.expand F (q ^ m)) g = ↑(Polynomial.expand F (q ^ m')) g') (hg : Polynomial.Separable g) (hg' : Polynomial.Separable g') :

          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.