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 #

is_separable_contraction: is the condition that, for g a separable polynomial, we have 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 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.dvd_degree and has_separable_contraction.eq_degree specialize the statement of separable_degree_dvd_degree
is_separable_contraction.degree_eq: the separable degree is well-defined, implemented as the statement that the degree of any separable contraction equals has_separable_contraction.degree

Tags #

separable degree, degree, polynomial

source

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

polynomial.is_separable_contraction q f g = (g.separable ∧ ∃ (m : ℕ), ⇑(polynomial.expand F (q ^ m)) g = f)

source

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

polynomial.has_separable_contraction q f = ∃ (g : polynomial F), polynomial.is_separable_contraction q f g

source

noncomputable def polynomial.has_separable_contraction.contraction {F : Type u_1} [comm_semiring F] {q : ℕ} {f : polynomial F} (hf : polynomial.has_separable_contraction q f) :

polynomial F

A choice of a separable contraction.

Equations

hf.contraction = classical.some hf

source

noncomputable def polynomial.has_separable_contraction.degree {F : Type u_1} [comm_semiring F] {q : ℕ} {f : polynomial F} (hf : polynomial.has_separable_contraction q f) :

ℕ

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

Equations

hf.degree = hf.contraction.nat_degree

source

theorem polynomial.is_separable_contraction.dvd_degree' {F : Type u_1} [comm_semiring F] {q : ℕ} {f g : polynomial F} (hf : polynomial.is_separable_contraction q f g) :

∃ (m : ℕ), g.nat_degree * q ^ m = f.nat_degree

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

source

theorem polynomial.has_separable_contraction.dvd_degree' {F : Type u_1} [comm_semiring F] {q : ℕ} {f : polynomial F} (hf : polynomial.has_separable_contraction q f) :

∃ (m : ℕ), hf.degree * q ^ m = f.nat_degree

source

theorem polynomial.has_separable_contraction.dvd_degree {F : Type u_1} [comm_semiring F] {q : ℕ} {f : polynomial F} (hf : polynomial.has_separable_contraction q f) :

hf.degree ∣ f.nat_degree

The separable degree divides the degree.

source

theorem polynomial.has_separable_contraction.eq_degree {F : Type u_1} [comm_semiring F] {f : polynomial F} (hf : polynomial.has_separable_contraction 1 f) :

hf.degree = f.nat_degree

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

source

theorem irreducible.has_separable_contraction {F : Type u_1} [field F] (q : ℕ) [hF : exp_char F q] (f : polynomial F) (irred : irreducible f) :

polynomial.has_separable_contraction q f

Every irreducible polynomial can be contracted to a separable polynomial. https://stacks.math.columbia.edu/tag/09H0

source

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) :

g.nat_degree = g'.nat_degree

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

source

theorem polynomial.is_separable_contraction.degree_eq {F : Type u_1} [field F] (q : ℕ) {f : polynomial F} (hf : polynomial.has_separable_contraction q f) [hF : exp_char F q] (g : polynomial F) (hg : polynomial.is_separable_contraction q f g) :

g.nat_degree = hf.degree

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