refactor(data/finsupp): generalize module construction for finsupp

Author: johoelzl

algebra/linear_algebra/basic.lean

@@ -67,30 +67,15 @@ end finsupp
 namespace lc
 variables [ring α] [module α β]
 
-instance : has_scalar α (lc α β) :=
-⟨λa (v : β →₀ α), v.map_range ((*) a) (mul_zero a)⟩
+instance : has_scalar α (lc α β) := finsupp.to_has_scalar
 
-@[simp] lemma smul_apply {a : α} {v : lc α β} {b : β} :
-  (a • v) b = a * v b :=
-rfl
-
-instance : module α (lc α β) :=
-{ smul     := (•),
-  smul_add := assume a x y, finsupp.ext $ by simp [mul_add],
-  add_smul := assume a x y, finsupp.ext $ by simp [add_mul],
-  one_smul := assume x, finsupp.ext $ by simp,
-  mul_smul := assume r s x, finsupp.ext $ by simp [mul_assoc],
-  .. finsupp.add_comm_group }
-
-lemma sum_smul_index {γ : Type x} [add_comm_monoid γ] {g : lc α β} {a : α} {h : β → α → γ}
-  (h0 : ∀i, h i 0 = 0) : (a • g).sum h = g.sum (λi b, h i (a * b)) :=
-finsupp.sum_map_range_index h0
+instance : module α (lc α β) := finsupp.to_module
 
 lemma is_linear_map_sum [module α γ] [module α δ] {f : β → α → γ} {g : δ → lc α β}
   (hf : ∀b, is_linear_map (f b)) (hg : is_linear_map g) : is_linear_map (λd, (g d).sum f) :=
 ⟨assume d₁ d₂, by simp [hg.add, finsupp.sum_add_index, (hf _).zero, (hf _).add],
   assume a d,
-    by simp [hg.smul, sum_smul_index, (hf _).zero, finsupp.smul_sum, ((hf _).smul _ _).symm]⟩
+    by simp [hg.smul, finsupp.sum_smul_index, (hf _).zero, finsupp.smul_sum, ((hf _).smul _ _).symm]⟩
 
 end lc
 
@@ -144,7 +129,7 @@ def span (s : set β) : set β := { x | ∃(v : lc α β), (∀x∉s, v x = 0) 
   add_  := assume x y ⟨vx, hx, eqx⟩ ⟨vy, hy, eqy⟩, ⟨vx + vy,
     by simp [hx, hy, eqx, eqy, finsupp.sum_add_index, add_smul] {contextual := tt}⟩,
   smul  := assume a b ⟨v, hv, veq⟩, ⟨a • v,
-    by simp [hv, veq, lc.sum_smul_index, finsupp.smul_sum, smul_smul] {contextual := tt}⟩ }
+    by simp [hv, veq, finsupp.sum_smul_index, finsupp.smul_sum, smul_smul] {contextual := tt}⟩ }
 
 lemma subset_span : s ⊆ span s :=
 assume b (hb : b ∈ s),
@@ -377,7 +362,7 @@ repr_eq hs (is_submodule.add hb hb')
 repr_eq hs (is_submodule.smul _ hb)
   (by simp [repr_eq_zero] {contextual := tt})
   (calc (a • hs.repr b).sum (λb a, a • b) = (hs.repr b).sum (λb a', a • (a' • b)) :
-      by simp [lc.sum_smul_index, add_smul, smul_smul]
+      by simp [finsupp.sum_smul_index, add_smul, smul_smul]
     ... = a • (hs.repr b).sum (λb a', a' • b) : finsupp.smul_sum.symm
     ... = a • b : by rw [repr_sum_eq hs hb])
 
@@ -652,7 +637,7 @@ iff.intro
         have l.sum (λb a', (a * a') • b) = a • l.sum (λb a, a • b),
           by simp [finsupp.smul_sum, smul_smul],
         by simp [-sub_eq_add_neg, add_smul, finsupp.sum_add_index, finsupp.sum_single_index,
-                lc.sum_smul_index, this, eq]⟩)
+                finsupp.sum_smul_index, this, eq]⟩)
 
 lemma linear_independent_singleton {b : β} (hb : b ≠ 0) : linear_independent ({b} : set β) :=
 linear_independent_iff_not_mem_span.mpr $ by simp [hb] {contextual := tt}

algebra/linear_algebra/multivariate_polynomial.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 
 Multivariate Polynomial
 -/
-import data.finsupp
+import data.finsupp algebra.linear_algebra.basic
 noncomputable theory
 
 open classical set function finsupp lattice
@@ -241,4 +241,12 @@ end total_degree
 
 end comm_semiring
 
+section comm_ring
+variable [comm_ring α]
+instance : ring (mv_polynomial σ α) := finsupp.to_ring
+instance : has_scalar α (mv_polynomial σ α) := finsupp.to_has_scalar
+instance : module α (mv_polynomial σ α) := finsupp.to_module
+
+end comm_ring
+
 end mv_polynomial

data/finsupp.lean

@@ -21,7 +21,7 @@ The best is to define a copy and select the instances best suited.
 
 -/
 
-import data.set.finite data.finset algebra.big_operators
+import data.set.finite data.finset algebra.big_operators algebra.module
 noncomputable theory
 
 open classical set function
@@ -38,7 +38,8 @@ def finsupp (α : Type u) (β : Type v) [has_zero β] := {f : α → β // finit
 infix →₀ := finsupp
 
 namespace finsupp
-variables {α : Type u} {β : Type v} {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
+variables {α : Type u} {β : Type v} {γ : Type w}
+  {α₁ : Type u₁} {α₂ : Type u₂} {β₁ : Type v₁} {β₂ : Type v₂}
 
 section
 variable [has_zero β]
@@ -156,27 +157,27 @@ finset.ext.mpr $ assume a, by by_cases p a; simp *
 end filter
 
 -- [to_additive finsupp.sum] for finsupp.prod doesn't work, the equation lemmas are not generated
-def sum {γ : Type w} [has_zero β] [add_comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
+def sum [has_zero β] [add_comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
 f.support.sum (λa, g a (f a))
 
 @[to_additive finsupp.sum]
-def prod {γ : Type w} [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
+def prod [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
 f.support.prod (λa, g a (f a))
 attribute [to_additive finsupp.sum.equations._eqn_1] finsupp.prod.equations._eqn_1
 
 @[to_additive finsupp.sum_map_range_index]
-lemma prod_map_range_index {γ : Type w} [has_zero β₁] [has_zero β₂] [comm_monoid γ]
+lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ]
   {f : β₁ → β₂} {hf : f 0 = 0} {g : α →₀ β₁} {h : α → β₂ → γ} (h0 : ∀a, h a 0 = 1) :
   (map_range f hf g).prod h = g.prod (λa b, h a (f b)) :=
 finset.prod_subset support_map_range $ by simp [h0] {contextual := tt}
 
 @[to_additive finsupp.sum_zero_index]
-lemma prod_zero_index {γ : Type w} [add_comm_monoid β] [comm_monoid γ] {h : α → β → γ} :
+lemma prod_zero_index [add_comm_monoid β] [comm_monoid γ] {h : α → β → γ} :
   (0 : α →₀ β).prod h = 1 :=
 by simp [finsupp.prod]
 
 @[to_additive finsupp.sum_single_index]
-lemma prod_single_index {γ : Type w} [add_comm_monoid β] [comm_monoid γ] {a : α} {b : β}
+lemma prod_single_index [add_comm_monoid β] [comm_monoid γ] {a : α} {b : β}
   {h : α → β → γ} (h_zero : h a 0 = 1) : (single a b).prod h = h a b :=
 begin
   by_cases b = 0 with h,
@@ -226,18 +227,13 @@ instance [add_group β] : add_group (α →₀ β) :=
   .. finsupp.add_monoid }
 
 @[to_additive finsupp.sum_neg_index]
-lemma prod_neg_index {γ : Type w} [add_group β] [comm_monoid γ]
-  {g : α →₀ β} {h : α → β → γ} (h0 : ∀a, h a 0 = 1) :
-  (-g).prod h = g.prod (λa b, h a (- b)) :=
+lemma prod_neg_index [add_group β] [comm_monoid γ] {g : α →₀ β} {h : α → β → γ}
+  (h0 : ∀a, h a 0 = 1) : (-g).prod h = g.prod (λa b, h a (- b)) :=
 prod_map_range_index h0
 
-@[simp] lemma neg_apply [add_group β] {g : α →₀ β} {a : α} :
-  (- g) a = - g a :=
-rfl
+@[simp] lemma neg_apply [add_group β] {g : α →₀ β} {a : α} : (- g) a = - g a := rfl
 
-@[simp] lemma sub_apply [add_group β] {g₁ g₂ : α →₀ β} {a : α} :
-  (g₁ - g₂) a = g₁ a - g₂ a :=
-rfl
+@[simp] lemma sub_apply [add_group β] {g₁ g₂ : α →₀ β} {a : α} : (g₁ - g₂) a = g₁ a - g₂ a := rfl
 
 @[simp] lemma support_neg [add_group β] {f : α →₀ β} : support (-f) = support f :=
 finset.subset.antisymm
@@ -414,7 +410,7 @@ rfl
 
 section comap_domain
 
-variables {α' : Type u₁} {γ : Type x} {δ : Type y} [has_zero δ]
+variables {α' : Type u₁} {δ : Type y} [has_zero δ]
   {f : α → α'} {hf : injective f} {p : α → Prop}
 
 section zero
@@ -565,4 +561,23 @@ lemma prod_single {ι : Type x} [add_comm_monoid α] [comm_semiring β] {s : fin
   s.prod (λi, single (a i) (b i)) = single (s.sum a) (s.prod b) :=
  finset.induction_on s (by simp [one_def]) (by simp [single_mul_single] {contextual := tt})
 
+def to_has_scalar [semiring β] : has_scalar β (α →₀ β) := ⟨λa v, v.map_range ((*) a) (mul_zero a)⟩
+local attribute [instance] to_has_scalar
+
+@[simp] lemma smul_apply [semiring β] {a : α} {b : β} {v : α →₀ β} : (b • v) a = b * v a :=
+rfl
+
+/- should this be stronger? [module γ β] → module γ (α →₀ β) -/
+def to_module [ring β] : module β (α →₀ β) :=
+{ smul     := (•),
+  smul_add := assume a x y, finsupp.ext $ by simp [mul_add],
+  add_smul := assume a x y, finsupp.ext $ by simp [add_mul],
+  one_smul := assume x, finsupp.ext $ by simp,
+  mul_smul := assume r s x, finsupp.ext $ by simp [mul_assoc],
+  .. finsupp.add_comm_group }
+
+lemma sum_smul_index [ring β] [add_comm_monoid γ] {g : α →₀ β} {b : β} {h : α → β → γ}
+  (h0 : ∀i, h i 0 = 0) : (b • g).sum h = g.sum (λi a, h i (b * a)) :=
+finsupp.sum_map_range_index h0
+
 end finsupp