Skip to content

Commit

Permalink
feat(data/polynomial/ring_division): make polynomial.roots a multis…
Browse files Browse the repository at this point in the history 
…et (#4061)

The original definition of `polynomial.roots` was basically "while ∃ x, p.is_root x { finset.insert x polynomial.roots }", so it was not
too hard to replace this with `multiset.cons`.

I tried to refactor most usages of `polynomial.roots` to talk about the multiset instead of coercing it to a finset, since that should give a bit more power to the results.
  • Loading branch information
@Vierkantor
Vierkantor committed Sep 10, 2020
1 parent 660a6c4 commit 9f55ed7
Show file tree
Hide file tree
Showing 8 changed files with 276 additions and 151 deletions.
233 changes: 149 additions & 84 deletions src/data/polynomial/ring_division.lean
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,3 @@

/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Expand Down Expand Up @@ -87,10 +86,106 @@ begin
rw [nat_degree_mul h2.1 h2.2], exact nat.le_add_right _ _
end

section roots

open multiset

local attribute [reducible] with_zero

lemma exists_finset_roots : ∀ {p : polynomial R} (hp : p ≠ 0),
∃ s : finset R, (s.card : with_bot ℕ) ≤ degree p ∧ ∀ x, x ∈ s ↔ is_root p x
lemma degree_eq_zero_of_is_unit (h : is_unit p) : degree p = 0 :=
let ⟨q, hq⟩ := is_unit_iff_dvd_one.1 h in
have hp0 : p ≠ 0, from λ hp0, by simpa [hp0] using hq,
have hq0 : q ≠ 0, from λ hp0, by simpa [hp0] using hq,
have nat_degree (1 : polynomial R) = nat_degree (p * q),
from congr_arg _ hq,
by rw [nat_degree_one, nat_degree_mul hp0 hq0, eq_comm,
_root_.add_eq_zero_iff, ← with_bot.coe_eq_coe,
← degree_eq_nat_degree hp0] at this;
exact this.1

@[simp] lemma degree_coe_units (u : units (polynomial R)) :
degree (u : polynomial R) = 0 :=
degree_eq_zero_of_is_unit ⟨u, rfl⟩

theorem prime_X_sub_C {r : R} : prime (X - C r) :=
⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C,
λ _ _, by { simp_rw [dvd_iff_is_root, is_root.def, eval_mul, mul_eq_zero], exact id }⟩

theorem prime_X : prime (X : polynomial R) :=
by { convert (prime_X_sub_C : prime (X - C 0 : polynomial R)), simp }

lemma prime_of_degree_eq_one_of_monic (hp1 : degree p = 1)
(hm : monic p) : prime p :=
have p = X - C (- p.coeff 0),
by simpa [hm.leading_coeff] using eq_X_add_C_of_degree_eq_one hp1,
this.symm ▸ prime_X_sub_C

theorem irreducible_X_sub_C (r : R) : irreducible (X - C r) :=
irreducible_of_prime prime_X_sub_C

theorem irreducible_X : irreducible (X : polynomial R) :=
irreducible_of_prime prime_X

lemma irreducible_of_degree_eq_one_of_monic (hp1 : degree p = 1)
(hm : monic p) : irreducible p :=
irreducible_of_prime (prime_of_degree_eq_one_of_monic hp1 hm)

theorem eq_of_monic_of_associated (hp : p.monic) (hq : q.monic) (hpq : associated p q) : p = q :=
begin
obtain ⟨u, hu⟩ := hpq,
unfold monic at hp hq,
rw eq_C_of_degree_le_zero (le_of_eq $ degree_coe_units _) at hu,
rw [← hu, leading_coeff_mul, hp, one_mul, leading_coeff_C] at hq,
rwa [hq, C_1, mul_one] at hu
end

@[simp] lemma root_multiplicity_zero {x : R} : root_multiplicity x 0 = 0 := dif_pos rfl

lemma root_multiplicity_eq_zero {p : polynomial R} {x : R} (h : ¬ is_root p x) :
root_multiplicity x p = 0 :=
begin
rw root_multiplicity_eq_multiplicity,
split_ifs, { refl },
rw [← enat.coe_inj, enat.coe_get, multiplicity.multiplicity_eq_zero_of_not_dvd, enat.coe_zero],
intro hdvd,
exact h (dvd_iff_is_root.mp hdvd)
end

lemma root_multiplicity_pos {p : polynomial R} (hp : p ≠ 0) {x : R} :
0 < root_multiplicity x p ↔ is_root p x :=
begin
rw [← dvd_iff_is_root, root_multiplicity_eq_multiplicity, dif_neg hp,
← enat.coe_lt_coe, enat.coe_get],
exact multiplicity.dvd_iff_multiplicity_pos
end

lemma root_multiplicity_mul {p q : polynomial R} {x : R} (hpq : p * q ≠ 0) :
root_multiplicity x (p * q) = root_multiplicity x p + root_multiplicity x q :=
begin
have hp : p ≠ 0 := left_ne_zero_of_mul hpq,
have hq : q ≠ 0 := right_ne_zero_of_mul hpq,
rw [root_multiplicity_eq_multiplicity (p * q), dif_neg hpq,
root_multiplicity_eq_multiplicity p, dif_neg hp,
root_multiplicity_eq_multiplicity q, dif_neg hq,
@multiplicity.mul' _ _ _ (X - C x) _ _ prime_X_sub_C],
end

lemma root_multiplicity_X_sub_C_self {x : R} :
root_multiplicity x (X - C x) = 1 :=
by rw [root_multiplicity_eq_multiplicity, dif_neg (X_sub_C_ne_zero x),
multiplicity.get_multiplicity_self]

lemma root_multiplicity_X_sub_C {x y : R} :
root_multiplicity x (X - C y) = if x = y then 1 else 0 :=
begin
split_ifs with hxy,
{ rw hxy,
exact root_multiplicity_X_sub_C_self },
exact root_multiplicity_eq_zero (mt root_X_sub_C.mp (ne.symm hxy))
end

lemma exists_multiset_roots : ∀ {p : polynomial R} (hp : p ≠ 0),
∃ s : multiset R, (s.card : with_bot ℕ) ≤ degree p ∧ ∀ a, s.count a = root_multiplicity a p
| p := λ hp, by haveI := classical.prop_decidable (∃ x, is_root p x); exact
if h : ∃ x, is_root p x
then
Expand All @@ -101,44 +196,47 @@ then
have wf : degree (p /ₘ _) < degree p :=
degree_div_by_monic_lt _ (monic_X_sub_C x) hp
((degree_X_sub_C x).symm ▸ dec_trivial),
let ⟨t, htd, htr⟩ := @exists_finset_roots (p /ₘ (X - C x)) hd0 in
let ⟨t, htd, htr⟩ := @exists_multiset_roots (p /ₘ (X - C x)) hd0 in
have hdeg : degree (X - C x) ≤ degree p := begin
rw [degree_X_sub_C, degree_eq_nat_degree hp],
rw degree_eq_nat_degree hp at hpd,
exact with_bot.coe_le_coe.2 (with_bot.coe_lt_coe.1 hpd)
end,
have hdiv0 : p /ₘ (X - C x) ≠ 0 := mt (div_by_monic_eq_zero_iff (monic_X_sub_C x)
(ne_zero_of_monic (monic_X_sub_C x))).1 $ not_lt.2 hdeg,
⟨insert x t, calc (card (insert x t) : with_bot ℕ) ≤ card t + 1 :
with_bot.coe_le_coe.2 $ finset.card_insert_le _ _
⟨x :: t, calc (card (x :: t) : with_bot ℕ) = t.card + 1 :
by exact_mod_cast card_cons _ _
... ≤ degree p :
by rw [← degree_add_div_by_monic (monic_X_sub_C x) hdeg,
degree_X_sub_C, add_comm];
exact add_le_add (le_refl (1 : with_bot ℕ)) htd,
begin
assume y,
rw [mem_insert, htr, eq_comm, ← root_X_sub_C],
conv {to_rhs, rw ← mul_div_by_monic_eq_iff_is_root.2 hx},
exact ⟨λ h, or.cases_on h (root_mul_right_of_is_root _) (root_mul_left_of_is_root _),
root_or_root_of_root_mul⟩
assume a,
conv_rhs { rw ← mul_div_by_monic_eq_iff_is_root.mpr hx },
rw [root_multiplicity_mul (mul_ne_zero (X_sub_C_ne_zero _) hdiv0),
root_multiplicity_X_sub_C, ← htr a],
split_ifs with ha,
{ rw [ha, count_cons_self, nat.succ_eq_add_one, add_comm] },
{ rw [count_cons_of_ne ha, zero_add] },
end⟩
else
⟨∅, (degree_eq_nat_degree hp).symm ▸ with_bot.coe_le_coe.2 (nat.zero_le _),
by simpa only [not_mem_empty, false_iff, not_exists] using h⟩
⟨0, (degree_eq_nat_degree hp).symm ▸ with_bot.coe_le_coe.2 (nat.zero_le _),
by { intro a, rw [count_zero, root_multiplicity_eq_zero (not_exists.mp h a)] }⟩
using_well_founded {dec_tac := tactic.assumption}

/-- `roots p` noncomputably gives a finset containing all the roots of `p` -/
noncomputable def roots (p : polynomial R) : finset R :=
if h : p = 0 then ∅ else classical.some (exists_finset_roots h)
/-- `roots p` noncomputably gives a multiset containing all the roots of `p`,
including their multiplicities. -/
noncomputable def roots (p : polynomial R) : multiset R :=
if h : p = 0 then ∅ else classical.some (exists_multiset_roots h)

@[simp] lemma roots_zero : (0 : polynomial R).roots = ∅ :=
@[simp] lemma roots_zero : (0 : polynomial R).roots = 0 :=
dif_pos rfl

lemma card_roots (hp0 : p ≠ 0) : ((roots p).card : with_bot ℕ) ≤ degree p :=
begin
unfold roots,
rw dif_neg hp0,
exact (classical.some_spec (exists_finset_roots hp0)).1
exact (classical.some_spec (exists_multiset_roots hp0)).1
end

lemma card_roots' {p : polynomial R} (hp0 : p ≠ 0) : p.roots.card ≤ nat_degree p :=
Expand All @@ -155,62 +253,74 @@ lemma card_roots_sub_C' {p : polynomial R} {a : R} (hp0 : 0 < degree p) :
with_bot.coe_le_coe.1 (le_trans (card_roots_sub_C hp0) (le_of_eq $ degree_eq_nat_degree
(λ h, by simp [*, lt_irrefl] at *)))

@[simp] lemma count_roots (hp : p ≠ 0) : p.roots.count a = root_multiplicity a p :=
by { rw [roots, dif_neg hp], exact (classical.some_spec (exists_multiset_roots hp)).2 a }

@[simp] lemma mem_roots (hp : p ≠ 0) : a ∈ p.roots ↔ is_root p a :=
by unfold roots; rw dif_neg hp; exact (classical.some_spec (exists_finset_roots hp)).2 _
by rw [← count_pos, count_roots hp, root_multiplicity_pos hp]

lemma roots_mul (hpq : p * q ≠ 0) : (p * q).roots = p.roots ∪ q.roots :=
finset.ext $ λ r, by rw [mem_union, mem_roots hpq, mem_roots (mul_ne_zero_iff.1 hpq).1,
mem_roots (mul_ne_zero_iff.1 hpq).2, root_mul]
lemma roots_mul {p q : polynomial R} (hpq : p * q ≠ 0) : (p * q).roots = p.roots + q.roots :=
multiset.ext.mpr $ λ r,
by rw [count_add, count_roots hpq, count_roots (left_ne_zero_of_mul hpq),
count_roots (right_ne_zero_of_mul hpq), root_multiplicity_mul hpq]

@[simp] lemma mem_roots_sub_C {p : polynomial R} {a x : R} (hp0 : 0 < degree p) :
x ∈ (p - C a).roots ↔ p.eval x = a :=
(mem_roots (show p - C a ≠ 0, from mt sub_eq_zero.1 $ λ h,
not_le_of_gt hp0 $ h.symm ▸ degree_C_le)).trans
(by rw [is_root.def, eval_sub, eval_C, sub_eq_zero])

@[simp] lemma roots_X_sub_C (r : R) : roots (X - C r) = {r} :=
finset.ext $ λ s, by rw [mem_roots (X_sub_C_ne_zero r), root_X_sub_C, mem_singleton, eq_comm]
@[simp] lemma roots_X_sub_C (r : R) : roots (X - C r) = r :: 0 :=
begin
ext s,
rw [count_roots (X_sub_C_ne_zero r), root_multiplicity_X_sub_C],
split_ifs with h,
{ rw [h, count_singleton] },
{ rw [count_cons_of_ne h, count_zero] }
end

@[simp] lemma roots_C (x : R) : (C x).roots = ∅ :=
if H : x = 0 then by rw [H, C_0, roots_zero] else finset.ext $ λ r,
@[simp] lemma roots_C (x : R) : (C x).roots = 0 :=
if H : x = 0 then by rw [H, C_0, roots_zero] else multiset.ext.mpr $ λ r,
have h : C x ≠ 0, from λ h, H $ C_inj.1 $ h.symm ▸ C_0.symm,
by rw [mem_roots h, is_root.def, eval_C, eq_false_intro H, eq_false_intro (finset.not_mem_empty r)]
have not_root : ¬ is_root (C x) r := mt (λ (h : eval r (C x) = 0), trans eval_C.symm h) H,
by rw [count_roots h, count_zero, root_multiplicity_eq_zero not_root]

@[simp] lemma roots_one : (1 : polynomial R).roots = ∅ :=
roots_C 1

lemma roots_list_prod (L : list (polynomial R)) :
(∀ p ∈ L, (p : _) ≠ 0) → L.prod.roots = L.to_finset.bind roots :=
(∀ p ∈ L, (p : _) ≠ 0) → L.prod.roots = (L : multiset (polynomial R)).bind roots :=
list.rec_on L (λ _, roots_one) $ λ hd tl ih H,
begin
rw list.forall_mem_cons at H,
rw [list.prod_cons, roots_mul (mul_ne_zero H.1 $ list.prod_ne_zero H.2),
list.to_finset_cons, finset.bind_insert, ih H.2]
← multiset.cons_coe, multiset.cons_bind, ih H.2]
end

lemma roots_multiset_prod (m : multiset (polynomial R)) :
(∀ p ∈ m, (p : _) ≠ 0) → m.prod.roots = m.to_finset.bind roots :=
(∀ p ∈ m, (p : _) ≠ 0) → m.prod.roots = m.bind roots :=
multiset.induction_on m (λ _, roots_one) $ λ hd tl ih H,
begin
rw multiset.forall_mem_cons at H,
rw [multiset.prod_cons, roots_mul (mul_ne_zero H.1 $ multiset.prod_ne_zero H.2),
multiset.to_finset_cons, finset.bind_insert, ih H.2]
multiset.cons_bind, ih H.2]
end

lemma roots_prod {ι : Type*} (f : ι → polynomial R) (s : finset ι) :
s.prod f ≠ 0 → (s.prod f).roots = s.bind (λ i, roots (f i)) :=
s.prod f ≠ 0 → (s.prod f).roots = s.val.bind (λ i, roots (f i)) :=
begin
refine s.induction_on _ _,
{ intros, exact roots_one },
intros i s hi ih ne_zero,
rw prod_insert hi at ⊢ ne_zero,
rw [roots_mul ne_zero, ih (right_ne_zero_of_mul ne_zero), bind_insert]
rw [roots_mul ne_zero, ih (right_ne_zero_of_mul ne_zero), insert_val,
ndinsert_of_not_mem hi, cons_bind]
end

lemma roots_prod_X_sub_C (s : finset R) :
(s.prod (λ a, X - C a)).roots = s :=
(s.prod (λ a, X - C a)).roots = s.val :=
(roots_prod (λ a, X - C a) s (prod_ne_zero_iff.mpr (λ a _, X_sub_C_ne_zero a))).trans
(by simp_rw [roots_X_sub_C, bind_singleton_eq_self])
(by simp_rw [roots_X_sub_C, bind_cons, bind_zero, add_zero, multiset.map_id'])

lemma card_roots_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
(roots ((X : polynomial R) ^ n - C a)).card ≤ n :=
Expand All @@ -221,7 +331,7 @@ calc ((roots ((X : polynomial R) ^ n - C a)).card : with_bot ℕ)


/-- `nth_roots n a` noncomputably returns the solutions to `x ^ n = a`-/
def nth_roots {R : Type*} [integral_domain R] (n : ℕ) (a : R) : finset R :=
def nth_roots {R : Type*} [integral_domain R] (n : ℕ) (a : R) : multiset R :=
roots ((X : polynomial R) ^ n - C a)

@[simp] lemma mem_nth_roots {R : Type*} [integral_domain R] {n : ℕ} (hn : 0 < n) {a x : R} :
Expand All @@ -233,7 +343,7 @@ lemma card_nth_roots {R : Type*} [integral_domain R] (n : ℕ) (a : R) :
(nth_roots n a).card ≤ n :=
if hn : n = 0
then if h : (X : polynomial R) ^ n - C a = 0
then by simp only [nat.zero_le, nth_roots, roots, h, dif_pos rfl, card_empty]
then by simp only [nat.zero_le, nth_roots, roots, h, dif_pos rfl, empty_eq_zero, card_zero]
else with_bot.coe_le_coe.1 (le_trans (card_roots h)
(by rw [hn, pow_zero, ← C_1, ← @is_ring_hom.map_sub _ _ _ _ (@C R _)];
exact degree_C_le))
Expand Down Expand Up @@ -288,21 +398,6 @@ lemma leading_coeff_comp (hq : nat_degree q ≠ 0) : leading_coeff (p.comp q) =
leading_coeff p * leading_coeff q ^ nat_degree p :=
by rw [← coeff_comp_degree_mul_degree hq, ← nat_degree_comp]; refl

lemma degree_eq_zero_of_is_unit (h : is_unit p) : degree p = 0 :=
let ⟨q, hq⟩ := is_unit_iff_dvd_one.1 h in
have hp0 : p ≠ 0, from λ hp0, by simpa [hp0] using hq,
have hq0 : q ≠ 0, from λ hp0, by simpa [hp0] using hq,
have nat_degree (1 : polynomial R) = nat_degree (p * q),
from congr_arg _ hq,
by rw [nat_degree_one, nat_degree_mul hp0 hq0, eq_comm,
_root_.add_eq_zero_iff, ← with_bot.coe_eq_coe,
← degree_eq_nat_degree hp0] at this;
exact this.1

@[simp] lemma degree_coe_units (u : units (polynomial R)) :
degree (u : polynomial R) = 0 :=
degree_eq_zero_of_is_unit ⟨u, rfl⟩

lemma units_coeff_zero_smul (c : units (polynomial R)) (p : polynomial R) :
(c : polynomial R).coeff 0 • p = c * p :=
by rw [←polynomial.C_mul', ←polynomial.eq_C_of_degree_eq_zero (degree_coe_units c)]
Expand All @@ -311,6 +406,8 @@ by rw [←polynomial.C_mul', ←polynomial.eq_C_of_degree_eq_zero (degree_coe_un
nat_degree (u : polynomial R) = 0 :=
nat_degree_eq_of_degree_eq_some (degree_coe_units u)

end roots

theorem is_unit_iff {f : polynomial R} : is_unit f ↔ ∃ r : R, is_unit r ∧ C r = f :=
⟨λ hf, ⟨f.coeff 0,
is_unit_C.1 $ eq_C_of_degree_eq_zero (degree_eq_zero_of_is_unit hf) ▸ hf,
Expand Down Expand Up @@ -338,38 +435,6 @@ this.elim
by rw h₁ at h₂; exact absurd h₂ dec_trivial)
(λ hgu, by rw [hg, degree_mul, degree_X_sub_C, degree_eq_zero_of_is_unit hgu, add_zero])

theorem prime_X_sub_C {r : R} : prime (X - C r) :=
⟨X_sub_C_ne_zero r, not_is_unit_X_sub_C,
λ _ _, by { simp_rw [dvd_iff_is_root, is_root.def, eval_mul, mul_eq_zero], exact id }⟩

theorem prime_X : prime (X : polynomial R) :=
by simpa only [C_0, sub_zero] using (prime_X_sub_C : prime (X - C 0 : polynomial R))

lemma prime_of_degree_eq_one_of_monic (hp1 : degree p = 1)
(hm : monic p) : prime p :=
have p = X - C (- p.coeff 0),
by simpa [hm.leading_coeff] using eq_X_add_C_of_degree_eq_one hp1,
this.symm ▸ prime_X_sub_C

theorem irreducible_X_sub_C (r : R) : irreducible (X - C r) :=
irreducible_of_prime prime_X_sub_C

theorem irreducible_X : irreducible (X : polynomial R) :=
irreducible_of_prime prime_X

lemma irreducible_of_degree_eq_one_of_monic (hp1 : degree p = 1)
(hm : monic p) : irreducible p :=
irreducible_of_prime (prime_of_degree_eq_one_of_monic hp1 hm)

theorem eq_of_monic_of_associated (hp : p.monic) (hq : q.monic) (hpq : associated p q) : p = q :=
begin
obtain ⟨u, hu⟩ := hpq,
unfold monic at hp hq,
rw eq_C_of_degree_le_zero (le_of_eq $ degree_coe_units _) at hu,
rw [← hu, leading_coeff_mul, hp, one_mul, leading_coeff_C] at hq,
rwa [hq, C_1, mul_one] at hu
end

end integral_domain

section
Expand Down
5 changes: 3 additions & 2 deletions src/field_theory/finite.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,8 +53,9 @@ open polynomial
lemma card_image_polynomial_eval [decidable_eq R] [fintype R] {p : polynomial R} (hp : 0 < p.degree) :
fintype.card R ≤ nat_degree p * (univ.image (λ x, eval x p)).card :=
finset.card_le_mul_card_image _ _
(λ a _, calc _ = (p - C a).roots.card : congr_arg card
(by simp [finset.ext_iff, mem_roots_sub_C hp, -sub_eq_add_neg])
(λ a _, calc _ = (p - C a).roots.to_finset.card : congr_arg card
(by simp [finset.ext_iff, mem_roots_sub_C hp])
... ≤ (p - C a).roots.card : multiset.to_finset_card_le _
... ≤ _ : card_roots_sub_C' hp)

/-- If `f` and `g` are quadratic polynomials, then the `f.eval a + g.eval b = 0` has a solution. -/
Expand Down
3 changes: 2 additions & 1 deletion src/field_theory/normal.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,8 @@ begin
splits_prod _ $ λ x hx, normal.splits F K x,
subalgebra.to_submodule_injective _⟩,
rw [algebra.coe_top, eq_top_iff, ← hs.2, submodule.span_le, set.range_subset_iff],
refine λ x, algebra.subset_adjoin ((mem_roots $ mt (map_eq_zero $ algebra_map F K).1 $
refine λ x, algebra.subset_adjoin (multiset.mem_to_finset.mpr $
(mem_roots $ mt (map_eq_zero $ algebra_map F K).1 $
finset.prod_ne_zero_iff.2 $ λ x hx, _).2 _),
{ exact minimal_polynomial.ne_zero _ },
rw [is_root.def, eval_map, ← aeval_def, alg_hom.map_prod],
Expand Down
Loading

0 comments on commit 9f55ed7

Please sign in to comment.