Documentation

Mathlib.RingTheory.Polynomial.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 : ℕ.

Equations
Instances For

    The condition of having a separable contraction.

    Equations
    Instances For

      A choice of a separable contraction.

      Equations
      Instances For

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

        Equations
        • hf.degree = hf.contraction.natDegree
        Instances For
          theorem Polynomial.IsSeparableContraction.dvd_degree' {F : Type u_1} [CommSemiring F] {q : } {f : Polynomial F} {g : Polynomial F} (hf : Polynomial.IsSeparableContraction q f g) :
          ∃ (m : ), g.natDegree * q ^ m = f.natDegree

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

          theorem Polynomial.HasSeparableContraction.dvd_degree' {F : Type u_1} [CommSemiring F] {q : } {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) :
          ∃ (m : ), hf.degree * q ^ m = f.natDegree
          theorem Polynomial.HasSeparableContraction.dvd_degree {F : Type u_1} [CommSemiring F] {q : } {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) :
          hf.degree f.natDegree

          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 : 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 : g.Separable) (hg' : g'.Separable) :
          g.natDegree = g'.natDegree

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

          theorem Polynomial.IsSeparableContraction.degree_eq {F : Type u_1} [Field F] (q : ) {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f) [hF : ExpChar F q] (g : Polynomial F) (hg : Polynomial.IsSeparableContraction q f g) :
          g.natDegree = hf.degree

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