refactor(data/mv_polynomial): upgrade monomial to a linear_map (#…

…9870)

src/data/mv_polynomial/basic.lean

@@ -130,7 +130,7 @@ end instances
 variables [comm_semiring R] [comm_semiring S₁] {p q : mv_polynomial σ R}
 
 /-- `monomial s a` is the monomial with coefficient `a` and exponents given by `s`  -/
-def monomial (s : σ →₀ ℕ) (a : R) : mv_polynomial σ R := single s a
+def monomial (s : σ →₀ ℕ) : R →ₗ[R] mv_polynomial σ R := lsingle s
 
 lemma single_eq_monomial (s : σ →₀ ℕ) (a : R) : single s a = monomial s a := rfl
 
@@ -197,55 +197,70 @@ theorem C_mul' : mv_polynomial.C a * p = a • p :=
 
 lemma smul_eq_C_mul (p : mv_polynomial σ R) (a : R) : a • p = C a * p := C_mul'.symm
 
-lemma X_pow_eq_single : X n ^ e = monomial (single n e) (1 : R) :=
-begin
-  induction e,
-  { simp [X], refl },
-  { simp [pow_succ, e_ih],
-    simp [X, monomial, single_mul_single, nat.succ_eq_add_one, add_comm] }
-end
+lemma C_eq_smul_one : (C a : mv_polynomial σ R) = a • 1 :=
+by rw [← C_mul', mul_one]
+
+lemma monomial_pow : monomial s a ^ e = monomial (e • s) (a ^ e) :=
+add_monoid_algebra.single_pow e
+
+@[simp] lemma monomial_mul {s s' : σ →₀ ℕ} {a b : R} :
+  monomial s a * monomial s' b = monomial (s + s') (a * b) :=
+add_monoid_algebra.single_mul_single
+
+variables (σ R)
+
+/-- `λ s, monomial s 1` as a homomorphism. -/
+def monomial_one_hom : multiplicative (σ →₀ ℕ) →* mv_polynomial σ R :=
+add_monoid_algebra.of _ _
+
+variables {σ R}
+
+@[simp] lemma monomial_one_hom_apply :
+  monomial_one_hom R σ s = (monomial s 1 : mv_polynomial σ R) := rfl
+
+lemma X_pow_eq_monomial : X n ^ e = monomial (single n e) (1 : R) :=
+by simp [X, monomial_pow]
 
 lemma monomial_add_single : monomial (s + single n e) a = (monomial s a * X n ^ e) :=
-by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
+by rw [X_pow_eq_monomial, monomial_mul, mul_one]
 
 lemma monomial_single_add : monomial (single n e + s) a = (X n ^ e * monomial s a) :=
-by rw [X_pow_eq_single, monomial, monomial, monomial, single_mul_single]; simp
+by rw [X_pow_eq_monomial, monomial_mul, one_mul]
 
 lemma monomial_eq_C_mul_X {s : σ} {a : R} {n : ℕ} :
   monomial (single s n) a = C a * (X s)^n :=
 by rw [← zero_add (single s n), monomial_add_single, C_apply]
 
-@[simp] lemma monomial_add {s : σ →₀ ℕ} {a b : R} :
-  monomial s a + monomial s b = monomial s (a + b) :=
-single_add.symm
-
-@[simp] lemma monomial_mul {s s' : σ →₀ ℕ} {a b : R} :
-  monomial s a * monomial s' b = monomial (s + s') (a * b) :=
-add_monoid_algebra.single_mul_single
-
 @[simp] lemma monomial_zero {s : σ →₀ ℕ}: monomial s (0 : R) = 0 :=
 single_zero
 
-@[simp] lemma sum_monomial_eq  {A : Type*} [add_comm_monoid A]
+@[simp] lemma monomial_zero' : (monomial (0 : σ →₀ ℕ) : R → mv_polynomial σ R) = C := rfl
+
+@[simp] lemma sum_monomial_eq {A : Type*} [add_comm_monoid A]
   {u : σ →₀ ℕ} {r : R} {b : (σ →₀ ℕ) → R → A} (w : b u 0 = 0) :
   sum (monomial u r) b = b u r :=
 sum_single_index w
 
 @[simp] lemma sum_C {A : Type*} [add_comm_monoid A]
   {b : (σ →₀ ℕ) → R → A} (w : b 0 0 = 0) :
   sum (C a) b = b 0 a :=
-by simp [C_apply, w]
+sum_monomial_eq w
+
+lemma monomial_sum_one {α : Type*} (s : finset α) (f : α → (σ →₀ ℕ)) :
+  (monomial (∑ i in s, f i) 1 : mv_polynomial σ R) = ∏ i in s, monomial (f i) 1 :=
+(monomial_one_hom R σ).map_prod (λ i, multiplicative.of_add (f i)) s
+
+lemma monomial_sum_index {α : Type*} (s : finset α) (f : α → (σ →₀ ℕ)) (a : R) :
+  (monomial (∑ i in s, f i) a) = C a * ∏ i in s, monomial (f i) 1 :=
+by rw [← monomial_sum_one, C_mul', ← (monomial _).map_smul, smul_eq_mul, mul_one]
+
+lemma monomial_finsupp_sum_index {α β : Type*} [has_zero β] (f : α →₀ β)
+  (g : α → β → (σ →₀ ℕ)) (a : R) :
+  (monomial (f.sum g) a) = C a * f.prod (λ a b, monomial (g a b) 1) :=
+monomial_sum_index _ _ _
 
 lemma monomial_eq : monomial s a = C a * (s.prod $ λn e, X n ^ e : mv_polynomial σ R) :=
-begin
-  apply @finsupp.induction σ ℕ _ _ s,
-  { simp only [C_apply, prod_zero_index]; exact (mul_one _).symm },
-  { assume n e s hns he ih,
-    rw [monomial_single_add, ih, prod_add_index, prod_single_index, mul_left_comm],
-    { simp only [pow_zero], },
-    { intro a, simp only [pow_zero], },
-    { intros, rw pow_add, }, }
-end
+by simp only [X_pow_eq_monomial, ← monomial_finsupp_sum_index, finsupp.sum_single]
 
 @[recursor 5]
 lemma induction_on {M : mv_polynomial σ R → Prop} (p : mv_polynomial σ R)
@@ -324,6 +339,8 @@ The finite set of all `m : σ →₀ ℕ` such that `X^m` has a non-zero coeffic
 def support (p : mv_polynomial σ R) : finset (σ →₀ ℕ) :=
 p.support
 
+lemma finsupp_support_eq_support (p : mv_polynomial σ R) : finsupp.support p = p.support := rfl
+
 lemma support_monomial [decidable (a = 0)] : (monomial s a).support = if a = 0 then ∅ else {s} :=
 by convert rfl
 
@@ -583,7 +600,7 @@ finsupp.sum_add_index
 finsupp.sum_single_index (by simp [f.map_zero])
 
 @[simp] lemma eval₂_C (a) : (C a).eval₂ f g = f a :=
-by simp [eval₂_monomial, C, prod_zero_index]
+by rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]
 
 @[simp] lemma eval₂_one : (1 : mv_polynomial σ R).eval₂ f g = 1 :=
 (eval₂_C _ _ _).trans f.map_one
@@ -606,12 +623,15 @@ begin
           f.map_one, -add_comm] }
 end
 
+lemma eval₂_mul_C : (p * C a).eval₂ f g = p.eval₂ f g * f a :=
+(eval₂_mul_monomial _ _).trans $ by simp
+
 @[simp] lemma eval₂_mul : ∀{p}, (p * q).eval₂ f g = p.eval₂ f g * q.eval₂ f g :=
 begin
   apply mv_polynomial.induction_on q,
-  { simp [C, eval₂_monomial, eval₂_mul_monomial, prod_zero_index] },
+  { simp [eval₂_C, eval₂_mul_C] },
   { simp [mul_add, eval₂_add] {contextual := tt} },
-  { simp [X, eval₂_monomial, eval₂_mul_monomial, (mul_assoc _ _ _).symm] { contextual := tt} }
+  { simp [X, eval₂_monomial, eval₂_mul_monomial, ← mul_assoc] { contextual := tt} }
 end
 
 @[simp] lemma eval₂_pow {p:mv_polynomial σ R} : ∀{n:ℕ}, (p ^ n).eval₂ f g = (p.eval₂ f g)^n

src/data/mv_polynomial/comm_ring.lean

@@ -64,13 +64,6 @@ variables (σ a a')
 @[simp] lemma coeff_sub (m : σ →₀ ℕ) (p q : mv_polynomial σ R) :
   coeff m (p - q) = coeff m p - coeff m q := finsupp.sub_apply _ _ _
 
-@[simp] lemma monomial_neg (m : σ →₀ ℕ) (a : R) : -(monomial m a) = monomial m (-a) :=
-single_neg.symm
-
-@[simp] lemma monomial_sub (m : σ →₀ ℕ) (a b : R) :
-  monomial m a - monomial m b = monomial m (a - b) :=
-single_sub.symm
-
 @[simp] lemma support_neg : (- p).support = p.support :=
 finsupp.support_neg
 

src/data/mv_polynomial/monad.lean

@@ -143,7 +143,7 @@ variable (f : σ → mv_polynomial τ R)
 
 @[simp]
 lemma bind₁_C_right (f : σ → mv_polynomial τ R) (x) : bind₁ f (C x) = C x :=
-by simp [bind₁, C, aeval_monomial, finsupp.prod_zero_index]; refl
+by simp [bind₁, algebra_map_eq]
 
 @[simp]
 lemma bind₂_C_right (f : R →+* mv_polynomial σ S) (r : R) : bind₂ f (C r) = f r :=

src/data/mv_polynomial/pderiv.lean

@@ -62,12 +62,12 @@ def pderiv (i : σ) : mv_polynomial σ R →ₗ[R] mv_polynomial σ R :=
   map_smul' := begin
     intros c x,
     rw [sum_smul_index', smul_sum],
-    { dsimp, simp_rw [monomial, smul_single, smul_eq_mul, mul_assoc] },
+    { dsimp, simp_rw [← (monomial _).map_smul, smul_eq_mul, mul_assoc] },
     { intros s,
       simp only [monomial_zero, zero_mul] }
   end,
   map_add' := λ f g, sum_add_index (by simp only [monomial_zero, forall_const, zero_mul])
-    (by simp only [add_mul, forall_const, eq_self_iff_true, monomial_add]), }
+    (by simp only [add_mul, forall_const, eq_self_iff_true, (monomial _).map_add]), }
 
 @[simp]
 lemma pderiv_monomial {i : σ} :
@@ -96,18 +96,10 @@ end
 lemma pderiv_X [decidable_eq σ] {i j : σ} :
   pderiv i (X j : mv_polynomial σ R) = if i = j then 1 else 0 :=
 begin
-  dsimp [pderiv],
-  erw finsupp.sum_single_index,
-  simp only [mul_boole, if_congr, finsupp.single_apply, nat.cast_zero, nat.cast_one, nat.cast_ite],
-  by_cases h : i = j,
-  { rw [if_pos h, if_pos h.symm],
-    subst h,
-    congr,
-    ext j,
-    simp, },
-  { rw [if_neg h, if_neg (ne.symm h)],
-    simp, },
-  { simp, },
+  refine pderiv_monomial.trans _,
+  rcases eq_or_ne i j with (rfl|hne),
+  { simp },
+  { simp [hne, hne.symm] }
 end
 
 @[simp] lemma pderiv_X_self {i : σ} : pderiv i (X i : mv_polynomial σ R) = 1 :=
@@ -131,9 +123,9 @@ lemma pderiv_monomial_mul {i : σ} {s' : σ →₀ ℕ} :
   pderiv i (monomial s a * monomial s' a') =
     pderiv i (monomial s a) * monomial s' a' + monomial s a * pderiv i (monomial s' a') :=
 begin
-  simp [monomial_sub_single_one_add, monomial_add_sub_single_one],
-  congr,
-  ring,
+  simp only [monomial_sub_single_one_add, monomial_add_sub_single_one, pderiv_monomial,
+    pi.add_apply, monomial_mul, nat.cast_add, coe_add],
+  rw [mul_add, (monomial _).map_add, ← mul_assoc, mul_right_comm a _ a']
 end
 
 @[simp]

src/data/mv_polynomial/rename.lean

@@ -91,14 +91,9 @@ end
 lemma rename_eq (f : σ → τ) (p : mv_polynomial σ R) :
   rename f p = finsupp.map_domain (finsupp.map_domain f) p :=
 begin
-  simp only [rename, aeval_def, eval₂, finsupp.map_domain],
-  congr' with s a : 2,
-  rw [← monomial, monomial_eq, finsupp.prod_sum_index],
-  congr' with n i : 2,
-  rw [finsupp.prod_single_index],
-  exact pow_zero _,
-  exact assume a, pow_zero _,
-  exact assume a b c, pow_add _ _ _
+  simp only [rename, aeval_def, eval₂, finsupp.map_domain, algebra_map_eq, X_pow_eq_monomial,
+     ← monomial_finsupp_sum_index],
+  refl
 end
 
 lemma rename_injective (f : σ → τ) (hf : function.injective f) :

src/ring_theory/mv_polynomial/basic.lean

@@ -57,15 +57,12 @@ lemma map_range_eq_map {R S : Type*} [comm_ring R] [comm_ring S] (p : mv_polynom
   (f : R →+* S) :
   finsupp.map_range f f.map_zero p = map f p :=
 begin
-  rw [← finsupp.sum_single p, finsupp.sum],
-  -- It's not great that we need to use an `erw` here,
-  -- but hopefully it will become smoother when we move entirely away from `is_semiring_hom`.
-  -- [note added later: we have moved entirely away from it but we still need the `erw` because
-  -- `finsupp.map_range ⇑↑f` is not syntactically `finsupp.map_range ⇑f` ]
-  erw [finsupp.map_range_finset_sum (f : R →+ S)],
-  rw (map f).map_sum,
+  -- `finsupp.map_range_finset_sum` expects `f : R →+ S`
+  change finsupp.map_range (f : R →+ S) (f : R →+ S).map_zero p = map f p,
+  rw [p.as_sum, finsupp.map_range_finset_sum, (map f).map_sum],
   refine finset.sum_congr rfl (assume n _, _),
-  rw [finsupp.map_range_single, ← monomial, ← monomial, map_monomial], refl,
+  rw [map_monomial, ← single_eq_monomial, finsupp.map_range_single, single_eq_monomial,
+    f.coe_add_monoid_hom],
 end
 
 end homomorphism

src/ring_theory/polynomial/symmetric.lean

@@ -193,7 +193,7 @@ lemma support_esymm'' (n : ℕ) [decidable_eq σ] [nontrivial R] :
     (λ t, (finsupp.single (∑ (i : σ) in t, finsupp.single i 1) (1:R)).support) :=
 begin
   rw esymm_eq_sum_monomial,
-  simp only [monomial],
+  simp only [← single_eq_monomial],
   convert finsupp.support_sum_eq_bUnion (powerset_len n (univ : finset σ)) _,
   intros s t hst d,
   simp only [finsupp.support_single_ne_zero one_ne_zero, and_imp, inf_eq_inter, mem_inter,

src/ring_theory/witt_vector/witt_polynomial.lean

@@ -73,7 +73,7 @@ It is defined as:
 
 `∑_{i ≤ n} p^i X_i^{p^{n-i}} ∈ R[X_0, X_1, X_2, …]`. -/
 noncomputable def witt_polynomial (n : ℕ) : mv_polynomial ℕ R :=
-∑ i in range (n+1), monomial (single i (p ^ (n - i))) (p ^ i)
+∑ i in range (n+1), monomial (single i (p ^ (n - i))) (p ^ i : R)
 
 lemma witt_polynomial_eq_sum_C_mul_X_pow (n : ℕ) :
   witt_polynomial p R n = ∑ i in range (n+1), C (p ^ i : R) * X i ^ (p ^ (n - i)) :=
@@ -159,12 +159,9 @@ lemma witt_polynomial_vars [char_zero R] (n : ℕ) :
 begin
   have : ∀ i, (monomial (finsupp.single i (p ^ (n - i))) (p ^ i : R)).vars = {i},
   { intro i,
-    rw vars_monomial_single,
-    { rw ← pos_iff_ne_zero,
-      apply pow_pos hp.1.pos },
-    { rw [← nat.cast_pow, nat.cast_ne_zero],
-      apply ne_of_gt,
-      apply pow_pos hp.1.pos i } },
+    refine vars_monomial_single i (pow_ne_zero _ hp.1.ne_zero) _,
+    rw [← nat.cast_pow, nat.cast_ne_zero],
+    exact pow_ne_zero i hp.1.ne_zero },
   rw [witt_polynomial, vars_sum_of_disjoint],
   { simp only [this, int.nat_cast_eq_coe_nat, bUnion_singleton_eq_self], },
   { simp only [this, int.nat_cast_eq_coe_nat],