Separable polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define a polynomial to be separable if it is coprime with its derivative. We prove basic properties about separable polynomials here.
Main definitions #
polynomial.separable f: a polynomialfis separable iff it is coprime with its derivative.
A polynomial is separable iff it is coprime with its derivative.
Equations
- f.separable = is_coprime f (⇑polynomial.derivative f)
theorem
polynomial.separable_def
{R : Type u}
[comm_semiring R]
(f : polynomial R) :
f.separable ↔ is_coprime f (⇑polynomial.derivative f)
theorem
polynomial.separable_of_subsingleton
{R : Type u}
[comm_semiring R]
[subsingleton R]
(f : polynomial R) :
theorem
polynomial.separable_C
{R : Type u}
[comm_semiring R]
(r : R) :
(⇑polynomial.C r).separable ↔ is_unit 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) :
is_coprime f g
theorem
polynomial.separable.of_pow'
{R : Type u}
[comm_semiring R]
{f : polynomial R}
{n : ℕ}
(h : (f ^ n).separable) :
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} :
(polynomial.map f p).separable
theorem
polynomial.is_unit_of_self_mul_dvd_separable
{R : Type u}
[comm_semiring R]
{p q : polynomial R}
(hp : p.separable)
(hq : q * q ∣ p) :
is_unit q
theorem
polynomial.multiplicity_le_one_of_separable
{R : Type u}
[comm_semiring R]
{p q : polynomial R}
(hq : ¬is_unit q)
(hsep : p.separable) :
multiplicity q p ≤ 1
theorem
polynomial.separable.squarefree
{R : Type u}
[comm_semiring R]
{p : polynomial R}
(hsep : p.separable) :
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) :
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) :
(finset.univ.prod (λ (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 : (s.prod (λ (i : ι), 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 : (finset.univ.prod (λ (i : ι), polynomial.X - ⇑polynomial.C (f i))).separable) :
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
theorem
polynomial.root_multiplicity_le_one_of_separable
{R : Type u}
[comm_ring R]
[nontrivial R]
{p : polynomial R}
(hsep : p.separable)
(x : R) :
theorem
polynomial.count_roots_le_one
{R : Type u}
[comm_ring R]
[is_domain R]
{p : polynomial R}
(hsep : p.separable)
(x : R) :
multiset.count x p.roots ≤ 1
theorem
polynomial.nodup_roots
{R : Type u}
[comm_ring R]
[is_domain R]
{p : polynomial R}
(hsep : p.separable) :
theorem
polynomial.separable_iff_derivative_ne_zero
{F : Type u}
[field F]
{f : polynomial F}
(hf : irreducible f) :
f.separable ↔ ⇑polynomial.derivative f ≠ 0
theorem
polynomial.separable_map
{F : Type u}
[field F]
{K : Type v}
[field K]
(f : F →+* K)
{p : polynomial F} :
(polynomial.map f p).separable ↔ p.separable
theorem
polynomial.separable_prod_X_sub_C_iff
{F : Type u}
[field F]
{ι : Type u_1}
[fintype ι]
{f : ι → F} :
(finset.univ.prod (λ (i : ι), polynomial.X - ⇑polynomial.C (f i))).separable ↔ function.injective f
theorem
polynomial.separable_or
{F : Type u}
[field F]
(p : ℕ)
[HF : char_p F p]
{f : polynomial F}
(hf : irreducible f) :
f.separable ∨ ¬f.separable ∧ ∃ (g : polynomial F), irreducible g ∧ ⇑(polynomial.expand F p) g = f
theorem
polynomial.exists_separable_of_irreducible
{F : Type u}
[field F]
(p : ℕ)
[HF : char_p F p]
{f : polynomial F}
(hf : irreducible f)
(hp : p ≠ 0) :
∃ (n : ℕ) (g : polynomial F), g.separable ∧ ⇑(polynomial.expand F (p ^ n)) g = f
theorem
polynomial.unique_separable_of_irreducible
{F : Type u}
[field F]
(p : ℕ)
[HF : char_p F p]
{f : polynomial F}
(hf : irreducible f)
(hp : 0 < p)
(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) :
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.
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) :
fintype.card ↥(p.root_set K) = p.nat_degree
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_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)
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) * s.prod (λ (a : K), polynomial.X - ⇑polynomial.C a)
theorem
irreducible.separable
{F : Type u}
[field F]
[char_zero F]
{f : polynomial F}
(hf : irreducible f) :
@[class]
- is_integral' : ∀ (x : K), is_integral F x
- separable' : ∀ (x : K), (minpoly F x).separable
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 of this typeclass
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
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
@[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.
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
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
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
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