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] (f : 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 * polynomial.derivative f = 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} (h : (f * g).separable) :
theorem polynomial.separable.of_mul_right {R : Type u} [comm_semiring R] {f g : polynomial R} (h : (f * g).separable) :
theorem polynomial.separable.of_dvd {R : Type u} [comm_semiring R] {f g : polynomial R} (hf : f.separable) (hfg : g f) :
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) (hg : g.separable) :
theorem polynomial.separable.is_coprime {R : Type u} [comm_semiring R] {f g : polynomial R} (h : (f * g).separable) :
theorem polynomial.separable.of_pow' {R : Type u} [comm_semiring R] {f : polynomial R} {n : } (h : (f ^ n).separable) :
is_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 : } (hn : n 0) (hfs : (f ^ n).separable) :
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] (p : ) :

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 = f.sum (λ (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_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.expand_injective {R : Type u} [comm_semiring R] {n : } (hn : 0 < n) :

Expansion is injective.

theorem polynomial.separable.mul {R : Type u} [comm_ring R] {f g : polynomial R} (hf : f.separable) (hg : g.separable) (h : is_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} (h1 : pairwise (is_coprime on f)) (h2 : ∀ (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 : ι} (hx : x s) (hy : y s) (hfxy : f x = f y) :
x = y
theorem polynomial.separable.injective_of_prod_X_sub_C {R : Type u} [comm_ring R] [nontrivial R] {ι : Type u_1} [fintype ι] {f : ι → R} (hfs : (∏ (i : ι), (polynomial.X - polynomial.C (f i))).separable) :
theorem polynomial.is_unit_of_self_mul_dvd_separable {R : Type u} [comm_ring R] {p q : polynomial R} (hp : p.separable) (hq : q * q p) :
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 : ) (f : polynomial F) :

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} (hf : irreducible ((polynomial.expand F p) 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} (hf : polynomial.derivative f = 0) :
theorem polynomial.separable_or {F : Type u} [field F] (p : ) [hp : fact (nat.prime p)] [HF : char_p F p] {f : polynomial F} (hf : irreducible 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} (hf : irreducible f) (hf0 : f 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 : ) (hf : ((polynomial.expand F (p ^ n)) f).separable) :
is_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) (hg₂ : g₂.separable) (hgf₂ : (polynomial.expand F (p ^ n₂)) g₂ = f) :
n₁ = 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} (hs : (multiset.map (λ (a : F), polynomial.X - polynomial.C a) s).prod.separable) :
theorem polynomial.multiplicity_le_one_of_separable {F : Type u} [field F] {p q : polynomial F} (hq : ¬is_unit q) (hsep : p.separable) :
theorem polynomial.separable.squarefree {F : Type u} [field F] {p : polynomial F} (hsep : p.separable) :
theorem polynomial.separable_X_pow_sub_C {F : Type u} [field F] {n : } (a : F) (hn : n 0) (ha : a 0) :

If n ≠ 0 in F, then X ^ n - a is separable for any a ≠ 0.

theorem polynomial.squarefree_X_pow_sub_C {F : Type u} [field F] {n : } (a : F) (hn : n 0) (ha : a 0) :

If n ≠ 0 in F, then X ^ n - a is squarefree for any a ≠ 0.

theorem polynomial.root_multiplicity_le_one_of_separable {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} (hsep : p.separable) :
theorem polynomial.card_root_set_eq_nat_degree {F : Type u} [field F] {K : Type v} [field K] [algebra F K] {p : polynomial F} (hsep : p.separable) (hsplit : polynomial.splits (algebra_map F K) p) :
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_ne_zero : h 0) (h_sep : h.separable) (h_root : polynomial.eval x h = 0) (h_splits : polynomial.splits i h) (h_roots : ∀ (y : K), y (polynomial.map i h).rootsy = i x) :
theorem polynomial.exists_finset_of_splits {F : Type u} [field F] {K : Type v} [field K] (i : F →+* K) {f : polynomial F} (sep : f.separable) (sp : polynomial.splits i f) :
∃ (s : finset K), polynomial.map i f = (polynomial.C (i f.leading_coeff)) * ∏ (a : K) in s, (polynomial.X - polynomial.C a)
theorem irreducible.separable {F : Type u} [field F] [char_zero F] {f : polynomial F} (hf : irreducible f) :
@[class]
structure is_separable (F : Type u_1) (K : Type u_2) [comm_ring F] [ring 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.

We define this for general (commutative) rings and only assume F and K are fields if this is needed for a proof.

Instances
theorem is_separable.is_integral (F : Type u_1) {K : Type u_2} [comm_ring F] [ring K] [algebra F K] [is_separable F K] (x : K) :
theorem is_separable.separable (F : Type u_1) {K : Type u_2} [comm_ring F] [ring K] [algebra F K] [is_separable F K] (x : K) :
theorem is_separable_iff {F : Type u_1} {K : Type u_2} [comm_ring F] [ring K] [algebra F K] :
is_separable F K ∀ (x : K), is_integral F x (minpoly F x).separable
@[instance]
def is_separable_self (F : Type u_1) [field F] :
@[instance]
def is_separable.of_finite (F : Type u_1) (K : Type u_2) [field F] [field K] [algebra F K] [finite_dimensional F K] [char_zero F] :

A finite field extension in characteristic 0 is separable.

theorem is_separable_tower_top_of_is_separable (F : Type u_1) (K : Type u_2) (E : Type u_3) [field F] [field K] [field E] [algebra F K] [algebra F E] [algebra K E] [is_scalar_tower F K E] [is_separable F E] :
theorem is_separable_tower_bot_of_is_separable (F : Type u_1) (K : Type u_2) (E : Type u_3) [field F] [field K] [field E] [algebra F K] [algebra F E] [algebra K E] [is_scalar_tower F K E] [h : is_separable F E] :
theorem is_separable.of_alg_hom (F : Type u_1) {E : Type u_3} [field F] [field E] [algebra F E] (E' : Type u_2) [field E'] [algebra F E'] (f : E →ₐ[F] E') [is_separable F E'] :
theorem alg_hom.card_of_power_basis {S : Type u_2} [comm_ring S] {K : Type u_4} {L : Type u_5} [field K] [field L] [algebra K S] [algebra K L] (pb : power_basis K S) (h_sep : (minpoly K pb.gen).separable) (h_splits : polynomial.splits (algebra_map K L) (minpoly K pb.gen)) :