mathlib documentation

field_theory.separable

Separable polynomials

We define a polynomial to be separable if it is coprime with its derivative. We prove basic properties about separable polynomials here.

Main definitions

def polynomial.separable {R : Type u} [comm_semiring R] :
polynomial R → Prop

A polynomial is separable iff it is coprime with its derivative.

Equations
theorem polynomial.separable_def' {R : Type u} [comm_semiring R] (f : polynomial R) :
f.separable ∃ (a b : polynomial R), a * f + b * f.derivative = 1

theorem polynomial.separable_one {R : Type u} [comm_semiring R] :

theorem polynomial.separable_C {R : Type u} [comm_semiring R] (r : R) :

theorem polynomial.separable.of_mul_left {R : Type u} [comm_semiring R] {f g : polynomial R} :
(f * g).separable → f.separable

theorem polynomial.separable.of_mul_right {R : Type u} [comm_semiring R] {f g : polynomial R} :
(f * g).separable → g.separable

theorem polynomial.separable.of_dvd {R : Type u} [comm_semiring R] {f g : polynomial R} :
f.separableg f → g.separable

theorem polynomial.separable_gcd_left {F : Type u_1} [field F] {f : polynomial F} (hf : f.separable) (g : polynomial F) :

theorem polynomial.separable_gcd_right {F : Type u_1} [field F] {g : polynomial F} (f : polynomial F) :

theorem polynomial.separable.is_coprime {R : Type u} [comm_semiring R] {f g : polynomial R} :
(f * g).separableis_coprime f g

theorem polynomial.separable.of_pow' {R : Type u} [comm_semiring R] {f : polynomial R} {n : } :
(f ^ n).separableis_unit f f.separable n = 1 n = 0

theorem polynomial.separable.of_pow {R : Type u} [comm_semiring R] {f : polynomial R} (hf : ¬is_unit f) {n : } :
n 0(f ^ n).separablef.separable n = 1

theorem polynomial.separable.map {R : Type u} [comm_semiring R] {S : Type v} [comm_semiring S] {p : polynomial R} (h : p.separable) {f : R →+* S} :

def polynomial.expand (R : Type u) [comm_semiring R] :

Expand the polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.

Equations
theorem polynomial.expand_eq_sum {R : Type u} [comm_semiring R] (p : ) {f : polynomial R} :
(polynomial.expand R p) f = finsupp.sum f (λ (e : ) (a : R), (polynomial.C a) * (polynomial.X ^ p) ^ e)

@[simp]
theorem polynomial.expand_C {R : Type u} [comm_semiring R] (p : ) (r : R) :

@[simp]

@[simp]
theorem polynomial.expand_monomial {R : Type u} [comm_semiring R] (p q : ) (r : R) :

theorem polynomial.expand_expand {R : Type u} [comm_semiring R] (p q : ) (f : polynomial R) :

theorem polynomial.expand_mul {R : Type u} [comm_semiring R] (p q : ) (f : polynomial R) :

@[simp]
theorem polynomial.expand_one {R : Type u} [comm_semiring R] (f : polynomial R) :

theorem polynomial.expand_pow {R : Type u} [comm_semiring R] (p q : ) (f : polynomial R) :

theorem polynomial.coeff_expand {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
((polynomial.expand R p) f).coeff n = ite (p n) (f.coeff (n / p)) 0

@[simp]
theorem polynomial.coeff_expand_mul {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
((polynomial.expand R p) f).coeff (n * p) = f.coeff n

@[simp]
theorem polynomial.coeff_expand_mul' {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) (f : polynomial R) (n : ) :
((polynomial.expand R p) f).coeff (p * n) = f.coeff n

theorem polynomial.expand_eq_map_domain {R : Type u} [comm_semiring R] (p : ) (f : polynomial R) :
(polynomial.expand R p) f = finsupp.map_domain (λ (_x : ), _x * p) f

theorem polynomial.expand_inj {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) {f g : polynomial R} :

theorem polynomial.expand_eq_zero {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) {f : polynomial R} :
(polynomial.expand R p) f = 0 f = 0

theorem polynomial.expand_eq_C {R : Type u} [comm_semiring R] {p : } (hp : 0 < p) {f : polynomial R} {r : R} :

theorem polynomial.nat_degree_expand {R : Type u} [comm_semiring R] (p : ) (f : polynomial R) :

theorem polynomial.map_expand {R : Type u} [comm_semiring R] {S : Type v} [comm_semiring S] {p : } (hp : 0 < p) {f : R →+* S} {q : polynomial R} :

theorem polynomial.separable.mul {R : Type u} [comm_ring R] {f g : polynomial R} :
f.separableg.separableis_coprime f g(f * g).separable

theorem polynomial.separable_prod' {R : Type u} [comm_ring R] {ι : Type u_1} {f : ι → polynomial R} {s : finset ι} :
(∀ (x : ι), x s∀ (y : ι), y sx yis_coprime (f x) (f y))(∀ (x : ι), x s(f x).separable)(∏ (x : ι) in s, f x).separable

theorem polynomial.separable_prod {R : Type u} [comm_ring R] {ι : Type u_1} [fintype ι] {f : ι → polynomial R} :
pairwise (is_coprime on f)(∀ (x : ι), (f x).separable)(∏ (x : ι), f x).separable

theorem polynomial.separable.inj_of_prod_X_sub_C {R : Type u} [comm_ring R] [nontrivial R] {ι : Type u_1} {f : ι → R} {s : finset ι} (hfs : (∏ (i : ι) in s, (polynomial.X - polynomial.C (f i))).separable) {x y : ι} :
x sy sf x = f yx = y

theorem polynomial.separable.injective_of_prod_X_sub_C {R : Type u} [comm_ring R] [nontrivial R] {ι : Type u_1} [fintype ι] {f : ι → R} :

theorem polynomial.is_unit_of_self_mul_dvd_separable {R : Type u} [comm_ring R] {p q : polynomial R} :
p.separableq * q pis_unit q

theorem polynomial.separable_map {F : Type u} [field F] {K : Type v} [field K] (f : F →+* K) {p : polynomial F} :

def polynomial.contract {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] :

The opposite of expand: sends ∑ aₙ xⁿᵖ to ∑ aₙ xⁿ.

Equations
theorem polynomial.coeff_contract {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] (f : polynomial F) (n : ) :

theorem polynomial.of_irreducible_expand {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] {f : polynomial F} :

theorem polynomial.of_irreducible_expand_pow {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] {f : polynomial F} {n : } :

theorem polynomial.expand_char {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] (f : polynomial F) :

theorem polynomial.map_expand_pow_char {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] (f : polynomial F) (n : ) :
polynomial.map (frobenius F p ^ n) ((polynomial.expand F (p ^ n)) f) = f ^ p ^ n

theorem polynomial.expand_contract {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] {f : polynomial F} :

theorem polynomial.separable_or {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] {f : polynomial F} :

theorem polynomial.exists_separable_of_irreducible {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] {f : polynomial F} :
irreducible ff 0(∃ (n : ) (g : polynomial F), g.separable (polynomial.expand F (p ^ n)) g = f)

theorem polynomial.is_unit_or_eq_zero_of_separable_expand {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] {f : polynomial F} (n : ) :
((polynomial.expand F (p ^ n)) f).separableis_unit f n = 0

theorem polynomial.unique_separable_of_irreducible {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] {f : polynomial F} (hf : irreducible f) (hf0 : f 0) (n₁ : ) (g₁ : polynomial F) (hg₁ : g₁.separable) (hgf₁ : (polynomial.expand F (p ^ n₁)) g₁ = f) (n₂ : ) (g₂ : polynomial F) :
g₂.separable(polynomial.expand F (p ^ n₂)) g₂ = fn₁ = n₂ g₁ = g₂

theorem polynomial.separable_prod_X_sub_C_iff' {F : Type u} [field F] {ι : Type u_1} {f : ι → F} {s : finset ι} :
(∏ (i : ι) in s, (polynomial.X - polynomial.C (f i))).separable ∀ (x : ι), x s∀ (y : ι), y sf x = f yx = y

theorem polynomial.separable_prod_X_sub_C_iff {F : Type u} [field F] {ι : Type u_1} [fintype ι] {f : ι → F} :

theorem polynomial.nodup_of_separable_prod {F : Type u} [field F] {s : multiset F} :

theorem polynomial.multiplicity_le_one_of_seperable {F : Type u} [field F] {p q : polynomial F} :

theorem polynomial.root_multiplicity_le_one_of_seperable {F : Type u} [field F] {p : polynomial F} (hp : p 0) (hsep : p.separable) (x : F) :

theorem polynomial.count_roots_le_one {F : Type u} [field F] {p : polynomial F} (hsep : p.separable) (x : F) :

theorem polynomial.nodup_roots {F : Type u} [field F] {p : polynomial F} :

theorem polynomial.eq_X_sub_C_of_separable_of_root_eq {F : Type u} [field F] {K : Type v} [field K] {i : F →+* K} {x : F} {h : polynomial F} :
h 0h.separablepolynomial.eval x h = 0polynomial.splits i h(∀ (y : K), y (polynomial.map i h).rootsy = i x)h = (polynomial.C h.leading_coeff) * (polynomial.X - polynomial.C x)

theorem irreducible.separable {F : Type u} [field F] [char_zero F] {f : polynomial F} :
irreducible ff 0 → f.separable

@[class]
def is_separable (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] :
Prop

Typeclass for separable field extension: K is a separable field extension of F iff the minimal polynomial of every x : K is separable.

Equations
Instances
theorem is_separable_tower_top_of_is_separable {F : Type u_1} {E : Type u_2} (K : Type u_3) [field F] [field K] [field E] [algebra F K] [algebra F E] [algebra K E] [is_scalar_tower F K E] :

theorem is_separable_tower_bot_of_is_separable {F : Type u_1} {E : Type u_2} (K : Type u_3) [field F] [field K] [field E] [algebra F K] [algebra F E] [algebra K E] [is_scalar_tower F K E] :