[Merged by Bors] - feat(field_theory/splitting_field): generalize some results from field to domain

src/data/multiset/basic.lean

@@ -2151,10 +2151,14 @@ begin
     simp only [h, if_false, zero_min],
 end
 
+theorem count_map {α β : Type*} (f : α → β) (s : multiset α) [decidable_eq β] (b : β) :
+  count b (map f s) = (s.filter (λ a, b = f a)).card :=
+countp_map _ _ _
+
 /-- `multiset.map f` preserves `count` if `f` is injective on the set of elements contained in
 the multiset -/
 theorem count_map_eq_count [decidable_eq β] (f : α → β) (s : multiset α)
- (hf : set.inj_on f {x : α | x ∈ s}) (x ∈ s) : (s.map f).count (f x) = s.count x :=
+  (hf : set.inj_on f {x : α | x ∈ s}) (x ∈ s) : (s.map f).count (f x) = s.count x :=
 begin
   suffices : (filter (λ (a : α), f x = f a) s).count x = card (filter (λ (a : α), f x = f a) s),
   { rw [count, countp_map, ← this],
@@ -2163,6 +2167,18 @@ begin
     simp only [count_repeat, eq_self_iff_true, if_true, card_repeat]},
 end
 
+/-- `multiset.map f` preserves `count` if `f` is injective -/
+theorem count_map_eq_count' [decidable_eq β] (f : α → β) (s : multiset α)
+  (hf : function.injective f) (x : α) : (s.map f).count (f x) = s.count x :=
+begin
+  by_cases H : x ∈ s,
+  { exact count_map_eq_count f _ (set.inj_on_of_injective hf _) _ H, },
+  { simp [H, not_exists, count_eq_zero, count_eq_zero_of_not_mem H, hf],
+    intros y hy hh,
+    apply H,
+    rwa [← hf hh], }
+end
+
 lemma filter_eq' (s : multiset α) (b : α) : s.filter (= b) = repeat b (count b s) :=
 begin
   ext a,

src/data/polynomial/field_division.lean

@@ -59,19 +59,8 @@ by simp only [polynomial.coe_norm_unit, normalize_apply, hp.leading_coeff, norm_
 
 end is_domain
 
-section field
-variables [field R] {p q : polynomial R}
-
-lemma is_unit_iff_degree_eq_zero : is_unit p ↔ degree p = 0 :=
-⟨degree_eq_zero_of_is_unit,
-  λ h, have degree p ≤ 0, by simp [*, le_refl],
-    have hc : coeff p 0 ≠ 0, from λ hc,
-        by rw [eq_C_of_degree_le_zero this, hc] at h;
-        simpa using h,
-    is_unit_iff_dvd_one.2 ⟨C (coeff p 0)⁻¹, begin
-      conv in p { rw eq_C_of_degree_le_zero this },
-      rw [← C_mul, _root_.mul_inv_cancel hc, C_1]
-    end⟩⟩
+section division_ring
+variables [division_ring R] {p q : polynomial R}
 
 lemma degree_pos_of_ne_zero_of_nonunit (hp0 : p ≠ 0) (hp : ¬is_unit p) :
   0 < degree p :=
@@ -92,6 +81,22 @@ have h₁ : (leading_coeff q)⁻¹ ≠ 0 :=
   inv_ne_zero (mt leading_coeff_eq_zero.1 h),
 by rw [degree_mul, degree_C h₁, add_zero]
 
+end division_ring
+
+section field
+variables [field R] {p q : polynomial R}
+
+lemma is_unit_iff_degree_eq_zero : is_unit p ↔ degree p = 0 :=
+⟨degree_eq_zero_of_is_unit,
+  λ h, have degree p ≤ 0, by simp [*, le_refl],
+    have hc : coeff p 0 ≠ 0, from λ hc,
+        by rw [eq_C_of_degree_le_zero this, hc] at h;
+        simpa using h,
+    is_unit_iff_dvd_one.2 ⟨C (coeff p 0)⁻¹, begin
+      conv in p { rw eq_C_of_degree_le_zero this },
+      rw [← C_mul, _root_.mul_inv_cancel hc, C_1]
+    end⟩⟩
+
 theorem irreducible_of_monic {p : polynomial R} (hp1 : p.monic) (hp2 : p ≠ 1) :
   irreducible p ↔ (∀ f g : polynomial R, f.monic → g.monic → f * g = p → f = 1 ∨ g = 1) :=
 ⟨λ hp3 f g hf hg hfg, or.cases_on (hp3.is_unit_or_is_unit hfg.symm)
@@ -427,18 +432,16 @@ begin
   rw [← C_inj, this, C_0],
 end
 
-lemma prod_multiset_root_eq_finset_root {p : polynomial R} (hzero : p ≠ 0) :
+lemma prod_multiset_root_eq_finset_root {R : Type*} [comm_ring R] [is_domain R] {p : polynomial R} :
   (multiset.map (λ (a : R), X - C a) p.roots).prod =
   ∏ a in (multiset.to_finset p.roots), (λ (a : R), (X - C a) ^ (root_multiplicity a p)) a :=
-by simp only [count_roots hzero, finset.prod_multiset_map_count]
+by simp only [count_roots, finset.prod_multiset_map_count]
 
 /-- The product `∏ (X - a)` for `a` inside the multiset `p.roots` divides `p`. -/
 lemma prod_multiset_X_sub_C_dvd (p : polynomial R) :
   (multiset.map (λ (a : R), X - C a) p.roots).prod ∣ p :=
 begin
-  by_cases hp0 : p = 0,
-  { simp only [hp0, roots_zero, is_unit_one, multiset.prod_zero, multiset.map_zero, is_unit.dvd] },
-  rw prod_multiset_root_eq_finset_root hp0,
+  rw prod_multiset_root_eq_finset_root,
   have hcoprime : pairwise (is_coprime on λ (a : R), polynomial.X - C (id a)) :=
     pairwise_coprime_X_sub function.injective_id,
   have H : pairwise (is_coprime on λ (a : R), (polynomial.X - C (id a)) ^ (root_multiplicity a p)),
@@ -449,29 +452,25 @@ begin
   exact pow_root_multiplicity_dvd p a
 end
 
-lemma roots_C_mul (p : polynomial R) {a : R} (hzero : a ≠ 0) : (C a * p).roots = p.roots :=
+lemma roots_C_mul {R : Type*} [comm_ring R] [is_domain R] (p : polynomial R) {a : R}
+  (hzero : a ≠ 0) : (C a * p).roots = p.roots :=
 begin
   by_cases hpzero : p = 0,
   { simp only [hpzero, mul_zero] },
   rw multiset.ext,
   intro b,
   have prodzero : C a * p ≠ 0,
   { simp only [hpzero, or_false, ne.def, mul_eq_zero, C_eq_zero, hzero, not_false_iff] },
-  rw [count_roots hpzero, count_roots prodzero, root_multiplicity_mul prodzero],
+  rw [count_roots, count_roots, root_multiplicity_mul prodzero],
   have mulzero : root_multiplicity b (C a) = 0,
   { simp only [hzero, root_multiplicity_eq_zero, eval_C, is_root.def, not_false_iff] },
   simp only [mulzero, zero_add]
 end
 
-lemma roots_normalize : (normalize p).roots = p.roots :=
-begin
-  by_cases hzero : p = 0,
-  { rw [hzero, normalize_zero], },
-  { have hcoeff : p.leading_coeff ≠ 0,
-    { intro h, exact hzero (leading_coeff_eq_zero.1 h) },
-    rw [normalize_apply, mul_comm, coe_norm_unit_of_ne_zero hzero,
-      roots_C_mul _ (inv_ne_zero hcoeff)], },
-end
+lemma roots_normalize {R : Type*} [comm_ring R] [is_domain R] [normalization_monoid R]
+  {p : polynomial R} : (normalize p).roots = p.roots :=
+by rw [normalize_apply, mul_comm, coe_norm_unit,
+  roots_C_mul _ (norm_unit (leading_coeff p)).ne_zero]
 
 end field
 end polynomial

src/data/polynomial/ring_division.lean

@@ -329,11 +329,16 @@ 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 count_roots : p.roots.count a = root_multiplicity a p :=
+begin
+  unfold roots,
+  split_ifs with hp,
+  { simp [hp], },
+  exact (classical.some_spec (exists_multiset_roots hp)).2 a,
+end
 
 @[simp] lemma mem_roots (hp : p ≠ 0) : a ∈ p.roots ↔ is_root p a :=
-by rw [← count_pos, count_roots hp, root_multiplicity_pos hp]
+by rw [← count_pos, count_roots, root_multiplicity_pos hp]
 
 lemma eq_zero_of_infinite_is_root
   (p : polynomial R) (h : set.infinite {x | is_root p x}) : p = 0 :=
@@ -363,8 +368,8 @@ end
 
 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]
+  by rw [count_add, count_roots, count_roots,
+         count_roots, 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 :=
@@ -375,17 +380,16 @@ multiset.ext.mpr $ λ r,
 @[simp] lemma roots_X_sub_C (r : R) : roots (X - C r) = {r} :=
 begin
   ext s,
-  rw [count_roots (X_sub_C_ne_zero r), root_multiplicity_X_sub_C],
+  rw [count_roots, root_multiplicity_X_sub_C],
   split_ifs with h,
   { rw [h, count_singleton_self] },
   { rw [singleton_eq_cons, count_cons_of_ne h, count_zero] }
 end
 
 @[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,
 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]
+by rw [count_roots, count_zero, root_multiplicity_eq_zero not_root]
 
 @[simp] lemma roots_one : (1 : polynomial R).roots = ∅ :=
 roots_C 1
@@ -422,6 +426,48 @@ calc ((roots ((X : polynomial R) ^ n - C a)).card : with_bot ℕ)
       ≤ degree ((X : polynomial R) ^ n - C a) : card_roots (X_pow_sub_C_ne_zero hn a)
   ... = n : degree_X_pow_sub_C hn a
 
+lemma le_root_multiplicity_map {K L : Type*} [comm_ring K] [is_domain K]
+  [comm_ring L] [is_domain L] {p : polynomial K} {f : K →+* L} (hf : function.injective f)
+  (hroots : p.roots.card = p.nat_degree) (a : K) :
+  root_multiplicity a p ≤ root_multiplicity (f a) (map f p) :=
+begin
+  by_cases hp0 : p = 0, { simp only [hp0, root_multiplicity_zero, map_zero], },
+  have hmap : map f p ≠ 0, { simpa only [map_zero] using (map_injective f hf).ne hp0, },
+  rw [root_multiplicity, root_multiplicity, dif_neg hp0, dif_neg hmap],
+  simp only [not_not, nat.lt_find_iff, nat.le_find_iff],
+  intros m hm,
+  have := ring_hom.map_dvd (map_ring_hom f) (hm m le_rfl),
+  simpa only [coe_map_ring_hom, map_pow, map_sub, map_X, map_C],
+end
+
+lemma count_map_roots {K L : Type*} [comm_ring K] [is_domain K]
+  [comm_ring L] [is_domain L] {p : polynomial K} {f : K →+* L} (hf : function.injective f)
+  (hroots : p.roots.card = p.nat_degree) (a : L) :
+  count a (multiset.map f p.roots) ≤ root_multiplicity a (map f p) :=
+begin
+  by_cases h : ∃ t, f t = a,
+  { rcases h with ⟨h_w, rfl⟩,
+    rw [multiset.count_map_eq_count' f _ hf, count_roots],
+    exact le_root_multiplicity_map hf hroots h_w },
+  { suffices : multiset.count a (multiset.map f p.roots) = 0,
+    { rw this, exact zero_le _, },
+    rw [multiset.count_map, multiset.card_eq_zero, multiset.filter_eq_nil],
+    rintro k hk rfl,
+    exact h ⟨k, rfl⟩, },
+end
+
+lemma roots_map_of_injective_card_eq_total_degree {K L : Type*} [comm_ring K] [is_domain K]
+  [comm_ring L] [is_domain L] {p : polynomial K} {f : K →+* L} (hf : function.injective f)
+  (hroots : p.roots.card = p.nat_degree) :
+  multiset.map f p.roots = (map f p).roots :=
+begin
+  by_cases hp0 : p = 0, { simp only [hp0, roots_zero, multiset.map_zero, map_zero], },
+  have hmap : map f p ≠ 0, { simpa only [map_zero] using (map_injective f hf).ne hp0, },
+  apply multiset.eq_of_le_of_card_le,
+  { simpa only [multiset.le_iff_count, count_roots] using count_map_roots hf hroots },
+  { simpa only [multiset.card_map, hroots] using (card_roots' hmap).trans (nat_degree_map_le f p) },
+end
+
 section nth_roots
 
 /-- `nth_roots n a` noncomputably returns the solutions to `x ^ n = a`-/

src/field_theory/separable.lean

@@ -432,7 +432,7 @@ lemma count_roots_le_one {p : polynomial R} (hsep : separable p) (x : R) :
 begin
   rcases eq_or_ne p 0 with rfl | hp,
   { simp },
-  rw count_roots hp,
+  rw count_roots,
   exact root_multiplicity_le_one_of_separable hp hsep x
 end
 

src/field_theory/splitting_field.lean

@@ -38,7 +38,7 @@ if it is the smallest field extension of `K` such that `f` splits.
   `L`, then `algebra.adjoin F S` embeds into `L`.
 * `polynomial.is_splitting_field.lift`: An embedding of a splitting field of the polynomial `f` into
   another field such that `f` splits.
-* `polynomial.is_splitting_field.alg_equiv`: Every splitting field of a polynomial `f` is isomorpic
+* `polynomial.is_splitting_field.alg_equiv`: Every splitting field of a polynomial `f` is isomorphic
   to `splitting_field f` and thus, being a splitting field is unique up to isomorphism.
 
 -/
@@ -373,12 +373,12 @@ end
 
 /-- A monic polynomial `p` that has as many roots as its degree
 can be written `p = ∏(X - a)`, for `a` in `p.roots`. -/
-lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq {p : polynomial K}
+lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq_of_field {p : polynomial K}
   (hmonic : p.monic) (hroots : p.roots.card = p.nat_degree) :
   (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
 begin
   have hprodmonic : (multiset.map (λ (a : K), X - C a) p.roots).prod.monic,
-  { simp only [prod_multiset_root_eq_finset_root (ne_zero_of_monic hmonic),
+  { simp only [prod_multiset_root_eq_finset_root,
       monic_prod_of_monic, monic_X_sub_C, monic_pow, forall_true_iff] },
   have hdegree : (multiset.map (λ (a : K), X - C a) p.roots).prod.nat_degree = p.nat_degree,
   { rw [← hroots, nat_degree_multiset_prod _ (zero_nmem_multiset_map_X_sub_C _ (λ a : K, a))],
@@ -400,11 +400,33 @@ begin
   exact eq_of_monic_of_associated hprodmonic hmonic hassoc
 end
 
+lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq {K : Type*} [comm_ring K] [is_domain K]
+  {p : polynomial K} (hmonic : p.monic) (hroots : p.roots.card = p.nat_degree) :
+  (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
+begin
+  apply map_injective _ (is_fraction_ring.injective K (fraction_ring K)),
+  rw map_multiset_prod,
+  simp only [map_C, function.comp_app, map_X, multiset.map_map, map_sub],
+  have : p.roots.map (algebra_map K (fraction_ring K)) =
+    (map (algebra_map K (fraction_ring K)) p).roots :=
+    roots_map_of_injective_card_eq_total_degree
+      (is_fraction_ring.injective K (fraction_ring K)) hroots,
+  rw ← prod_multiset_X_sub_C_of_monic_of_roots_card_eq_of_field
+    (monic_map (algebra_map K (fraction_ring K)) hmonic),
+  { simp only [map_C, function.comp_app, map_X, map_sub],
+    congr' 1,
+    rw ← this,
+    simp, },
+  { rw [nat_degree_map' (is_fraction_ring.injective K (fraction_ring K)), ← this],
+    simp only [←hroots, multiset.card_map], },
+end
+
 /-- A polynomial `p` that has as many roots as its degree
-can be written `p = p.leading_coeff * ∏(X - a)`, for `a` in `p.roots`. -/
-lemma C_leading_coeff_mul_prod_multiset_X_sub_C {p : polynomial K}
+can be written `p = p.leading_coeff * ∏(X - a)`, for `a` in `p.roots`.
+Used to prove the more general `C_leading_coeff_mul_prod_multiset_X_sub_C` below. -/
+lemma C_leading_coeff_mul_prod_multiset_X_sub_C_of_field {p : polynomial K}
   (hroots : p.roots.card = p.nat_degree) :
-  (C p.leading_coeff) * (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
+  C p.leading_coeff * (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
 begin
   by_cases hzero : p = 0,
   { rw [hzero, leading_coeff_zero, ring_hom.map_zero, zero_mul], },
@@ -423,6 +445,39 @@ begin
     ... = p : by simp only [mul_one, ring_hom.map_one], },
 end
 
+/-- A polynomial `p` that has as many roots as its degree
+can be written `p = p.leading_coeff * ∏(X - a)`, for `a` in `p.roots`. -/
+lemma C_leading_coeff_mul_prod_multiset_X_sub_C {K : Type*} [comm_ring K] [is_domain K]
+  {p : polynomial K} (hroots : p.roots.card = p.nat_degree) :
+  C p.leading_coeff * (multiset.map (λ (a : K), X - C a) p.roots).prod = p :=
+begin
+  by_cases hzero : p = 0,
+  { rw [hzero, leading_coeff_zero, ring_hom.map_zero, zero_mul], },
+  have hcoeff : p.leading_coeff ≠ 0,
+  { intro h, exact hzero (leading_coeff_eq_zero.1 h) },
+  apply map_injective _ (is_fraction_ring.injective K (fraction_ring K)),
+  rw [map_mul, map_multiset_prod],
+  simp only [map_C, function.comp_app, map_X, multiset.map_map, map_sub],
+  have h : p.roots.map (algebra_map K (fraction_ring K)) =
+    (map (algebra_map K (fraction_ring K)) p).roots :=
+    roots_map_of_injective_card_eq_total_degree
+      (is_fraction_ring.injective K (fraction_ring K)) hroots,
+  have : multiset.card (map (algebra_map K (fraction_ring K)) p).roots =
+    (map (algebra_map K (fraction_ring K)) p).nat_degree,
+  { rw [nat_degree_map' (is_fraction_ring.injective K (fraction_ring K)), ← h],
+    simp only [←hroots, multiset.card_map], },
+  rw [← C_leading_coeff_mul_prod_multiset_X_sub_C_of_field this],
+  simp only [map_C, function.comp_app, map_X, map_sub],
+  congr' 2,
+  { rw leading_coeff_map_of_leading_coeff_ne_zero,
+    intro hn,
+    apply hcoeff,
+    apply is_fraction_ring.injective K (fraction_ring K),
+    simp [hn], },
+  rw ← h,
+  simp,
+end
+
 /-- A polynomial splits if and only if it has as many roots as its degree. -/
 lemma splits_iff_card_roots {p : polynomial K} :
   splits (ring_hom.id K) p ↔ p.roots.card = p.nat_degree :=