feat(ring_theory/polynomial): Vieta's formula in terms of `polynomial…

….roots` (#14908)

Specialize `multiset.prod_X_sub_C_coeff` to the root multiset of a split polynomial over an integral domain to derive the familiar Vieta's formula; update *undergrad.yaml*.

Make various stylistic improvements to *polynomial/vieta.lean*: most notably, `open polynomial` to be able to omit the prefix in `polynomial.X` and `polynomial.C`. Instead, write `mv_polynomial.X` with the prefix because it's less frequent.

Prove miscellaneous lemmas `list.prod_map_neg`, `multiset.prod_map_neg`, `list.map_nth_le` and `multiset.length_to_list`, which are remnants of a previous approach to prove `polynomial.vieta` superseded by #15008. See below/#14908 for the original motivation for introducing them.

docs/undergrad.yaml

@@ -162,7 +162,7 @@ Ring Theory:
     polynomial algebra in one or several indeterminates over a commutative ring: 'mv_polynomial'
     roots of a polynomial: 'polynomial.roots'
     multiplicity: 'polynomial.root_multiplicity'
-    relationship between the coefficients and the roots of a split polynomial: 'https://en.wikipedia.org/wiki/Vieta%27s_formulas'
+    relationship between the coefficients and the roots of a split polynomial: 'polynomial.coeff_eq_esymm_roots_of_card'
     Newton's identities: 'https://en.wikipedia.org/wiki/Newton%27s_identities'
     polynomial derivative: 'polynomial.derivative'
     decomposition into sums of homogeneous polynomials: 'mv_polynomial.sum_homogeneous_component'

src/algebra/big_operators/multiset.lean

@@ -135,6 +135,11 @@ lemma prod_map_one : prod (m.map (λ i, (1 : α))) = 1 := by rw [map_const, prod
 lemma prod_map_mul : (m.map $ λ i, f i * g i).prod = (m.map f).prod * (m.map g).prod :=
 m.prod_hom₂ (*) mul_mul_mul_comm (mul_one _) _ _
 
+@[simp]
+lemma prod_map_neg [has_distrib_neg α] (s : multiset α) :
+  (s.map has_neg.neg).prod = (-1) ^ s.card * s.prod :=
+by { refine quotient.ind _ s, simp }
+
 @[to_additive]
 lemma prod_map_pow {n : ℕ} : (m.map $ λ i, f i ^ n).prod = (m.map f).prod ^ n :=
 m.prod_hom' (pow_monoid_hom n : α →* α) f

src/data/list/big_operators.lean

@@ -89,6 +89,17 @@ lemma prod_map_mul {α : Type*} [comm_monoid α] {l : list ι} {f g : ι → α}
   (l.map $ λ i, f i * g i).prod = (l.map f).prod * (l.map g).prod :=
 l.prod_hom₂ (*) mul_mul_mul_comm (mul_one _) _ _
 
+@[simp]
+lemma prod_map_neg {α} [comm_monoid α] [has_distrib_neg α] (l : list α) :
+  (l.map has_neg.neg).prod = (-1) ^ l.length * l.prod :=
+begin
+  convert @prod_map_mul α α _ l (λ _, -1) id,
+  { ext, rw neg_one_mul, refl },
+  { convert (prod_repeat _ _).symm, rw eq_repeat,
+    use l.length_map _, intro, rw mem_map, rintro ⟨_, _, rfl⟩, refl },
+  { rw l.map_id },
+end
+
 @[to_additive]
 lemma prod_map_hom (L : list ι) (f : ι → M) {G : Type*} [monoid_hom_class G M N] (g : G) :
   (L.map (g ∘ f)).prod = g ((L.map f).prod) :=

src/data/list/range.lean

@@ -282,6 +282,11 @@ option.some.inj $ by rw [← nth_le_nth _, nth_range (by simpa using H)]
   (fin_range n).nth_le i h = ⟨i, length_fin_range n ▸ h⟩ :=
 by simp only [fin_range, nth_le_range, nth_le_pmap, fin.mk_eq_subtype_mk]
 
+@[simp] lemma map_nth_le (l : list α) :
+  (fin_range l.length).map (λ n, l.nth_le n n.2) = l :=
+ext_le (by rw [length_map, length_fin_range]) $ λ n _ h,
+by { rw ← nth_le_map_rev, congr, { rw nth_le_fin_range, refl }, { rw length_fin_range, exact h } }
+
 theorem of_fn_eq_pmap {α n} {f : fin n → α} :
   of_fn f = pmap (λ i hi, f ⟨i, hi⟩) (range n) (λ _, mem_range.1) :=
 by rw [pmap_eq_map_attach]; from ext_le (by simp)

src/data/multiset/basic.lean

@@ -486,6 +486,9 @@ def card : multiset α →+ ℕ :=
 
 @[simp] theorem coe_card (l : list α) : card (l : multiset α) = length l := rfl
 
+@[simp] theorem length_to_list (s : multiset α) : s.to_list.length = s.card :=
+by rw [← coe_card, coe_to_list]
+
 @[simp] theorem card_zero : @card α 0 = 0 := rfl
 
 theorem card_add (s t : multiset α) : card (s + t) = card s + card t :=

src/ring_theory/polynomial/vieta.lean

@@ -3,26 +3,31 @@ Copyright (c) 2020 Hanting Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hanting Zhang
 -/
-import ring_theory.polynomial.basic
+import field_theory.splitting_field
 import ring_theory.polynomial.symmetric
 
 /-!
 # Vieta's Formula
 
 The main result is `multiset.prod_X_add_C_eq_sum_esymm`, which shows that the product of
-linear terms ` X + λ` with `λ` in a `multiset s` is equal to a linear combination of the
+linear terms `X + λ` with `λ` in a `multiset s` is equal to a linear combination of the
 symmetric functions `esymm s`.
 
 From this, we deduce `mv_polynomial.prod_X_add_C_eq_sum_esymm` which is the equivalent formula
 for the product of linear terms `X + X i` with `i` in a `fintype σ` as a linear combination
 of the symmetric polynomials `esymm σ R j`.
 
+For `R` be an integral domain (so that `p.roots` is defined for any `p : R[X]` as a multiset),
+we derive `polynomial.coeff_eq_esymm_roots_of_card`, the relationship between the coefficients and
+the roots of `p` for a polynomial `p` that splits (i.e. having as many roots as its degree).
 -/
 
 open_locale big_operators polynomial
 
 namespace multiset
 
+open polynomial
+
 section semiring
 
 variables {R : Type*} [comm_semiring R]
@@ -31,8 +36,8 @@ variables {R : Type*} [comm_semiring R]
 `λ` runs through a multiset `s` is equal to a linear combination of the symmetric functions
 `esymm s` of the `λ`'s .-/
 lemma prod_X_add_C_eq_sum_esymm (s : multiset R) :
-  (s.map (λ r, polynomial.X + polynomial.C r)).prod =
-  ∑ j in finset.range (s.card + 1), (polynomial.C (s.esymm j) * polynomial.X^(s.card - j)) :=
+  (s.map (λ r, X + C r)).prod =
+  ∑ j in finset.range (s.card + 1), C (s.esymm j) * X ^ (s.card - j) :=
 begin
   classical,
   rw [prod_map_add, antidiagonal_eq_map_powerset, map_map, ←bind_powerset_len, function.comp,
@@ -46,12 +51,11 @@ end
 
 /-- Vieta's formula for the coefficients of the product of linear terms `X + λ` where `λ` runs
 through a multiset `s` : the `k`th coefficient is the symmetric function `esymm (card s - k) s`. -/
-lemma prod_X_add_C_coeff (s : multiset R) {k : ℕ} (h : k ≤ s.card):
-  polynomial.coeff (s.map (λ r, polynomial.X + polynomial.C r)).prod k =
-  s.esymm (s.card - k) :=
+lemma prod_X_add_C_coeff (s : multiset R) {k : ℕ} (h : k ≤ s.card) :
+  (s.map (λ r, X + C r)).prod.coeff k = s.esymm (s.card - k) :=
 begin
   convert polynomial.ext_iff.mp (prod_X_add_C_eq_sum_esymm s) k,
-  simp_rw [polynomial.finset_sum_coeff, polynomial.coeff_C_mul_X_pow],
+  simp_rw [finset_sum_coeff, coeff_C_mul_X_pow],
   rw finset.sum_eq_single_of_mem (s.card - k) _,
   { rw if_pos (nat.sub_sub_self h).symm, },
   { intros j hj1 hj2,
@@ -68,10 +72,10 @@ end semiring
 
 section ring
 
-variables  {R : Type*} [comm_ring R]
+variables {R : Type*} [comm_ring R]
 
 lemma esymm_neg (s : multiset R) (k : ℕ) :
-  (map has_neg.neg s).esymm k = (-1)^k * esymm s k :=
+  (map has_neg.neg s).esymm k = (-1) ^ k * esymm s k :=
 begin
   rw [esymm, esymm, ←multiset.sum_map_mul_left, multiset.powerset_len_map, multiset.map_map,
     map_congr (eq.refl _)],
@@ -83,32 +87,47 @@ begin
 end
 
 lemma prod_X_sub_C_eq_sum_esymm (s : multiset R) :
-  (s.map (λ t, polynomial.X - polynomial.C t)).prod =
-  ∑ j in finset.range (s.card + 1),
-  (-1)^j* (polynomial.C (s.esymm j) * polynomial.X ^ (s.card - j)) :=
+  (s.map (λ t, X - C t)).prod =
+  ∑ j in finset.range (s.card + 1), (-1) ^ j * (C (s.esymm j) * X ^ (s.card - j)) :=
 begin
-  conv_lhs { congr, congr, funext, rw sub_eq_add_neg, rw ←map_neg polynomial.C _, },
+  conv_lhs { congr, congr, funext, rw sub_eq_add_neg, rw ←map_neg C _, },
   convert prod_X_add_C_eq_sum_esymm (map (λ t, -t) s) using 1,
   { rwa map_map, },
   { simp only [esymm_neg, card_map, mul_assoc, map_mul, map_pow, map_neg, map_one], },
 end
 
-lemma prod_X_sub_C_coeff (s : multiset R) {k : ℕ} (h : k ≤ s.card):
-  polynomial.coeff (s.map (λ t, polynomial.X - polynomial.C t)).prod k =
-  (-1)^(s.card - k) * s.esymm (s.card - k) :=
+lemma prod_X_sub_C_coeff (s : multiset R) {k : ℕ} (h : k ≤ s.card) :
+  (s.map (λ t, X - C t)).prod.coeff k = (-1) ^ (s.card - k) * s.esymm (s.card - k) :=
 begin
-  conv_lhs { congr, congr, congr, funext, rw sub_eq_add_neg, rw ←map_neg polynomial.C _, },
+  conv_lhs { congr, congr, congr, funext, rw sub_eq_add_neg, rw ←map_neg C _, },
   convert prod_X_add_C_coeff (map (λ t, -t) s) _ using 1,
   { rwa map_map, },
   { rwa [esymm_neg, card_map] },
   { rwa card_map },
 end
 
+/-- Vieta's formula for the coefficients and the roots of a polynomial over an integral domain
+  with as many roots as its degree. -/
+theorem _root_.polynomial.coeff_eq_esymm_roots_of_card [is_domain R] {p : R[X]}
+  (hroots : p.roots.card = p.nat_degree) {k : ℕ} (h : k ≤ p.nat_degree) :
+  p.coeff k = p.leading_coeff * (-1) ^ (p.nat_degree - k) * p.roots.esymm (p.nat_degree - k) :=
+begin
+  conv_lhs { rw ← C_leading_coeff_mul_prod_multiset_X_sub_C hroots },
+  rw [coeff_C_mul, mul_assoc], congr,
+  convert p.roots.prod_X_sub_C_coeff _ using 3; rw hroots, exact h,
+end
+
+/-- Vieta's formula for split polynomials over a field. -/
+theorem _root_.polynomial.coeff_eq_esymm_roots_of_splits {F} [field F] {p : F[X]}
+  (hsplit : p.splits (ring_hom.id F)) {k : ℕ} (h : k ≤ p.nat_degree) :
+  p.coeff k = p.leading_coeff * (-1) ^ (p.nat_degree - k) * p.roots.esymm (p.nat_degree - k) :=
+polynomial.coeff_eq_esymm_roots_of_card (splits_iff_card_roots.1 hsplit) h
+
 end ring
 
 end multiset
 
-namespace mv_polynomial
+section mv_polynomial
 
 open finset polynomial fintype
 
@@ -117,26 +136,24 @@ variables (R σ : Type*) [comm_semiring R] [fintype σ]
 /-- A sum version of Vieta's formula for `mv_polynomial`: viewing `X i` as variables,
 the product of linear terms `λ + X i` is equal to a linear combination of
 the symmetric polynomials `esymm σ R j`. -/
-lemma prod_C_add_X_eq_sum_esymm :
-  (∏ i : σ, (polynomial.X + polynomial.C (X i)) : polynomial (mv_polynomial σ R) )=
-  ∑ j in range (card σ + 1),
-  (polynomial.C (esymm σ R j) * polynomial.X ^ (card σ - j)) :=
+lemma mv_polynomial.prod_C_add_X_eq_sum_esymm :
+  ∏ i : σ, (X + C (mv_polynomial.X i)) =
+  ∑ j in range (card σ + 1), (C (mv_polynomial.esymm σ R j) * X ^ (card σ - j)) :=
 begin
-  let s := (multiset.map (λ i : σ, (X i : mv_polynomial σ R)) finset.univ.val),
+  let s := finset.univ.val.map (λ i : σ, mv_polynomial.X i),
   rw (_ : card σ = s.card),
-  { simp_rw [esymm_eq_multiset.esymm σ R _, finset.prod_eq_multiset_prod],
+  { simp_rw [mv_polynomial.esymm_eq_multiset.esymm σ R _, finset.prod_eq_multiset_prod],
     convert multiset.prod_X_add_C_eq_sum_esymm s,
     rwa multiset.map_map, },
   { rw multiset.card_map, exact rfl, }
 end
 
-lemma prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ):
-  (∏ i : σ, (polynomial.X + polynomial.C (X i)) : polynomial (mv_polynomial σ R) ).coeff k =
-  esymm σ R (card σ - k) :=
+lemma mv_polynomial.prod_X_add_C_coeff (k : ℕ) (h : k ≤ card σ) :
+  (∏ i : σ, (X + C (mv_polynomial.X i))).coeff k = mv_polynomial.esymm σ R (card σ - k) :=
 begin
-  let s := (multiset.map (λ i : σ, (X i : mv_polynomial σ R)) finset.univ.val),
+  let s := finset.univ.val.map (λ i, (mv_polynomial.X i : mv_polynomial σ R)),
   rw (_ : card σ = s.card) at ⊢ h,
-  { rw [esymm_eq_multiset.esymm σ R (s.card - k), finset.prod_eq_multiset_prod],
+  { rw [mv_polynomial.esymm_eq_multiset.esymm σ R (s.card - k), finset.prod_eq_multiset_prod],
     convert multiset.prod_X_add_C_coeff s h,
     rwa multiset.map_map },
   repeat { rw multiset.card_map, exact rfl, },