feat(data/finsupp): lift a collection of add_monoid_homs to an `add…

…_monoid_hom` on `α →₀ β` (#4395)

src/algebra/module/basic.lean

@@ -267,7 +267,6 @@ instance : has_coe_to_fun (M →ₗ[R] M₂) := ⟨_, to_fun⟩
 @[simp] lemma coe_mk (f : M → M₂) (h₁ h₂) :
   ((linear_map.mk f h₁ h₂ : M →ₗ[R] M₂) : M → M₂) = f := rfl
 
-
 /-- Identity map as a `linear_map` -/
 def id : M →ₗ[R] M :=
 ⟨id, λ _ _, rfl, λ _ _, rfl⟩
@@ -334,6 +333,10 @@ def to_add_monoid_hom : M →+ M₂ :=
   f (∑ i in t, g i) = (∑ i in t, f (g i)) :=
 f.to_add_monoid_hom.map_sum _ _
 
+theorem to_add_monoid_hom_injective [semimodule R M] [semimodule R M₂] :
+  function.injective (to_add_monoid_hom : (M →ₗ[R] M₂) → (M →+ M₂)) :=
+λ f g h, coe_inj $ funext $ add_monoid_hom.congr_fun h
+
 end
 
 section

src/data/finsupp/basic.lean

@@ -3,6 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Scott Morrison
 -/
+import algebra.group.pi
 import algebra.big_operators.order
 import algebra.module.basic
 import data.fintype.card
@@ -451,19 +452,25 @@ def sum [has_zero β] [add_comm_monoid γ] (f : α →₀ β) (g : α → β →
 def prod [has_zero β] [comm_monoid γ] (f : α →₀ β) (g : α → β → γ) : γ :=
 ∏ a in f.support, g a (f a)
 
+@[to_additive]
+lemma prod_of_support_subset [has_zero β] [comm_monoid γ] (f : α →₀ β) {s : finset α}
+  (hs : f.support ⊆ s) (g : α → β → γ) (h : ∀ i ∈ s, g i 0 = 1) :
+  f.prod g = ∏ x in s, g x (f x) :=
+finset.prod_subset hs $ λ x hxs hx, h x hxs ▸ congr_arg (g x) $ not_mem_support_iff.1 hx
+
 @[to_additive]
 lemma prod_fintype [fintype α] [has_zero β] [comm_monoid γ]
   (f : α →₀ β) (g : α → β → γ) (h : ∀ i, g i 0 = 1) :
   f.prod g = ∏ i, g i (f i) :=
-begin
-  classical,
-  rw [finsupp.prod, ← fintype.prod_extend_by_one, finset.prod_congr rfl],
-  intros i hi,
-  split_ifs with hif hif,
-  { refl },
-  { rw finsupp.not_mem_support_iff at hif,
-    rw [hif, h] }
-end
+f.prod_of_support_subset (subset_univ _) g (λ x _, h x)
+
+@[simp, to_additive]
+lemma prod_single_index [has_zero β] [comm_monoid γ] {a : α} {b : β} {h : α → β → γ}
+  (h_zero : h a 0 = 1) :
+  (single a b).prod h = h a b :=
+calc (single a b).prod h = ∏ x in {a}, h x (single a b x) :
+  prod_of_support_subset _ support_single_subset h $ λ x hx, (mem_singleton.1 hx).symm ▸ h_zero
+... = h a b : by simp
 
 @[to_additive]
 lemma prod_map_range_index [has_zero β₁] [has_zero β₂] [comm_monoid γ]
@@ -521,15 +528,6 @@ end
 section add_monoid
 variables [add_monoid β]
 
-@[to_additive]
-lemma prod_single_index [comm_monoid γ] {a : α} {b : β} {h : α → β → γ} (h_zero : h a 0 = 1) :
-  (single a b).prod h = h a b :=
-begin
-  by_cases h : b = 0,
-  { simp only [h, h_zero, single_zero]; refl },
-  { simp only [finsupp.prod, support_single_ne_zero h, prod_singleton, single_eq_same] }
-end
-
 instance : has_add (α →₀ β) := ⟨zip_with (+) (add_zero 0)⟩
 
 @[simp] lemma add_apply {g₁ g₂ : α →₀ β} {a : α} : (g₁ + g₂) a = g₁ a + g₂ a :=
@@ -565,6 +563,10 @@ instance : add_monoid (α →₀ β) :=
   zero_add  := assume ⟨s, f, hf⟩, ext $ assume a, zero_add _,
   add_zero  := assume ⟨s, f, hf⟩, ext $ assume a, add_zero _ }
 
+/-- `finsupp.single` as an `add_monoid_hom`. -/
+@[simps] def single_add_hom (a : α) : β →+ α →₀ β :=
+⟨single a, single_zero, λ _ _, single_add⟩
+
 /-- Evaluation of a function `f : α →₀ β` at a point as an additive monoid homomorphism. -/
 def eval_add_hom (a : α) : (α →₀ β) →+ β := ⟨λ g, g a, zero_apply, λ _ _, add_apply⟩
 
@@ -618,6 +620,22 @@ begin
     rw [support_erase, hf, finset.erase_insert has] }
 end
 
+@[simp] lemma add_closure_Union_range_single :
+  add_submonoid.closure (⋃ a : α, set.range (single a : β → α →₀ β)) = ⊤ :=
+top_unique $ λ x hx, finsupp.induction x (add_submonoid.zero_mem _) $
+  λ a b f ha hb hf, add_submonoid.add_mem _
+    (add_submonoid.subset_closure $ set.mem_Union.2 ⟨a, set.mem_range_self _⟩) hf
+
+@[ext] lemma add_hom_ext [add_monoid γ] ⦃f g : (α →₀ β) →+ γ⦄
+  (H : ∀ x y, f (single x y) = g (single x y)) :
+  f = g :=
+begin
+  refine add_monoid_hom.eq_of_eq_on_mdense add_closure_Union_range_single (λ f hf, _),
+  simp only [set.mem_Union, set.mem_range] at hf,
+  rcases hf with ⟨x, y, rfl⟩,
+  apply H
+end
+
 lemma map_range_add [add_monoid β₁] [add_monoid β₂]
   {f : β₁ → β₂} {hf : f 0 = 0} (hf' : ∀ x y, f (x + y) = f x + f y) (v₁ v₂ : α →₀ β₁) :
   map_range f hf (v₁ + v₂) = map_range f hf v₁ + map_range f hf v₂ :=
@@ -749,62 +767,52 @@ f.support.sum_hom (@has_neg.neg γ _)
   f.sum (λa b, h₁ a b - h₂ a b) = f.sum h₁ - f.sum h₂ :=
 by rw [sub_eq_add_neg, ←sum_neg, ←sum_add]; refl
 
-@[simp] lemma sum_single [add_comm_monoid β] (f : α →₀ β) :
-  f.sum single = f :=
-have ∀a:α, f.sum (λa' b, ite (a' = a) b 0) =
-    ∑ a' in {a}, ite (a' = a) (f a') 0,
-begin
-  intro a,
-  by_cases h : a ∈ f.support,
-  { have : ({a} : finset α) ⊆ f.support,
-      { simpa only [finset.subset_iff, mem_singleton, forall_eq] },
-    refine (finset.sum_subset this (λ _ _ H, _)).symm,
-    exact if_neg (mt mem_singleton.2 H) },
-  { transitivity (∑ a in f.support, (0 : β)),
-    { refine (finset.sum_congr rfl $ λ a' ha', if_neg _),
-      rintro rfl, exact h ha' },
-    { rw [sum_const_zero, sum_singleton, if_pos rfl, not_mem_support_iff.1 h] } }
-end,
-ext $ assume a, by simp only [sum_apply, single_apply, this, sum_singleton, if_pos]
-
 @[to_additive]
 lemma prod_add_index [add_comm_monoid β] [comm_monoid γ] {f g : α →₀ β}
   {h : α → β → γ} (h_zero : ∀a, h a 0 = 1) (h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
   (f + g).prod h = f.prod h * g.prod h :=
-have f_eq : ∏ a in f.support ∪ g.support, h a (f a) = f.prod h,
-  from (finset.prod_subset (finset.subset_union_left _ _) $
-    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
-have g_eq : ∏ a in f.support ∪ g.support, h a (g a) = g.prod h,
-  from (finset.prod_subset (finset.subset_union_right _ _) $
-    by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]).symm,
-calc ∏ a in (f + g).support, h a ((f + g) a) =
-      ∏ a in f.support ∪ g.support, h a ((f + g) a) :
-    finset.prod_subset support_add $
-      by intros _ _ H; rw [not_mem_support_iff.1 H, h_zero]
-  ... = (∏ a in f.support ∪ g.support, h a (f a)) *
-      (∏ a in f.support ∪ g.support, h a (g a)) :
-    by simp only [add_apply, h_add, finset.prod_mul_distrib]
-  ... = _ : by rw [f_eq, g_eq]
+have hf : f.prod h = ∏ a in f.support ∪ g.support, h a (f a),
+  from f.prod_of_support_subset (subset_union_left _ _) _ $ λ a ha, h_zero a,
+have hg : g.prod h = ∏ a in f.support ∪ g.support, h a (g a),
+  from g.prod_of_support_subset (subset_union_right _ _) _ $ λ a ha, h_zero a,
+have hfg : (f + g).prod h = ∏ a in f.support ∪ g.support, h a ((f + g) a),
+  from (f + g).prod_of_support_subset support_add _ $ λ a ha, h_zero a,
+by simp only [*, add_apply, prod_mul_distrib]
+
+/-- The canonical isomorphism between families of additive monoid homomorphisms `α → (β →+ γ)`
+and monoid homomorphisms `(α →₀ β) →+ γ`. -/
+def lift_add_hom [add_comm_monoid β] [add_comm_monoid γ] : (α → β →+ γ) ≃+ ((α →₀ β) →+ γ) :=
+{ to_fun := λ F,
+  { to_fun := λ f, f.sum (λ x, F x),
+    map_zero' := finset.sum_empty,
+    map_add' := λ _ _, sum_add_index (λ x, (F x).map_zero) (λ x, (F x).map_add) },
+  inv_fun := λ F x, F.comp $ single_add_hom x,
+  left_inv := λ F, by { ext, simp },
+  right_inv := λ F, by { ext, simp },
+  map_add' := λ F G, by { ext, simp } }
+
+@[simp] lemma lift_add_hom_apply [add_comm_monoid β] [add_comm_monoid γ]
+  (F : α → β →+ γ) (f : α →₀ β) :
+  lift_add_hom F f = f.sum (λ x, F x) :=
+rfl
+
+@[simp] lemma lift_add_hom_symm_apply [add_comm_monoid β] [add_comm_monoid γ]
+  (F : (α →₀ β) →+ γ) (x : α) :
+  lift_add_hom.symm F x = F.comp (single_add_hom x) :=
+rfl
+
+@[simp] lemma lift_add_hom_single_add_hom [add_comm_monoid β] :
+  lift_add_hom (single_add_hom : α → β →+ α →₀ β) = add_monoid_hom.id _ :=
+lift_add_hom.to_equiv.apply_eq_iff_eq_symm_apply.2 rfl
+
+@[simp] lemma sum_single [add_comm_monoid β] (f : α →₀ β) :
+  f.sum single = f :=
+add_monoid_hom.congr_fun lift_add_hom_single_add_hom f
 
 lemma sum_sub_index [add_comm_group β] [add_comm_group γ] {f g : α →₀ β}
   {h : α → β → γ} (h_sub : ∀a b₁ b₂, h a (b₁ - b₂) = h a b₁ - h a b₂) :
   (f - g).sum h = f.sum h - g.sum h :=
-have h_zero : ∀a, h a 0 = 0,
-  from assume a,
-  have h a (0 - 0) = h a 0 - h a 0, from h_sub a 0 0,
-  by simpa only [sub_self] using this,
-have h_neg : ∀a b, h a (- b) = - h a b,
-  from assume a b,
-  have h a (0 - b) = h a 0 - h a b, from h_sub a 0 b,
-  by simpa only [h_zero, zero_sub] using this,
-have h_add : ∀a b₁ b₂, h a (b₁ + b₂) = h a b₁ + h a b₂,
-  from assume a b₁ b₂,
-  have h a (b₁ - (- b₂)) = h a b₁ - h a (- b₂), from h_sub a b₁ (-b₂),
-  by simpa only [h_neg, sub_neg_eq_add] using this,
-calc (f - g).sum h = (f + - g).sum h : rfl
-  ... = f.sum h + - g.sum h : by simp only [sum_add_index h_zero h_add, sum_neg_index h_zero,
-                                   h_neg, sum_neg]
-  ... = f.sum h - g.sum h : rfl
+(lift_add_hom (λ a, add_monoid_hom.of_map_sub (h a) (h_sub a))).map_sub f g
 
 @[to_additive]
 lemma prod_finset_sum_index [add_comm_monoid β] [comm_monoid γ]
@@ -1524,11 +1532,10 @@ lemma smul_single_one [semiring β] (a : α) (b : β) : b • single a 1 = singl
 by rw [smul_single, smul_eq_mul, mul_one]
 
 /-- Two `R`-linear maps from `finsupp X R` which agree on `single x 1` agree everywhere. -/
-lemma hom_ext [semiring β] [add_comm_monoid γ] [semimodule β γ] (φ ψ : (α →₀ β) →ₗ[β] γ)
+@[ext] lemma hom_ext [semiring β] [add_comm_monoid γ] [semimodule β γ] ⦃φ ψ : (α →₀ β) →ₗ[β] γ⦄
   (h : ∀ a : α, φ (single a 1) = ψ (single a 1)) : φ = ψ :=
-linear_map.ext $ λ x, finsupp.induction x (by rw [φ.map_zero, ψ.map_zero]) $
-  λ _ _ _ _ _ hgh,
-  by rw [φ.map_add, ψ.map_add, hgh, ←smul_single_one, φ.map_smul, ψ.map_smul, h]
+linear_map.to_add_monoid_hom_injective $ add_hom_ext $ λ x y,
+  by simp only [← smul_single_one x y, linear_map.to_add_monoid_hom_coe, linear_map.map_smul, h]
 
 end