refactor(data/polynomial): Move some lemmas to monoid_algebra (#4627)

The `add_monoid_algebra.mul_apply_antidiagonal` lemma is copied verbatim from `monoid_algebra.mul_apply_antidiagonal`.

Author: eric-wieser

src/algebra/monoid_algebra.lean

@@ -114,9 +114,19 @@ instance [comm_semiring k] [comm_monoid G] : comm_semiring (monoid_algebra k G)
   end,
   .. monoid_algebra.semiring }
 
+instance [semiring k] [nontrivial k] [monoid G] : nontrivial (monoid_algebra k G) :=
+begin
+  refine nontrivial_of_ne 0 1 _, intro h,
+  have : (0 : G →₀ k) 1 = 0 := rfl,
+  simpa [h, one_def] using this,
+end
+
 /-! #### Derived instances -/
 section derived_instances
 
+instance [semiring k] [subsingleton k] : unique (monoid_algebra k G) :=
+finsupp.unique_of_right
+
 instance [ring k] : add_group (monoid_algebra k G) :=
 finsupp.add_group
 
@@ -532,9 +542,19 @@ instance [comm_semiring k] [add_comm_monoid G] : comm_semiring (add_monoid_algeb
   end,
   .. add_monoid_algebra.semiring }
 
+instance [semiring k] [nontrivial k] [add_monoid G] : nontrivial (add_monoid_algebra k G) :=
+begin
+  refine nontrivial_of_ne 0 1 _, intro h,
+  have : (0 : G →₀ k) 0 = 0 := rfl,
+  simpa [h, one_def] using this,
+end
+
 /-! #### Derived instances -/
 section derived_instances
 
+instance [semiring k] [subsingleton k] : unique (add_monoid_algebra k G) :=
+finsupp.unique_of_right
+
 instance [ring k] : add_group (add_monoid_algebra k G) :=
 finsupp.add_group
 
@@ -571,6 +591,25 @@ begin
   simp only [finsupp.sum_apply, single_apply],
 end
 
+lemma mul_apply_antidiagonal (f g : add_monoid_algebra k G) (x : G) (s : finset (G × G))
+  (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 + p.2 = x) :
+  (f * g) x = ∑ p in s, (f p.1 * g p.2) :=
+let F : G × G → k := λ p, if p.1 + p.2 = x then f p.1 * g p.2 else 0 in
+calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂)) :
+  mul_apply f g x
+... = ∑ p in f.support.product g.support, F p : finset.sum_product.symm
+... = ∑ p in (f.support.product g.support).filter (λ p : G × G, p.1 + p.2 = x), f p.1 * g p.2 :
+  (finset.sum_filter _ _).symm
+... = ∑ p in s.filter (λ p : G × G, p.1 ∈ f.support ∧ p.2 ∈ g.support), f p.1 * g p.2 :
+  sum_congr (by { ext, simp only [mem_filter, mem_product, hs, and_comm] }) (λ _ _, rfl)
+... = ∑ p in s, f p.1 * g p.2 : sum_subset (filter_subset _) $ λ p hps hp,
+  begin
+    simp only [mem_filter, mem_support_iff, not_and, not_not] at hp ⊢,
+    by_cases h1 : f p.1 = 0,
+    { rw [h1, zero_mul] },
+    { rw [hp hps h1, mul_zero] }
+  end
+
 lemma support_mul (a b : add_monoid_algebra k G) :
   (a * b).support ⊆ a.support.bind (λa₁, b.support.bind $ λa₂, {a₁ + a₂}) :=
 subset.trans support_sum $ bind_mono $ assume a₁ _,

src/data/polynomial/algebra_map.lean

@@ -234,7 +234,7 @@ begin
     congr, apply_congr, skip,
     rw [coeff_mul_X_sub_C, sub_mul, mul_assoc, ←pow_succ],
   },
-  simp [sum_range_sub', coeff_single],
+  simp [sum_range_sub', coeff_monomial],
 end
 
 theorem not_is_unit_X_sub_C [nontrivial R] {r : R} : ¬ is_unit (X - C r) :=

src/data/polynomial/basic.lean

@@ -33,13 +33,12 @@ variables {R : Type u} {a : R} {m n : ℕ}
 section semiring
 variables [semiring R] {p q : polynomial R}
 
-instance : inhabited (polynomial R) := finsupp.inhabited
+instance : inhabited (polynomial R) := add_monoid_algebra.inhabited _ _
 instance : semiring (polynomial R) := add_monoid_algebra.semiring
 instance : has_scalar R (polynomial R) := add_monoid_algebra.has_scalar
 instance : semimodule R (polynomial R) := add_monoid_algebra.semimodule
 
-instance subsingleton [subsingleton R] : subsingleton (polynomial R) :=
-⟨λ _ _, ext (λ _, subsingleton.elim _ _)⟩
+instance [subsingleton R] : unique (polynomial R) := add_monoid_algebra.unique
 
 @[simp] lemma support_zero : (0 : polynomial R).support = ∅ := rfl
 
@@ -48,15 +47,15 @@ def monomial (n : ℕ) (a : R) : polynomial R := finsupp.single n a
 
 @[simp] lemma monomial_zero_right (n : ℕ) :
   monomial n (0 : R) = 0 :=
-by simp [monomial]
+finsupp.single_zero
 
 lemma monomial_add (n : ℕ) (r s : R) :
   monomial n (r + s) = monomial n r + monomial n s :=
-by simp [monomial]
+finsupp.single_add
 
 lemma monomial_mul_monomial (n m : ℕ) (r s : R) :
   monomial n r * monomial m s = monomial (n + m) (r * s) :=
-by simp only [monomial, single_mul_single]
+add_monoid_algebra.single_mul_single
 
 
 /-- `X` is the polynomial variable (aka indeterminant). -/
@@ -80,19 +79,12 @@ by rw [mul_assoc, X_pow_mul, ←mul_assoc]
 lemma commute_X (p : polynomial R) : commute X p := X_mul
 
 /-- coeff p n is the coefficient of X^n in p -/
-def coeff (p : polynomial R) := p.to_fun
+def coeff (p : polynomial R) : ℕ → R := @coe_fn (ℕ →₀ R) _ p
 
 @[simp] lemma coeff_mk (s) (f) (h) : coeff (finsupp.mk s f h : polynomial R) = f := rfl
 
 lemma coeff_monomial : coeff (monomial n a) m = if n = m then a else 0 :=
-by { dsimp [monomial, single, finsupp.single], congr, }
-
-/--
-This lemma is needed for occasions when we break through the abstraction from
-`polynomial` to `finsupp`; ideally it wouldn't be necessary at all.
--/
-lemma coeff_single : coeff (single n a) m = if n = m then a else 0 :=
-coeff_monomial
+by { dsimp [monomial, coeff], rw finsupp.single_apply, congr }
 
 @[simp] lemma coeff_zero (n : ℕ) : coeff (0 : polynomial R) n = 0 := rfl
 
@@ -105,37 +97,20 @@ coeff_monomial
 lemma coeff_X : coeff (X : polynomial R) n = if 1 = n then 1 else 0 := coeff_monomial
 
 theorem ext_iff {p q : polynomial R} : p = q ↔ ∀ n, coeff p n = coeff q n :=
-⟨λ h n, h ▸ rfl, finsupp.ext⟩
+finsupp.ext_iff
 
 @[ext] lemma ext {p q : polynomial R} : (∀ n, coeff p n = coeff q n) → p = q :=
-(@ext_iff _ _ p q).2
+finsupp.ext
 
 -- this has the same content as the subsingleton
 lemma eq_zero_of_eq_zero (h : (0 : R) = (1 : R)) (p : polynomial R) : p = 0 :=
 by rw [←one_smul R p, ←h, zero_smul]
 
 lemma support_monomial (n) (a : R) (H : a ≠ 0) : (monomial n a).support = singleton n :=
-begin
-  ext,
-  have m3 : a_1 ∈ (monomial n a).support ↔ coeff (monomial n a) a_1 ≠ 0 := (monomial n a).mem_support_to_fun a_1,
-  rw [finset.mem_singleton, m3, coeff_monomial],
-  split_ifs,
-    { rwa [h, eq_self_iff_true, iff_true], },
-    { rw [← @not_not (a_1=n)],
-      apply not_congr,
-      rw [eq_self_iff_true, true_iff, ← ne.def],
-      symmetry,
-      assumption, },
-end
+finsupp.support_single_ne_zero H
 
 lemma support_monomial' (n) (a : R) : (monomial n a).support ⊆ singleton n :=
-begin
-  by_cases h : a = 0,
-  { rw [h, monomial_zero_right, support_zero],
-    exact finset.empty_subset {n}, },
-  { rw support_monomial n a h,
-    exact finset.subset.refl {n}, },
-end
+finsupp.support_single_subset
 
 lemma X_pow_eq_monomial (n) : X ^ n = monomial n (1:R) :=
 begin
@@ -167,7 +142,6 @@ section comm_semiring
 variables [comm_semiring R]
 
 instance : comm_semiring (polynomial R) := add_monoid_algebra.comm_semiring
-instance : comm_monoid (polynomial R) := comm_semiring.to_comm_monoid (polynomial R)
 
 end comm_semiring
 
@@ -188,11 +162,7 @@ instance [comm_ring R] : comm_ring (polynomial R) := add_monoid_algebra.comm_rin
 section nonzero_semiring
 
 variables [semiring R] [nontrivial R]
-instance : nontrivial (polynomial R) :=
-begin
-  refine nontrivial_of_ne 0 1 _, intro h,
-  have := coeff_zero 0, revert this, rw h, simp,
-end
+instance : nontrivial (polynomial R) := add_monoid_algebra.nontrivial
 
 lemma X_ne_zero : (X : polynomial R) ≠ 0 :=
 mt (congr_arg (λ p, coeff p 1)) (by simp)

src/data/polynomial/coeff.lean

@@ -48,9 +48,7 @@ by { rw [mem_support_to_fun, not_not], refl, }
 variable (R)
 /-- The nth coefficient, as a linear map. -/
 def lcoeff (n : ℕ) : polynomial R →ₗ[R] R :=
-{ to_fun := λ f, coeff f n,
-  map_add' := λ f g, coeff_add f g n,
-  map_smul' := λ r p, coeff_smul p r n }
+finsupp.leval n
 variable {R}
 
 @[simp] lemma lcoeff_apply (n : ℕ) (f : polynomial R) : lcoeff R n f = coeff f n := rfl
@@ -61,24 +59,7 @@ variable {R}
 
 lemma coeff_mul (p q : polynomial R) (n : ℕ) :
   coeff (p * q) n = ∑ x in nat.antidiagonal n, coeff p x.1 * coeff q x.2 :=
-have hite : ∀ a : ℕ × ℕ, ite (a.1 + a.2 = n) (coeff p (a.fst) * coeff q (a.snd)) 0 ≠ 0
-    → a.1 + a.2 = n, from λ a ha, by_contradiction
-  (λ h, absurd (eq.refl (0 : R)) (by rwa if_neg h at ha)),
-calc coeff (p * q) n = ∑ a in p.support, ∑ b in q.support,
-    ite (a + b = n) (coeff p a * coeff q b) 0 :
-  by { simp only [add_monoid_algebra.mul_def, coeff_sum, coeff_single], refl }
-... = ∑ v in p.support.product q.support, ite (v.1 + v.2 = n) (coeff p v.1 * coeff q v.2) 0 :
-  by rw sum_product
-... = ∑ x in nat.antidiagonal n, coeff p x.1 * coeff q x.2 :
-begin
-  refine sum_bij_ne_zero (λ x _ _, x)
-  (λ x _ hx, nat.mem_antidiagonal.2 (hite x hx)) (λ _ _ _ _ _ _ h, h)
-  (λ x h₁ h₂, ⟨x, _, _, rfl⟩) _,
-  { rw [mem_product, mem_support_iff, mem_support_iff],
-    exact ne_zero_and_ne_zero_of_mul h₂ },
-  { rw nat.mem_antidiagonal at h₁, rwa [if_pos h₁] },
-  { intros x h hx, rw [if_pos (hite x hx)] }
-end
+add_monoid_algebra.mul_apply_antidiagonal p q n _ (λ x, nat.mem_antidiagonal)
 
 @[simp] lemma mul_coeff_zero (p q : polynomial R) : coeff (p * q) 0 = coeff p 0 * coeff q 0 :=
 by simp [coeff_mul]
@@ -94,27 +75,14 @@ lemma coeff_C_mul_X (x : R) (k n : ℕ) :
 by rw [← single_eq_C_mul_X]; simp [monomial, single, eq_comm, coeff]; congr
 
 @[simp] lemma coeff_C_mul (p : polynomial R) : coeff (C a * p) n = a * coeff p n :=
-begin
-  conv in (a * _) { rw [← @sum_single _ _ _ p, coeff_sum] },
-  rw [add_monoid_algebra.mul_def, ←monomial_zero_left, monomial, sum_single_index],
-  { simp only [coeff_single, finsupp.mul_sum, coeff_sum],
-    apply sum_congr rfl,
-    assume i hi, by_cases i = n; simp [h] },
-  { simp [finsupp.sum] }
-end
+add_monoid_algebra.single_zero_mul_apply p a n
 
 lemma C_mul' (a : R) (f : polynomial R) : C a * f = a • f :=
 ext $ λ n, coeff_C_mul f
 
 @[simp] lemma coeff_mul_C (p : polynomial R) (n : ℕ) (a : R) :
   coeff (p * C a) n = coeff p n * a :=
-begin
-  conv_rhs { rw [← @finsupp.sum_single _ _ _ p, coeff_sum] },
-  rw [add_monoid_algebra.mul_def, ←monomial_zero_left], simp_rw [sum_single_index],
-  { simp only [coeff_single, finsupp.sum_mul, coeff_sum],
-    apply sum_congr rfl,
-    assume i hi, by_cases i = n; simp [h], },
-end
+add_monoid_algebra.mul_single_zero_apply p a n
 
 lemma coeff_X_pow (k n : ℕ) :
   coeff (X^k : polynomial R) n = if n = k then 1 else 0 :=