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
polynomial.separable f: a polynomialfis separable iff it is coprime with its derivative.polynomial.expand R p f: expand the polynomialfwith coefficients in a commutative semiringRby a factor of p, soexpand R p (∑ aₙ xⁿ)is∑ aₙ xⁿᵖ.polynomial.contract p f: the opposite ofexpand, so it sends∑ aₙ xⁿᵖto∑ aₙ xⁿ.
A polynomial is separable iff it is coprime with its derivative.
Equations
- f.separable = is_coprime f f.derivative
theorem
polynomial.separable_def
{R : Type u}
[comm_semiring R]
(f : polynomial R) :
f.separable ↔ is_coprime f f.derivative
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_C
{R : Type u}
[comm_semiring R]
(r : R) :
(⇑polynomial.C r).separable ↔ is_unit r
theorem
polynomial.separable.is_coprime
{R : Type u}
[comm_semiring R]
{f g : polynomial R} :
(f * g).separable → is_coprime f g
theorem
polynomial.separable.of_pow
{R : Type u}
[comm_semiring R]
{f : polynomial R}
(hf : ¬is_unit f)
{n : ℕ} :
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
Expand the polynomial by a factor of p, so ∑ aₙ xⁿ becomes ∑ aₙ xⁿᵖ.
Equations
- polynomial.expand R p = {to_fun := (polynomial.eval₂_ring_hom polynomial.C (polynomial.X ^ p)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}
theorem
polynomial.coe_expand
(R : Type u)
[comm_semiring R]
(p : ℕ) :
⇑(polynomial.expand R p) = polynomial.eval₂ polynomial.C (polynomial.X ^ p)
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) :
⇑(polynomial.expand R p) (⇑polynomial.C r) = ⇑polynomial.C r
@[simp]
theorem
polynomial.expand_X
{R : Type u}
[comm_semiring R]
(p : ℕ) :
⇑(polynomial.expand R p) polynomial.X = polynomial.X ^ p
@[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
theorem
polynomial.expand_expand
{R : Type u}
[comm_semiring R]
(p q : ℕ)
(f : polynomial R) :
⇑(polynomial.expand R p) (⇑(polynomial.expand R q) f) = ⇑(polynomial.expand R (p * q)) f
theorem
polynomial.expand_mul
{R : Type u}
[comm_semiring R]
(p q : ℕ)
(f : polynomial R) :
⇑(polynomial.expand R (p * q)) f = ⇑(polynomial.expand R p) (⇑(polynomial.expand R q) f)
@[simp]
theorem
polynomial.expand_one
{R : Type u}
[comm_semiring R]
(f : polynomial R) :
⇑(polynomial.expand R 1) f = f
theorem
polynomial.expand_pow
{R : Type u}
[comm_semiring R]
(p q : ℕ)
(f : polynomial R) :
⇑(polynomial.expand R (p ^ q)) f = ⇑(polynomial.expand R p)^[q] f
theorem
polynomial.derivative_expand
{R : Type u}
[comm_semiring R]
(p : ℕ)
(f : polynomial R) :
(⇑(polynomial.expand R p) f).derivative = ⇑(polynomial.expand R p) f.derivative * (↑p * polynomial.X ^ (p - 1))
theorem
polynomial.coeff_expand
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
(f : polynomial R)
(n : ℕ) :
@[simp]
theorem
polynomial.coeff_expand_mul
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
(f : polynomial R)
(n : ℕ) :
@[simp]
theorem
polynomial.coeff_expand_mul'
{R : Type u}
[comm_semiring R]
{p : ℕ}
(hp : 0 < p)
(f : polynomial R)
(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} :
⇑(polynomial.expand R p) f = ⇑(polynomial.expand R p) g ↔ f = g
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} :
⇑(polynomial.expand R p) f = ⇑polynomial.C r ↔ f = ⇑polynomial.C r
theorem
polynomial.nat_degree_expand
{R : Type u}
[comm_semiring R]
(p : ℕ)
(f : polynomial R) :
(⇑(polynomial.expand R p) f).nat_degree = f.nat_degree * p
theorem
polynomial.separable.mul
{R : Type u}
[comm_ring R]
{f g : polynomial R} :
f.separable → g.separable → 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 ι} :
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) → (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 : ι} :
theorem
polynomial.separable.injective_of_prod_X_sub_C
{R : Type u}
[comm_ring R]
[nontrivial R]
{ι : Type u_1}
[fintype ι]
{f : ι → R} :
(finset.univ.prod (λ (i : ι), polynomial.X - ⇑polynomial.C (f i))).separable → function.injective f
theorem
polynomial.is_unit_of_self_mul_dvd_separable
{R : Type u}
[comm_ring R]
{p q : polynomial R} :
theorem
polynomial.is_local_ring_hom_expand
(R : Type u)
[integral_domain R]
{p : ℕ} :
0 < p → is_local_ring_hom ↑(polynomial.expand R p)
theorem
polynomial.separable_iff_derivative_ne_zero
{F : Type u}
[field F]
{f : polynomial F} :
irreducible f → (f.separable ↔ f.derivative ≠ 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
def
polynomial.contract
{F : Type u}
[field F]
(p : ℕ)
[hp : fact (nat.prime p)] :
polynomial F → polynomial F
The opposite of expand: sends ∑ aₙ xⁿᵖ to ∑ aₙ xⁿ.
theorem
polynomial.coeff_contract
{F : Type u}
[field F]
(p : ℕ)
[hp : fact (nat.prime p)]
(f : polynomial F)
(n : ℕ) :
(polynomial.contract p f).coeff n = f.coeff (n * p)
theorem
polynomial.of_irreducible_expand
{F : Type u}
[field F]
(p : ℕ)
[hp : fact (nat.prime p)]
{f : polynomial F} :
irreducible (⇑(polynomial.expand F p) f) → irreducible f
theorem
polynomial.of_irreducible_expand_pow
{F : Type u}
[field F]
(p : ℕ)
[hp : fact (nat.prime p)]
{f : polynomial F}
{n : ℕ} :
irreducible (⇑(polynomial.expand F (p ^ n)) f) → irreducible f
theorem
polynomial.expand_contract
{F : Type u}
[field F]
(p : ℕ)
[hp : fact (nat.prime p)]
[HF : char_p F p]
{f : polynomial F} :
f.derivative = 0 → ⇑(polynomial.expand F p) (polynomial.contract p f) = f
theorem
polynomial.separable_or
{F : Type u}
[field F]
(p : ℕ)
[hp : fact (nat.prime p)]
[HF : char_p F p]
{f : polynomial F} :
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 : ℕ)
[hp : fact (nat.prime p)]
[HF : char_p F p]
{f : polynomial F} :
irreducible f → f ≠ 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 : ℕ)
[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) :
theorem
polynomial.separable_prod_X_sub_C_iff'
{F : Type u}
[field F]
{ι : Type u_1}
{f : ι → F}
{s : finset ι} :
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.nodup_of_separable_prod
{F : Type u}
[field F]
{s : multiset F} :
(multiset.map (λ (a : F), polynomial.X - ⇑polynomial.C a) s).prod.separable → s.nodup
theorem
polynomial.eq_prod_roots_of_separable
{F : Type u}
[field F]
{K : Type v}
[field K]
{p : polynomial F}
{i : F →+* K} :
p.separable → polynomial.splits i p → polynomial.map i p = ⇑polynomial.C (⇑i p.leading_coeff) * (polynomial.map i p).roots.prod (λ (a : K), polynomial.X - ⇑polynomial.C a)
theorem
polynomial.nat_degree_separable_eq_card_roots
{F : Type u}
[field F]
{K : Type v}
[field K]
{p : polynomial F}
{i : F →+* K} :
p.separable → polynomial.splits i p → p.nat_degree = (polynomial.map i p).roots.card
theorem
polynomial.degree_separable_eq_card_roots
{F : Type u}
[field F]
{K : Type v}
[field K]
{p : polynomial F}
{i : F →+* K} :
p ≠ 0 → p.separable → polynomial.splits i p → p.degree = ↑((polynomial.map i p).roots.card)
theorem
irreducible.separable
{F : Type u}
[field F]
[char_zero F]
{f : polynomial F} :
irreducible f → f ≠ 0 → f.separable
@[class]
Typeclass for separable field extension: K is a separable field extension of F iff
the minimal polynomial of every x : K is separable.
Equations
- is_separable F K = ∀ (x : K), ∃ (H : is_integral F x), (minimal_polynomial H).separable