golf(data/polynomial): factorization into linear factors when #roots=…

…degree (#14862)

+ Golf the proofs of `prod_multiset_X_sub_C_of_monic_of_roots_card_eq` and `C_leading_coeff_mul_prod_multiset_X_sub_C` and move them from *splitting_field.lean* to *ring_division.lean*; instead of using the former to deduce the latter as is currently done in mathlib, we prove the latter first and deduce the former easily. Remove the less general auxiliary, `private` `_of_field` versions.

+ Move `pairwise_coprime_X_sub` from *field_division.lean* to *ring_division.lean*. Rename it to `pairwise_coprime_X_sub_C` to conform with existing convention. Golf its proof using the more general new lemma `is_coprime_X_sub_C_of_is_unit_sub`.

+ Golf `monic.irreducible_of_irreducible_map`, but it's essentially the same proof.

src/data/polynomial/field_division.lean

@@ -469,14 +469,6 @@ theorem degree_pos_of_irreducible (hp : irreducible p) : 0 < p.degree :=
 lt_of_not_ge $ λ hp0, have _ := eq_C_of_degree_le_zero hp0,
   not_irreducible_C (p.coeff 0) $ this ▸ hp
 
-theorem pairwise_coprime_X_sub {α : Type u} [field α] {I : Type v}
-  {s : I → α} (H : function.injective s) :
-  pairwise (is_coprime on (λ i : I, polynomial.X - polynomial.C (s i))) :=
-λ i j hij, have h : s j - s i ≠ 0, from sub_ne_zero_of_ne $ function.injective.ne H hij.symm,
-⟨polynomial.C (s j - s i)⁻¹, -polynomial.C (s j - s i)⁻¹,
-by rw [neg_mul, ← sub_eq_add_neg, ← mul_sub, sub_sub_sub_cancel_left,
-    ← polynomial.C_sub, ← polynomial.C_mul, inv_mul_cancel h, polynomial.C_1]⟩
-
 /-- If `f` is a polynomial over a field, and `a : K` satisfies `f' a ≠ 0`,
 then `f / (X - a)` is coprime with `X - a`.
 Note that we do not assume `f a = 0`, because `f / (X - a) = (f - f a) / (X - a)`. -/
@@ -504,7 +496,7 @@ lemma prod_multiset_X_sub_C_dvd (p : R[X]) :
 begin
   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,
+    pairwise_coprime_X_sub_C function.injective_id,
   have H : pairwise (is_coprime on λ (a : R), (polynomial.X - C (id a)) ^ (root_multiplicity a p)),
   { intros a b hdiff, exact (hcoprime a b hdiff).pow },
   apply finset.prod_dvd_of_coprime (H.set_pairwise (↑(multiset.to_finset p.roots) : set R)),

src/data/polynomial/ring_division.lean

@@ -6,6 +6,8 @@ Authors: Chris Hughes, Johannes Hölzl, Scott Morrison, Jens Wagemaker, Johan Co
 import data.polynomial.algebra_map
 import data.polynomial.degree.lemmas
 import data.polynomial.div
+import ring_theory.localization.fraction_ring
+import algebra.polynomial.big_operators
 
 /-!
 # Theory of univariate polynomials
@@ -730,6 +732,43 @@ begin
   rw [hq.leading_coeff, C_1, one_mul],
 end
 
+lemma is_coprime_X_sub_C_of_is_unit_sub {R} [comm_ring R] {a b : R}
+  (h : is_unit (a - b)) : is_coprime (X - C a) (X - C b) :=
+⟨-C h.unit⁻¹.val, C h.unit⁻¹.val, by { rw [neg_mul_comm, ← left_distrib, neg_add_eq_sub,
+  sub_sub_sub_cancel_left, ← C_sub, ← C_mul], convert C_1, exact h.coe_inv_mul }⟩
+
+theorem pairwise_coprime_X_sub_C {K} [field K] {I : Type v} {s : I → K}
+  (H : function.injective s) : pairwise (is_coprime on (λ i : I, X - C (s i))) :=
+λ i j hij, is_coprime_X_sub_C_of_is_unit_sub (sub_ne_zero_of_ne $ H.ne hij).is_unit
+
+/-- 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 (hroots : p.roots.card = p.nat_degree) :
+  C p.leading_coeff * (p.roots.map (λ (a : R), X - C a)).prod = p :=
+begin
+  symmetry, classical,
+  apply eq_leading_coeff_mul_of_monic_of_dvd_of_nat_degree_le,
+  { exact monic_multiset_prod_of_monic _ _ (λ a _, monic_X_sub_C a) },
+  { rw ← map_dvd_map _ (is_fraction_ring.injective R $ fraction_ring R),
+    swap, { exact monic_multiset_prod_of_monic _ _ (λ a _, monic_X_sub_C a) },
+    rw [finset.prod_multiset_map_count, polynomial.map_prod],
+    refine finset.prod_dvd_of_coprime (λ a _ b _ h, _) (λ a _, _),
+    { simp_rw [polynomial.map_pow, polynomial.map_sub, map_C, map_X],
+      exact (pairwise_coprime_X_sub_C (is_fraction_ring.injective R $ fraction_ring R) _ _ h).pow },
+    { rw count_roots, exact polynomial.map_dvd _ (pow_root_multiplicity_dvd p a) } },
+  { rw [nat_degree_multiset_prod_of_monic, multiset.map_map],
+    { convert hroots.symm.le, convert multiset.sum_repeat 1 _,
+      { convert multiset.map_const _ 1, ext, apply nat_degree_X_sub_C }, { simp } },
+    { intros f hf, obtain ⟨a, ha, rfl⟩ := multiset.mem_map.1 hf, exact monic_X_sub_C a } },
+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
+  (hp : p.monic) (hroots : p.roots.card = p.nat_degree) :
+  (p.roots.map (λ (a : R), X - C a)).prod = p :=
+by {convert C_leading_coeff_mul_prod_multiset_X_sub_C hroots, rw [hp.leading_coeff, C_1, one_mul] }
+
 end comm_ring
 
 section
@@ -743,7 +782,7 @@ begin
   have dz := degree_eq_zero_of_is_unit H,
   rw degree_map_eq_of_leading_coeff_ne_zero at dz,
   { rw eq_C_of_degree_eq_zero dz,
-    refine is_unit.map (C : R →+* R[X]) _,
+    refine is_unit.map C _,
     convert hf,
     rw (degree_eq_iff_nat_degree_eq _).1 dz,
     rintro rfl,
@@ -769,27 +808,14 @@ lemma monic.irreducible_of_irreducible_map (f : R[X])
   (h_mon : monic f) (h_irr : irreducible (map φ f)) :
   irreducible f :=
 begin
-  fsplit,
-  { intro h,
-    exact h_irr.not_unit (is_unit.map (map_ring_hom φ) h), },
-  { intros a b h,
-
-    have q := (leading_coeff_mul a b).symm,
-    rw ←h at q,
-    dsimp [monic] at h_mon,
-    rw h_mon at q,
-    have au : is_unit a.leading_coeff := is_unit_of_mul_eq_one _ _ q,
-    rw mul_comm at q,
-    have bu : is_unit b.leading_coeff := is_unit_of_mul_eq_one _ _ q,
-    clear q h_mon,
-
-    have h' := congr_arg (map φ) h,
-    simp only [polynomial.map_mul] at h',
-    cases h_irr.is_unit_or_is_unit h' with w w,
-    { left,
-      exact is_unit_of_is_unit_leading_coeff_of_is_unit_map _ _ au w, },
-    { right,
-      exact is_unit_of_is_unit_leading_coeff_of_is_unit_map _ _ bu w, }, }
+  refine ⟨h_irr.not_unit ∘ is_unit.map (map_ring_hom φ), λ a b h, _⟩,
+  dsimp [monic] at h_mon,
+  have q := (leading_coeff_mul a b).symm,
+  rw [←h, h_mon] at q,
+  refine (h_irr.is_unit_or_is_unit $ (congr_arg (map φ) h).trans (polynomial.map_mul φ)).imp _ _;
+    apply is_unit_of_is_unit_leading_coeff_of_is_unit_map;
+    apply is_unit_of_mul_eq_one,
+  { exact q }, { rw mul_comm, exact q },
 end
 
 end

src/field_theory/fixed.lean

@@ -175,7 +175,7 @@ begin
   erw [← polynomial.map_dvd_map' (subfield.subtype $ fixed_points.subfield G F),
       minpoly, polynomial.map_to_subring _ (subfield G F).to_subring, prod_X_sub_smul],
   refine fintype.prod_dvd_of_coprime
-    (polynomial.pairwise_coprime_X_sub $ mul_action.injective_of_quotient_stabilizer G x)
+    (polynomial.pairwise_coprime_X_sub_C $ mul_action.injective_of_quotient_stabilizer G x)
     (λ y, quotient_group.induction_on y $ λ g, _),
   rw [polynomial.dvd_iff_is_root, polynomial.is_root.def, mul_action.of_quotient_stabilizer_mk,
       polynomial.eval_smul',

src/field_theory/separable.lean

@@ -262,7 +262,7 @@ lemma separable_prod_X_sub_C_iff' {ι : Sort*} {f : ι → F} {s : finset ι} :
   (∏ i in s, (X - C (f i))).separable ↔ (∀ (x ∈ s) (y ∈ s), f x = f y → x = y) :=
 ⟨λ hfs x hx y hy hfxy, hfs.inj_of_prod_X_sub_C hx hy hfxy,
 λ H, by { rw ← prod_attach, exact separable_prod' (λ x hx y hy hxy,
-    @pairwise_coprime_X_sub _ _ { x // x ∈ s } (λ x, f x)
+    @pairwise_coprime_X_sub_C _ _ { x // x ∈ s } (λ x, f x)
       (λ x y hxy, subtype.eq $ H x.1 x.2 y.1 y.2 hxy) _ _ hxy)
   (λ _ _, separable_X_sub_C) }⟩
 

src/field_theory/splitting_field.lean

@@ -374,111 +374,6 @@ begin
   exact splits_of_splits_id _ h
 end
 
-/-- A monic polynomial `p` that has as many roots as its degree
-can be written `p = ∏(X - a)`, for `a` in `p.roots`. -/
-private lemma prod_multiset_X_sub_C_of_monic_of_roots_card_eq_of_field {p : K[X]}
-  (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,
-      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))],
-    simp only [eq_self_iff_true, mul_one, nat.cast_id, nsmul_eq_mul, multiset.sum_repeat,
-      multiset.map_const,nat_degree_X_sub_C, function.comp, multiset.map_map] },
-  obtain ⟨q, hq⟩ := prod_multiset_X_sub_C_dvd p,
-  have qzero : q ≠ 0,
-  { rintro rfl, apply hmonic.ne_zero, simpa only [mul_zero] using hq },
-  have degp :
-    p.nat_degree = (multiset.map (λ (a : K), X - C a) p.roots).prod.nat_degree + q.nat_degree,
-  { nth_rewrite 0 [hq],
-    simp only [nat_degree_mul hprodmonic.ne_zero qzero] },
-  have degq : q.nat_degree = 0,
-  { rw hdegree at degp,
-    rw [← add_right_inj p.nat_degree, ← degp, add_zero], },
-  obtain ⟨u, hu⟩ := is_unit_iff_degree_eq_zero.2 ((degree_eq_iff_nat_degree_eq qzero).2 degq),
-  have hassoc : associated (multiset.map (λ (a : K), X - C a) p.roots).prod p,
-  { rw associated, use u, rw [hu, ← hq] },
-  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 : K[X]} (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 polynomial.map_multiset_prod,
-  simp only [map_C, function.comp_app, map_X, multiset.map_map, polynomial.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
-    (hmonic.map (algebra_map K (fraction_ring K))),
-  { simp only [map_C, function.comp_app, map_X, polynomial.map_sub],
-    congr' 1,
-    rw ← this,
-    simp, },
-  { rw [nat_degree_map_eq_of_injective (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`.
-Used to prove the more general `C_leading_coeff_mul_prod_multiset_X_sub_C` below. -/
-private lemma C_leading_coeff_mul_prod_multiset_X_sub_C_of_field {p : K[X]}
-  (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) },
-    have hrootsnorm : (normalize p).roots.card = (normalize p).nat_degree,
-    { rw [roots_normalize, normalize_apply, nat_degree_mul hzero (units.ne_zero _), hroots,
-          coe_norm_unit, nat_degree_C, add_zero], },
-    have hprod := prod_multiset_X_sub_C_of_monic_of_roots_card_eq (monic_normalize hzero)
-                    hrootsnorm,
-    rw [roots_normalize, normalize_apply, coe_norm_unit_of_ne_zero hzero] at hprod,
-    calc (C p.leading_coeff) * (multiset.map (λ (a : K), X - C a) p.roots).prod
-        = p * C ((p.leading_coeff)⁻¹ * p.leading_coeff) :
-        by rw [hprod, mul_comm, mul_assoc, ← C_mul]
-    ... = p * C 1 : by field_simp
-    ... = 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 : K[X]} (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 [polynomial.map_mul, polynomial.map_multiset_prod],
-  simp only [map_C, function.comp_app, map_X, multiset.map_map, polynomial.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_eq_of_injective (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, polynomial.map_sub],
-  have w : (algebra_map K (fraction_ring K)) p.leading_coeff ≠ 0,
-  { intro hn,
-    apply hcoeff,
-    apply is_fraction_ring.injective K (fraction_ring K),
-    simp [hn], },
-  rw [←h, leading_coeff_map_of_leading_coeff_ne_zero _ w, multiset.map_map],
-end
-
 /-- A polynomial splits if and only if it has as many roots as its degree. -/
 lemma splits_iff_card_roots {p : K[X]} :
   splits (ring_hom.id K) p ↔ p.roots.card = p.nat_degree :=