feat(algebra/polynomial, data/polynomial): lemmas about monic polynom…

…ials (#3402)




Co-authored-by: Aaron Anderson <awainverse@gmail.com>

src/algebra/char_p.lean

@@ -78,19 +78,27 @@ unfold ring_char; exact char_p.cast_eq_zero_iff α (ring_char α)
 theorem ring_char.eq (α : Type u) [semiring α] {p : ℕ} (C : char_p α p) : p = ring_char α :=
 (classical.some_spec (char_p.exists_unique α)).2 p C
 
+theorem add_pow_char_of_commute (R : Type u) [ring R] {p : ℕ} [fact p.prime]
+  [char_p R p] (x y : R) (h : commute x y):
+(x + y)^p = x^p + y^p :=
+begin
+  rw [commute.add_pow h, finset.sum_range_succ, nat.sub_self, pow_zero, nat.choose_self],
+  rw [nat.cast_one, mul_one, mul_one, add_right_inj],
+  convert finset.sum_eq_single 0 _ _, { simp },
+  swap, { intro h1, contrapose! h1, rw finset.mem_range, apply nat.prime.pos, assumption },
+  intros b h1 h2,
+  suffices : (p.choose b : R) = 0, { rw this, simp },
+  rw char_p.cast_eq_zero_iff R p,
+  apply nat.prime.dvd_choose_self, assumption', { omega },
+  rwa ← finset.mem_range
+end
+
 theorem add_pow_char (α : Type u) [comm_ring α] {p : ℕ} (hp : nat.prime p)
   [char_p α p] (x y : α) : (x + y)^p = x^p + y^p :=
 begin
-  rw [add_pow, finset.sum_range_succ, nat.sub_self, pow_zero, nat.choose_self],
-  rw [nat.cast_one, mul_one, mul_one, add_right_inj],
-  transitivity,
-  { refine finset.sum_eq_single 0 _ _,
-    { intros b h1 h2,
-      have := nat.prime.dvd_choose_self (nat.pos_of_ne_zero h2) (finset.mem_range.1 h1) hp,
-      rw [← nat.div_mul_cancel this, nat.cast_mul, char_p.cast_eq_zero α p],
-      simp only [mul_zero] },
-    { intro H, exfalso, apply H, exact finset.mem_range.2 hp.pos } },
-  rw [pow_zero, nat.sub_zero, one_mul, nat.choose_zero_right, nat.cast_one, mul_one]
+  haveI : fact p.prime := hp,
+  apply add_pow_char_of_commute,
+  apply commute.all,
 end
 
 lemma eq_iff_modeq_int (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :

src/algebra/polynomial/big_operators.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson, Jalex Stark.
 -/
-import algebra.polynomial.basic
+import data.polynomial.monic
 import tactic.linarith
 
 open polynomial finset
@@ -15,34 +15,36 @@ Lemmas for the interaction between polynomials and ∑ and ∏.
 
 ## Main results
 
-- `nat_degree_prod_eq_of_monic` : the degree of a product of monic polynomials is the product of
+- `nat_degree_prod_of_monic` : the degree of a product of monic polynomials is the product of
     degrees. We prove this only for [comm_semiring R],
     but it ought to be true for [semiring R] and list.prod.
-- `nat_degree_prod_eq` : for polynomials over an integral domain,
+- `nat_degree_prod` : for polynomials over an integral domain,
     the degree of the product is the sum of degrees
 - `leading_coeff_prod` : for polynomials over an integral domain,
     the leading coefficient is the product of leading coefficients
+- `prod_X_sub_C_coeff_card_pred` carries most of the content for computing
+    the second coefficient of the characteristic polynomial.
 -/
 
 open_locale big_operators
 
 universes u w
 
-variables {R : Type u} {α : Type w}
+variables {R : Type u} {ι : Type w}
 
 namespace polynomial
 
-variable (s : finset α)
+variable (s : finset ι)
 
 section comm_semiring
-variables [comm_semiring R] (f : α → polynomial R)
+variables [comm_semiring R] (f : ι → polynomial R)
 
 lemma nat_degree_prod_le : (∏ i in s, f i).nat_degree ≤ ∑ i in s, (f i).nat_degree :=
 begin
   classical,
   induction s using finset.induction with a s ha hs, { simp },
   rw [prod_insert ha, sum_insert ha],
-  transitivity (f a).nat_degree + (∏ (x : α) in s, (f x)).nat_degree,
+  transitivity (f a).nat_degree + (∏ x in s, f x).nat_degree,
   apply polynomial.nat_degree_mul_le, linarith,
 end
 
@@ -58,39 +60,60 @@ begin
 end
 
 /-- The degree of a product of polynomials is equal to the product of the degrees, provided that the product of leading coefficients is nonzero.
-See `nat_degree_prod_eq` (without the `'`) for a version for integral domains, where this condition is automatically satisfied. -/
-lemma nat_degree_prod_eq' (h : ∏ i in s, (f i).leading_coeff ≠ 0) :
+See `nat_degree_prod` (without the `'`) for a version for integral domains, where this condition is automatically satisfied. -/
+lemma nat_degree_prod' (h : ∏ i in s, (f i).leading_coeff ≠ 0) :
   (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
 begin
   classical,
   revert h, induction s using finset.induction with a s ha hs, { simp },
   rw [prod_insert ha, prod_insert ha, sum_insert ha],
-  intro h, rw polynomial.nat_degree_mul_eq', rw hs,
+  intro h, rw polynomial.nat_degree_mul', rw hs,
   apply right_ne_zero_of_mul h,
   rwa polynomial.leading_coeff_prod', apply right_ne_zero_of_mul h,
 end
 
-lemma monic_prod_of_monic :
-  (∀ a : α, a ∈ s → monic (f a)) → monic (∏ i in s, f i) :=
-by { apply prod_induction, apply monic_mul, apply monic_one }
-
-lemma nat_degree_prod_eq_of_monic [nontrivial R] (h : ∀ i : α, i ∈ s → (f i).monic) :
+lemma nat_degree_prod_of_monic [nontrivial R] (h : ∀ i ∈ s, (f i).monic) :
   (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
 begin
-  apply nat_degree_prod_eq',
-  suffices : ∏ (i : α) in s, (f i).leading_coeff = 1, { rw this, simp },
+  apply nat_degree_prod',
+  suffices : ∏ i in s, (f i).leading_coeff = 1, { rw this, simp },
   rw prod_eq_one, intros, apply h, assumption,
 end
 
 end comm_semiring
 
+section comm_ring
+variables [comm_ring R]
+
+open monic
+-- Eventually this can be generalized with Vieta's formulas
+-- plus the connection between roots and factorization.
+lemma prod_X_sub_C_next_coeff [nontrivial R] {s : finset ι} (f : ι → R) :
+next_coeff ∏ i in s, (X - C (f i)) = -∑ i in s, f i :=
+by { rw next_coeff_prod; { simp [monic_X_sub_C] } }
+
+lemma prod_X_sub_C_coeff_card_pred [nontrivial R] (s : finset ι) (f : ι → R) (hs : 0 < s.card) :
+(∏ i in s, (X - C (f i))).coeff (s.card - 1) = - ∑ i in s, f i :=
+begin
+  convert prod_X_sub_C_next_coeff (by assumption),
+  rw next_coeff, split_ifs,
+  { rw nat_degree_prod_of_monic at h,
+    swap, { intros, apply monic_X_sub_C },
+    rw sum_eq_zero_iff at h,
+    simp_rw nat_degree_X_sub_C at h, contrapose! h, norm_num,
+    exact multiset.card_pos_iff_exists_mem.mp hs },
+  congr, rw nat_degree_prod_of_monic; { simp [nat_degree_X_sub_C, monic_X_sub_C] },
+end
+
+end comm_ring
+
 section integral_domain
-variables [integral_domain R] (f : α → polynomial R)
+variables [integral_domain R] (f : ι → polynomial R)
 
-lemma nat_degree_prod_eq (h : ∀ i ∈ s, f i ≠ 0) :
+lemma nat_degree_prod (h : ∀ i ∈ s, f i ≠ 0) :
   (∏ i in s, f i).nat_degree = ∑ i in s, (f i).nat_degree :=
 begin
-  apply nat_degree_prod_eq', rw prod_ne_zero_iff,
+  apply nat_degree_prod', rw prod_ne_zero_iff,
   intros x hx, simp [h x hx],
 end
 

src/data/polynomial/algebra_map.lean

@@ -180,6 +180,15 @@ alg_hom.ext $ λ p, by rw [eval_unique (f.comp (aeval R A x)), alg_hom.comp_appl
 theorem aeval_alg_hom_apply (f : A →ₐ[R] B) (x : A) (p) : aeval R B (f x) p = f (aeval R A x p) :=
 alg_hom.ext_iff.1 (aeval_alg_hom f x) p
 
+@[simp] lemma coe_aeval_eq_eval (r : R) :
+  (aeval R R r : polynomial R → R) = eval r := rfl
+
+lemma coeff_zero_eq_aeval_zero (p : polynomial R) : p.coeff 0 = aeval R R 0 p :=
+by simp [coeff_zero_eq_eval_zero]
+
+lemma pow_comp (p q : polynomial R) (k : ℕ) : (p ^ k).comp q = (p.comp q) ^ k :=
+by { unfold comp, rw ← coe_eval₂_ring_hom, apply ring_hom.map_pow }
+
 variables [comm_ring S] {f : R →+* S}
 
 lemma is_root_of_eval₂_map_eq_zero

src/data/polynomial/degree.lean

@@ -10,7 +10,7 @@ import data.polynomial.eval
 # Theory of degrees of polynomials
 
 Some of the main results include
-- `degree_mul_eq` : The degree of the product is the sum of degrees
+- `degree_mul` : The degree of the product is the sum of degrees
 - `leading_coeff_add_of_degree_eq` and `leading_coeff_add_of_degree_lt` :
     The leading_coefficient of a sum is determined by the leading coefficients and degrees
 - `nat_degree_comp_le` : The degree of the composition is at most the product of degrees
@@ -207,7 +207,7 @@ calc coeff (p * q) (nat_degree p + nat_degree q) =
     { intro H, exfalso, apply H, rw nat.mem_antidiagonal }
   end
 
-lemma degree_mul_eq' (h : leading_coeff p * leading_coeff q ≠ 0) :
+lemma degree_mul' (h : leading_coeff p * leading_coeff q ≠ 0) :
   degree (p * q) = degree p + degree q :=
 have hp : p ≠ 0 := by refine mt _ h; exact λ hp, by rw [hp, leading_coeff_zero, zero_mul],
 have hq : q ≠ 0 := by refine mt _ h; exact λ hq, by rw [hq, leading_coeff_zero, mul_zero],
@@ -218,21 +218,21 @@ begin
   rwa coeff_mul_degree_add_degree
 end
 
-lemma nat_degree_mul_eq' (h : leading_coeff p * leading_coeff q ≠ 0) :
+lemma nat_degree_mul' (h : leading_coeff p * leading_coeff q ≠ 0) :
   nat_degree (p * q) = nat_degree p + nat_degree q :=
 have hp : p ≠ 0 := mt leading_coeff_eq_zero.2 (λ h₁, h $ by rw [h₁, zero_mul]),
 have hq : q ≠ 0 := mt leading_coeff_eq_zero.2 (λ h₁, h $ by rw [h₁, mul_zero]),
 have hpq : p * q ≠ 0 := λ hpq, by rw [← coeff_mul_degree_add_degree, hpq, coeff_zero] at h;
   exact h rfl,
 option.some_inj.1 (show (nat_degree (p * q) : with_bot ℕ) = nat_degree p + nat_degree q,
-  by rw [← degree_eq_nat_degree hpq, degree_mul_eq' h, degree_eq_nat_degree hp,
+  by rw [← degree_eq_nat_degree hpq, degree_mul' h, degree_eq_nat_degree hp,
     degree_eq_nat_degree hq])
 
 lemma leading_coeff_mul' (h : leading_coeff p * leading_coeff q ≠ 0) :
   leading_coeff (p * q) = leading_coeff p * leading_coeff q :=
 begin
   unfold leading_coeff,
-  rw [nat_degree_mul_eq' h, coeff_mul_degree_add_degree],
+  rw [nat_degree_mul' h, coeff_mul_degree_add_degree],
   refl
 end
 
@@ -246,7 +246,7 @@ have h₂ : leading_coeff p * leading_coeff (p ^ n) ≠ 0 :=
   by rwa [pow_succ, ← ih h₁] at h,
 by rw [pow_succ, pow_succ, leading_coeff_mul' h₂, ih h₁]
 
-lemma degree_pow_eq' : ∀ {n}, leading_coeff p ^ n ≠ 0 →
+lemma degree_pow' : ∀ {n}, leading_coeff p ^ n ≠ 0 →
   degree (p ^ n) = n •ℕ (degree p)
 | 0     := λ h, by rw [pow_zero, ← C_1] at *;
   rw [degree_C h, zero_nsmul]
@@ -255,9 +255,9 @@ have h₁ : leading_coeff p ^ n ≠ 0 := λ h₁, h $
   by rw [pow_succ, h₁, mul_zero],
 have h₂ : leading_coeff p * leading_coeff (p ^ n) ≠ 0 :=
   by rwa [pow_succ, ← leading_coeff_pow' h₁] at h,
-by rw [pow_succ, degree_mul_eq' h₂, succ_nsmul, degree_pow_eq' h₁]
+by rw [pow_succ, degree_mul' h₂, succ_nsmul, degree_pow' h₁]
 
-lemma nat_degree_pow_eq' {n : ℕ} (h : leading_coeff p ^ n ≠ 0) :
+lemma nat_degree_pow' {n : ℕ} (h : leading_coeff p ^ n ≠ 0) :
   nat_degree (p ^ n) = n * nat_degree p :=
 if hp0 : p = 0 then
   if hn0 : n = 0 then by simp *
@@ -267,7 +267,7 @@ have hpn : p ^ n ≠ 0, from λ hpn0,  have h1 : _ := h,
   by rw [← leading_coeff_pow' h1, hpn0, leading_coeff_zero] at h;
   exact h rfl,
 option.some_inj.1 $ show (nat_degree (p ^ n) : with_bot ℕ) = (n * nat_degree p : ℕ),
-  by rw [← degree_eq_nat_degree hpn, degree_pow_eq' h, degree_eq_nat_degree hp0,
+  by rw [← degree_eq_nat_degree hpn, degree_pow' h, degree_eq_nat_degree hp0,
     ← with_bot.coe_nsmul]; simp
 
 @[simp] lemma leading_coeff_X_pow : ∀ n : ℕ, leading_coeff ((X : polynomial R) ^ n) = 1
@@ -370,7 +370,7 @@ theorem degree_le_iff_coeff_zero (f : polynomial R) (n : with_bot ℕ) :
 lemma degree_lt_degree_mul_X (hp : p ≠ 0) : p.degree < (p * X).degree :=
 by haveI := nonzero.of_polynomial_ne hp; exact
 have leading_coeff p * leading_coeff X ≠ 0, by simpa,
-by erw [degree_mul_eq' this, degree_eq_nat_degree hp,
+by erw [degree_mul' this, degree_eq_nat_degree hp,
     degree_X, ← with_bot.coe_one, ← with_bot.coe_add, with_bot.coe_lt_coe];
   exact nat.lt_succ_self _
 
@@ -461,7 +461,7 @@ variables [semiring R] [nontrivial R] {p q : polynomial R}
 have h : leading_coeff (X : polynomial R) * leading_coeff (X ^ n) ≠ 0,
   by rw [leading_coeff_X, leading_coeff_X_pow n, one_mul];
     exact zero_ne_one.symm,
-by rw [pow_succ, degree_mul_eq' h, degree_X, degree_X_pow, add_comm]; refl
+by rw [pow_succ, degree_mul' h, degree_X, degree_X_pow, add_comm]; refl
 
 theorem not_is_unit_X : ¬ is_unit (X : polynomial R) :=
 λ ⟨⟨_, g, hfg, hgf⟩, rfl⟩, @zero_ne_one R _ _ $ by erw [← coeff_one_zero, ← hgf, coeff_mul_X_zero]
@@ -511,6 +511,10 @@ end
 @[simp] lemma nat_degree_X_sub_C (x : R) : (X - C x).nat_degree = 1 :=
 nat_degree_eq_of_degree_eq_some $ degree_X_sub_C x
 
+@[simp]
+lemma next_coeff_X_sub_C (c : R) : next_coeff (X - C c) = - c :=
+by simp [next_coeff_of_pos_nat_degree]
+
 lemma degree_X_pow_sub_C {n : ℕ} (hn : 0 < n) (a : R) :
   degree ((X : polynomial R) ^ n - C a) = n :=
 have degree (-C a) < degree ((X : polynomial R) ^ n),
@@ -533,4 +537,44 @@ by { apply nat_degree_eq_of_degree_eq_some, simp [degree_X_pow_sub_C hn], }
 
 end nonzero_ring
 
+section integral_domain
+variables [integral_domain R] {p q : polynomial R}
+
+@[simp] lemma degree_mul : degree (p * q) = degree p + degree q :=
+if hp0 : p = 0 then by simp only [hp0, degree_zero, zero_mul, with_bot.bot_add]
+else if hq0 : q = 0 then  by simp only [hq0, degree_zero, mul_zero, with_bot.add_bot]
+else degree_mul' $ mul_ne_zero (mt leading_coeff_eq_zero.1 hp0)
+    (mt leading_coeff_eq_zero.1 hq0)
+
+@[simp] lemma degree_pow (p : polynomial R) (n : ℕ) :
+  degree (p ^ n) = n •ℕ (degree p) :=
+by induction n; [simp only [pow_zero, degree_one, zero_nsmul],
+simp only [*, pow_succ, succ_nsmul, degree_mul]]
+
+@[simp] lemma leading_coeff_mul (p q : polynomial R) : leading_coeff (p * q) =
+  leading_coeff p * leading_coeff q :=
+begin
+  by_cases hp : p = 0,
+  { simp only [hp, zero_mul, leading_coeff_zero] },
+  { by_cases hq : q = 0,
+    { simp only [hq, mul_zero, leading_coeff_zero] },
+    { rw [leading_coeff_mul'],
+      exact mul_ne_zero (mt leading_coeff_eq_zero.1 hp) (mt leading_coeff_eq_zero.1 hq) } }
+end
+
+/-- `polynomial.leading_coeff` bundled as a `monoid_hom` when `R` is an `integral_domain`, and thus
+  `leading_coeff` is multiplicative -/
+def leading_coeff_hom : polynomial R →* R :=
+{ to_fun := leading_coeff,
+  map_one' := by simp,
+  map_mul' := leading_coeff_mul }
+
+@[simp] lemma leading_coeff_hom_apply (p : polynomial R) :
+  leading_coeff_hom p = leading_coeff p := rfl
+
+@[simp] lemma leading_coeff_pow (p : polynomial R) (n : ℕ) :
+  leading_coeff (p ^ n) = leading_coeff p ^ n :=
+leading_coeff_hom.map_pow p n
+end integral_domain
+
 end polynomial