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 #

source
def polynomial.separable {R : Type u} [comm_semiring R] (f : R[X]) :
Prop

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

Equations
source
theorem polynomial.separable_def {R : Type u} [comm_semiring R] (f : R[X]) :
f.separable ↔ is_coprime f (⇑polynomial.derivative f)
source
theorem polynomial.separable_def' {R : Type u} [comm_semiring R] (f : R[X]) :
f.separable ↔ ∃ (a b : R[X]), a * f + b * ⇑polynomial.derivative f = 1
source
theorem polynomial.not_separable_zero {R : Type u} [comm_semiring R] [nontrivial R] :
¬0.separable
source
theorem polynomial.separable_one {R : Type u} [comm_semiring R] :
1.separable
source
theorem polynomial.separable_of_subsingleton {R : Type u} [comm_semiring R] [subsingleton R] (f : R[X]) :
f.separable
source
theorem polynomial.separable_X_add_C {R : Type u} [comm_semiring R] (a : R) :
(polynomial.X + ⇑polynomial.C a).separable
source
theorem polynomial.separable_X {R : Type u} [comm_semiring R] :
polynomial.X.separable
source
theorem polynomial.separable_C {R : Type u} [comm_semiring R] (r : R) :
(⇑polynomial.C r).separable ↔ is_unit r
source
theorem polynomial.separable.of_mul_left {R : Type u} [comm_semiring R] {f g : R[X]} (h : (f * g).separable) :
f.separable
source
theorem polynomial.separable.of_mul_right {R : Type u} [comm_semiring R] {f g : R[X]} (h : (f * g).separable) :
g.separable
source
theorem polynomial.separable.of_dvd {R : Type u} [comm_semiring R] {f g : R[X]} (hf : f.separable) (hfg : g ∣ f) :
g.separable
source
theorem polynomial.separable_gcd_left {F : Type u_1} [field F] {f : F[X]} (hf : f.separable) (g : F[X]) :
(euclidean_domain.gcd f g).separable
source
theorem polynomial.separable_gcd_right {F : Type u_1} [field F] {g : F[X]} (f : F[X]) (hg : g.separable) :
(euclidean_domain.gcd f g).separable
source
theorem polynomial.separable.is_coprime {R : Type u} [comm_semiring R] {f g : R[X]} (h : (f * g).separable) :
is_coprime f g
source
theorem polynomial.separable.of_pow' {R : Type u} [comm_semiring R] {f : R[X]} {n : ℕ} (h : (f ^ n).separable) :
is_unit f ∨ f.separable ∧ n = 1 ∨ n = 0
source
theorem polynomial.separable.of_pow {R : Type u} [comm_semiring R] {f : R[X]} (hf : ¬is_unit f) {n : ℕ} (hn : n ≠ 0) (hfs : (f ^ n).separable) :
f.separable ∧ n = 1
source
theorem polynomial.separable.map {R : Type u} [comm_semiring R] {S : Type v} [comm_semiring S] {p : R[X]} (h : p.separable) {f : R →+* S} :
(polynomial.map f p).separable
source
noncomputable def polynomial.expand (R : Type u) [comm_semiring R] (p : ℕ) :
R[X] →ₐ[R] R[X]

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

Equations
source
theorem polynomial.coe_expand (R : Type u) [comm_semiring R] (p : ℕ) :
⇑(polynomial.expand R p) = polynomial.eval₂ polynomial.C (polynomial.X ^ p)
source
theorem polynomial.expand_eq_sum {R : Type u} [comm_semiring R] (p : ℕ) {f : R[X]} :
⇑(polynomial.expand R p) f = f.sum (λ (e : ℕ) (a : R), (⇑polynomial.C a) * (polynomial.X ^ p) ^ e)
source
@[simp]
theorem polynomial.expand_C {R : Type u} [comm_semiring R] (p : ℕ) (r : R) :
⇑(polynomial.expand R p) (⇑polynomial.C r) = ⇑polynomial.C r
source
@[simp]
theorem polynomial.expand_X {R : Type u} [comm_semiring R] (p : ℕ) :
⇑(polynomial.expand R p) polynomial.X = polynomial.X ^ p
source
@[simp]
theorem polynomial.expand_monomial {R : Type u} [comm_semiring R] (p q : ℕ) (r : R) :
⇑(polynomial.expand R p) (⇑(polynomial.monomial q) r) = ⇑(polynomial.monomial (q * p)) r
source
theorem polynomial.expand_expand {R : Type u} [comm_semiring R] (p q : ℕ) (f : R[X]) :
⇑(polynomial.expand R p) (⇑(polynomial.expand R q) f) = ⇑(polynomial.expand R (p * q)) f
source
theorem polynomial.expand_mul {R : Type u} [comm_semiring R] (p q : ℕ) (f : R[X]) :
⇑(polynomial.expand R (p * q)) f = ⇑(polynomial.expand R p) (⇑(polynomial.expand R q) f)
source
@[simp]
theorem polynomial.expand_zero {R : Type u} [comm_semiring R] (f : R[X]) :
⇑(polynomial.expand R 0) f = ⇑polynomial.C (polynomial.eval 1 f)
source
@[simp]
theorem polynomial.expand_one {R : Type u} [comm_semiring R] (f : R[X]) :
⇑(polynomial.expand R 1) f = f
source
theorem polynomial.expand_pow {R : Type u} [comm_semiring R] (p q : ℕ) (f : R[X]) :
⇑(polynomial.expand R (p ^ q)) f = ⇑(polynomial.expand R p)^[q] f
source
theorem polynomial.derivative_expand {R : Type u} [comm_semiring R] (p : ℕ) (f : R[X]) :
⇑polynomial.derivative (⇑(polynomial.expand R p) f) = (⇑(polynomial.expand R p) (⇑polynomial.derivative f)) * (↑p) * polynomial.X ^ (p - 1)
source
theorem polynomial.coeff_expand {R : Type u} [comm_semiring R] {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
(⇑(polynomial.expand R p) f).coeff n = ite (p ∣ n) (f.coeff (n / p)) 0
source
@[simp]
theorem polynomial.coeff_expand_mul {R : Type u} [comm_semiring R] {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
(⇑(polynomial.expand R p) f).coeff (n * p) = f.coeff n
source
@[simp]
theorem polynomial.coeff_expand_mul' {R : Type u} [comm_semiring R] {p : ℕ} (hp : 0 < p) (f : R[X]) (n : ℕ) :
(⇑(polynomial.expand R p) f).coeff (p * n) = f.coeff n
source
theorem polynomial.expand_inj {R : Type u} [comm_semiring R] {p : ℕ} (hp : 0 < p) {f g : R[X]} :
⇑(polynomial.expand R p) f = ⇑(polynomial.expand R p) g ↔ f = g
source
theorem polynomial.expand_eq_zero {R : Type u} [comm_semiring R] {p : ℕ} (hp : 0 < p) {f : R[X]} :
⇑(polynomial.expand R p) f = 0 ↔ f = 0
source
theorem polynomial.expand_eq_C {R : Type u} [comm_semiring R] {p : ℕ} (hp : 0 < p) {f : R[X]} {r : R} :
⇑(polynomial.expand R p) f = ⇑polynomial.C r ↔ f = ⇑polynomial.C r
source
theorem polynomial.nat_degree_expand {R : Type u} [comm_semiring R] (p : ℕ) (f : R[X]) :
(⇑(polynomial.expand R p) f).nat_degree = (f.nat_degree) * p
source
theorem polynomial.monic.expand {R : Type u} [comm_semiring R] {p : ℕ} {f : R[X]} (hp : 0 < p) (h : f.monic) :
(⇑(polynomial.expand R p) f).monic
source
theorem polynomial.map_expand {R : Type u} [comm_semiring R] {S : Type v} [comm_semiring S] {p : ℕ} {f : R →+* S} {q : R[X]} :
polynomial.map f (⇑(polynomial.expand R p) q) = ⇑(polynomial.expand S p) (polynomial.map f q)
source
theorem polynomial.expand_injective {R : Type u} [comm_semiring R] {n : ℕ} (hn : 0 < n) :
function.injective ⇑(polynomial.expand R n)

Expansion is injective.

source
@[simp]
theorem polynomial.expand_eval {R : Type u} [comm_semiring R] (p : ℕ) (P : R[X]) (r : R) :
polynomial.eval r (⇑(polynomial.expand R p) P) = polynomial.eval (r ^ p) P
source
theorem polynomial.is_unit_of_self_mul_dvd_separable {R : Type u} [comm_semiring R] {p q : R[X]} (hp : p.separable) (hq : q * q ∣ p) :
is_unit q
source
noncomputable def polynomial.contract {R : Type u} [comm_semiring R] (p : ℕ) (f : R[X]) :
R[X]

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

Equations
source
theorem polynomial.coeff_contract {R : Type u} [comm_semiring R] {p : ℕ} (hp : p ≠ 0) (f : R[X]) (n : ℕ) :
(polynomial.contract p f).coeff n = f.coeff (n * p)
source
theorem polynomial.contract_expand {R : Type u} [comm_semiring R] (p : ℕ) {f : R[X]} (hp : p ≠ 0) :
polynomial.contract p (⇑(polynomial.expand R p) f) = f
source
theorem polynomial.expand_contract {R : Type u} [comm_semiring R] (p : ℕ) [char_p R p] [no_zero_divisors R] {f : R[X]} (hf : ⇑polynomial.derivative f = 0) (hp : p ≠ 0) :
⇑(polynomial.expand R p) (polynomial.contract p f) = f
source
theorem polynomial.expand_char {R : Type u} [comm_semiring R] (p : ℕ) [char_p R p] [hp : fact (nat.prime p)] (f : R[X]) :
polynomial.map (frobenius R p) (⇑(polynomial.expand R p) f) = f ^ p
source
theorem polynomial.map_expand_pow_char {R : Type u} [comm_semiring R] (p : ℕ) [char_p R p] [hp : fact (nat.prime p)] (f : R[X]) (n : ℕ) :
polynomial.map (frobenius R p ^ n) (⇑(polynomial.expand R (p ^ n)) f) = f ^ p ^ n
source
theorem polynomial.multiplicity_le_one_of_separable {R : Type u} [comm_semiring R] {p q : R[X]} (hq : ¬is_unit q) (hsep : p.separable) :
multiplicity q p ≤ 1
source
theorem polynomial.separable.squarefree {R : Type u} [comm_semiring R] {p : R[X]} (hsep : p.separable) :
squarefree p
source
theorem polynomial.separable_X_sub_C {R : Type u} [comm_ring R] {x : R} :
(polynomial.X - ⇑polynomial.C x).separable
source
theorem polynomial.separable.mul {R : Type u} [comm_ring R] {f g : R[X]} (hf : f.separable) (hg : g.separable) (h : is_coprime f g) :
(f * g).separable
source
theorem polynomial.separable_prod' {R : Type u} [comm_ring R] {ι : Type u_1} {f : ι → R[X]} {s : finset ι} :
(∀ (x : ι), x ∈ s → ∀ (y : ι), y ∈ s → x ≠ y → is_coprime (f x) (f y)) → (∀ (x : ι), x ∈ s → (f x).separable) → (∏ (x : ι) in s, f x).separable
source
theorem polynomial.separable_prod {R : Type u} [comm_ring R] {ι : Type u_1} [fintype ι] {f : ι → R[X]} (h1 : pairwise (is_coprime on f)) (h2 : ∀ (x : ι), (f x).separable) :
(∏ (x : ι), f x).separable
source
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
source
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) :
function.injective f
source
theorem polynomial.nodup_of_separable_prod {R : Type u} [comm_ring R] [nontrivial R] {s : multiset R} (hs : (multiset.map (λ (a : R), polynomial.X - ⇑polynomial.C a) s).prod.separable) :
s.nodup
source
theorem polynomial.separable_X_pow_sub_C_unit {R : Type u} [comm_ring R] {n : ℕ} (u : Rˣ) (hn : is_unit ↑n) :
(polynomial.X ^ n - ⇑polynomial.C ↑u).separable

If is_unit n in a comm_ring R, then X ^ n - u is separable for any unit u.

source
theorem polynomial.root_multiplicity_le_one_of_separable {R : Type u} [comm_ring R] [nontrivial R] {p : R[X]} (hsep : p.separable) (x : R) :
polynomial.root_multiplicity x p ≤ 1
source
theorem polynomial.is_local_ring_hom_expand (R : Type u) [comm_ring R] [is_domain R] {p : ℕ} (hp : 0 < p) :
is_local_ring_hom ↑(polynomial.expand R p)
source
theorem polynomial.of_irreducible_expand {R : Type u} [comm_ring R] [is_domain R] {p : ℕ} (hp : p ≠ 0) {f : R[X]} (hf : irreducible (⇑(polynomial.expand R p) f)) :
irreducible f
source
theorem polynomial.of_irreducible_expand_pow {R : Type u} [comm_ring R] [is_domain R] {p : ℕ} (hp : p ≠ 0) {f : R[X]} {n : ℕ} :
irreducible (⇑(polynomial.expand R (p ^ n)) f) → irreducible f
source
theorem polynomial.count_roots_le_one {R : Type u} [comm_ring R] [is_domain R] {p : R[X]} (hsep : p.separable) (x : R) :
multiset.count x p.roots ≤ 1
source
theorem polynomial.nodup_roots {R : Type u} [comm_ring R] [is_domain R] {p : R[X]} (hsep : p.separable) :
p.roots.nodup
source
theorem polynomial.separable_iff_derivative_ne_zero {F : Type u} [field F] {f : F[X]} (hf : irreducible f) :
f.separable ↔ ⇑polynomial.derivative f ≠ 0
source
theorem polynomial.separable_map {F : Type u} [field F] {K : Type v} [field K] (f : F →+* K) {p : F[X]} :
(polynomial.map f p).separable ↔ p.separable
source
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 ∈ s → f x = f y → x = y
source
theorem polynomial.separable_prod_X_sub_C_iff {F : Type u} [field F] {ι : Type u_1} [fintype ι] {f : ι → F} :
(∏ (i : ι), (polynomial.X - ⇑polynomial.C (f i))).separable ↔ function.injective f
source
theorem polynomial.separable_or {F : Type u} [field F] (p : ℕ) [HF : char_p F p] {f : F[X]} (hf : irreducible f) :
f.separable ∨ ¬f.separable ∧ ∃ (g : F[X]), irreducible g ∧ ⇑(polynomial.expand F p) g = f
source
theorem polynomial.exists_separable_of_irreducible {F : Type u} [field F] (p : ℕ) [HF : char_p F p] {f : F[X]} (hf : irreducible f) (hp : p ≠ 0) :
∃ (n : ℕ) (g : F[X]), g.separable ∧ ⇑(polynomial.expand F (p ^ n)) g = f
source
theorem polynomial.is_unit_or_eq_zero_of_separable_expand {F : Type u} [field F] (p : ℕ) [HF : char_p F p] {f : F[X]} (n : ℕ) (hp : 0 < p) (hf : (⇑(polynomial.expand F (p ^ n)) f).separable) :
is_unit f ∨ n = 0
source
theorem polynomial.unique_separable_of_irreducible {F : Type u} [field F] (p : ℕ) [HF : char_p F p] {f : F[X]} (hf : irreducible f) (hp : 0 < p) (n₁ : ℕ) (g₁ : F[X]) (hg₁ : g₁.separable) (hgf₁ : ⇑(polynomial.expand F (p ^ n₁)) g₁ = f) (n₂ : ℕ) (g₂ : F[X]) (hg₂ : g₂.separable) (hgf₂ : ⇑(polynomial.expand F (p ^ n₂)) g₂ = f) :
n₁ = n₂ ∧ g₁ = g₂
source
theorem polynomial.separable_X_pow_sub_C {F : Type u} [field F] {n : ℕ} (a : F) (hn : ↑n ≠ 0) (ha : a ≠ 0) :
(polynomial.X ^ n - ⇑polynomial.C a).separable

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

source
theorem polynomial.X_pow_sub_one_separable_iff {F : Type u} [field F] {n : ℕ} :
(polynomial.X ^ n - 1).separable ↔ ↑n ≠ 0

In a field F, X ^ n - 1 is separable iff ↑n ≠ 0.

source
theorem polynomial.card_root_set_eq_nat_degree {F : Type u} [field F] {K : Type v} [field K] [algebra F K] {p : F[X]} (hsep : p.separable) (hsplit : polynomial.splits (algebra_map F K) p) :
fintype.card ↥(p.root_set K) = p.nat_degree
source
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 : F[X]} (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).roots → y = ⇑i x) :
h = (⇑polynomial.C h.leading_coeff) * (polynomial.X - ⇑polynomial.C x)
source
theorem polynomial.exists_finset_of_splits {F : Type u} [field F] {K : Type v} [field K] (i : F →+* K) {f : F[X]} (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)
source
theorem irreducible.separable {F : Type u} [field F] [char_zero F] {f : F[X]} (hf : irreducible f) :
f.separable
source
@[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
source
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) :
is_integral F x
source
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) :
(minpoly F x).separable
source
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
source
@[protected, instance]
def is_separable_self (F : Type u_1) [field F] :
is_separable F F
source
@[protected, 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] :
is_separable F K

A finite field extension in characteristic 0 is separable.

source
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] :
is_separable K E
source
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] :
is_separable F K
source
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'] :
is_separable F E
source
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)) :
fintype.card (S →ₐ[K] L) = pb.dim