chore: move algebraic properties of Finsupp.single to Algebra.Group.Finsupp (#28073)

They do not belong under `Data` as they are not about a datatype.

Author: YaelDillies

Mathlib/Algebra/Group/Finsupp.lean

@@ -4,22 +4,31 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kim Morrison
 -/
 import Mathlib.Algebra.Group.Equiv.Defs
-import Mathlib.Algebra.Group.InjSurj
-import Mathlib.Algebra.Group.Pi.Basic
-import Mathlib.Data.Finsupp.Defs
+import Mathlib.Data.Finset.Max
+import Mathlib.Data.Finsupp.Single
 import Mathlib.Tactic.FastInstance
 
 /-!
 # Additive monoid structure on `ι →₀ M`
 -/
 
+assert_not_exists MonoidWithZero
+
 open Finset
 
 noncomputable section
 
-variable {ι F M N G H : Type*}
+variable {ι F M N O G H : Type*}
 
 namespace Finsupp
+section Zero
+variable [Zero M] [Zero N]
+
+lemma apply_single [FunLike F M N] [ZeroHomClass F M N] (e : F) (i : ι) (m : M) (b : ι) :
+    e (single i m b) = single i (e m) b := apply_single' e (map_zero e) i m b
+
+end Zero
+
 section AddZeroClass
 variable [AddZeroClass M] [AddZeroClass N] {f : M → N} {g₁ g₂ : ι →₀ M}
 
@@ -105,6 +114,171 @@ def embDomain.addMonoidHom (f : ι ↪ F) : (ι →₀ M) →+ F →₀ M where
 lemma embDomain_add (f : ι ↪ F) (v w : ι →₀ M) :
     embDomain f (v + w) = embDomain f v + embDomain f w := (embDomain.addMonoidHom f).map_add v w
 
+@[simp]
+lemma single_add (a : ι) (b₁ b₂ : M) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
+  (zipWith_single_single _ _ _ _ _).symm
+
+lemma single_add_apply (a : ι) (m₁ m₂ : M) (b : ι) :
+    single a (m₁ + m₂) b = single a m₁ b + single a m₂ b := by simp
+
+lemma support_single_add {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
+    support (single a b + f) = cons a f.support ha := by
+  classical
+  have H := support_single_ne_zero a hb
+  rw [support_add_eq, H, cons_eq_insert, insert_eq]
+  rwa [H, disjoint_singleton_left]
+
+lemma support_add_single {a : ι} {b : M} {f : ι →₀ M} (ha : a ∉ f.support) (hb : b ≠ 0) :
+    support (f + single a b) = cons a f.support ha := by
+  classical
+  have H := support_single_ne_zero a hb
+  rw [support_add_eq, H, union_comm, cons_eq_insert, insert_eq]
+  rwa [H, disjoint_singleton_right]
+
+lemma _root_.AddEquiv.finsuppUnique_symm {M : Type*} [AddZeroClass M] (d : M) :
+    AddEquiv.finsuppUnique.symm d = single () d := by
+  rw [Finsupp.unique_single (AddEquiv.finsuppUnique.symm d), Finsupp.unique_single_eq_iff]
+  simp [AddEquiv.finsuppUnique]
+
+/-- `Finsupp.single` as an `AddMonoidHom`.
+
+See `Finsupp.lsingle` in `Mathlib/LinearAlgebra/Finsupp/Defs.lean` for the stronger version as a
+linear map. -/
+@[simps]
+def singleAddHom (a : ι) : M →+ ι →₀ M where
+  toFun := single a
+  map_zero' := single_zero a
+  map_add' := single_add a
+
+lemma update_eq_single_add_erase (f : ι →₀ M) (a : ι) (b : M) :
+    f.update a b = single a b + f.erase a := by
+  classical
+    ext j
+    rcases eq_or_ne a j with (rfl | h)
+    · simp
+    · simp [h, erase_ne, h.symm]
+
+lemma update_eq_erase_add_single (f : ι →₀ M) (a : ι) (b : M) :
+    f.update a b = f.erase a + single a b := by
+  classical
+    ext j
+    rcases eq_or_ne a j with (rfl | h)
+    · simp
+    · simp [h, erase_ne, h.symm]
+
+lemma single_add_erase (a : ι) (f : ι →₀ M) : single a (f a) + f.erase a = f := by
+  rw [← update_eq_single_add_erase, update_self]
+
+lemma erase_add_single (a : ι) (f : ι →₀ M) : f.erase a + single a (f a) = f := by
+  rw [← update_eq_erase_add_single, update_self]
+
+@[simp]
+lemma erase_add (a : ι) (f f' : ι →₀ M) : erase a (f + f') = erase a f + erase a f' := by
+  ext s; by_cases hs : s = a
+  · rw [hs, add_apply, erase_same, erase_same, erase_same, add_zero]
+  rw [add_apply, erase_ne hs, erase_ne hs, erase_ne hs, add_apply]
+
+/-- `Finsupp.erase` as an `AddMonoidHom`. -/
+@[simps]
+def eraseAddHom (a : ι) : (ι →₀ M) →+ ι →₀ M where
+  toFun := erase a
+  map_zero' := erase_zero a
+  map_add' := erase_add a
+
+@[elab_as_elim]
+protected lemma induction {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0)
+    (single_add : ∀ (a b) (f : ι →₀ M),
+      a ∉ f.support → b ≠ 0 → motive f → motive (single a b + f)) : motive f :=
+  suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl
+  fun s =>
+  Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf => by
+    suffices motive (single a (f a) + f.erase a) by rwa [single_add_erase] at this
+    classical
+      apply single_add
+      · rw [support_erase, mem_erase]
+        exact fun H => H.1 rfl
+      · rw [← mem_support_iff, hf]
+        exact mem_cons_self _ _
+      · apply ih _ _
+        rw [support_erase, hf, Finset.erase_cons]
+
+@[elab_as_elim]
+lemma induction₂ {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0)
+    (add_single : ∀ (a b) (f : ι →₀ M),
+      a ∉ f.support → b ≠ 0 → motive f → motive (f + single a b)) : motive f :=
+  suffices ∀ (s) (f : ι →₀ M), f.support = s → motive f from this _ _ rfl
+  fun s =>
+  Finset.cons_induction_on s (fun f hf => by rwa [support_eq_empty.1 hf]) fun a s has ih f hf => by
+    suffices motive (f.erase a + single a (f a)) by rwa [erase_add_single] at this
+    classical
+      apply add_single
+      · rw [support_erase, mem_erase]
+        exact fun H => H.1 rfl
+      · rw [← mem_support_iff, hf]
+        exact mem_cons_self _ _
+      · apply ih _ _
+        rw [support_erase, hf, Finset.erase_cons]
+
+@[elab_as_elim]
+lemma induction_linear {motive : (ι →₀ M) → Prop} (f : ι →₀ M) (zero : motive 0)
+    (add : ∀ f g : ι →₀ M, motive f → motive g → motive (f + g))
+    (single : ∀ a b, motive (single a b)) : motive f :=
+  induction₂ f zero fun _a _b _f _ _ w => add _ _ w (single _ _)
+
+section LinearOrder
+
+variable [LinearOrder ι] {p : (ι →₀ M) → Prop}
+
+/-- A finitely supported function can be built by adding up `single a b` for increasing `a`.
+
+The lemma `induction_on_max₂` swaps the argument order in the sum. -/
+lemma induction_on_max (f : ι →₀ M) (h0 : p 0)
+    (ha : ∀ (a b) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (single a b + f)) :
+    p f := by
+  suffices ∀ (s) (f : ι →₀ M), f.support = s → p f from this _ _ rfl
+  refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
+  · rwa [support_eq_empty.1 h]
+  · have hs' : (erase a f).support = s := by
+      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
+    rw [← single_add_erase a f]
+    refine ha _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
+    rw [← mem_support_iff, hs]
+    exact mem_insert_self a s
+
+/-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.
+
+The lemma `induction_on_min₂` swaps the argument order in the sum. -/
+lemma induction_on_min (f : ι →₀ M) (h0 : p 0)
+    (ha : ∀ (a b) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (single a b + f)) :
+    p f :=
+  induction_on_max (ι := ιᵒᵈ) f h0 ha
+
+/-- A finitely supported function can be built by adding up `single a b` for increasing `a`.
+
+The lemma `induction_on_max` swaps the argument order in the sum. -/
+lemma induction_on_max₂ (f : ι →₀ M) (h0 : p 0)
+    (ha : ∀ (a b) (f : ι →₀ M), (∀ c ∈ f.support, c < a) → b ≠ 0 → p f → p (f + single a b)) :
+    p f := by
+  suffices ∀ (s) (f : ι →₀ M), f.support = s → p f from this _ _ rfl
+  refine fun s => s.induction_on_max (fun f h => ?_) (fun a s hm hf f hs => ?_)
+  · rwa [support_eq_empty.1 h]
+  · have hs' : (erase a f).support = s := by
+      rw [support_erase, hs, erase_insert (fun ha => (hm a ha).false)]
+    rw [← erase_add_single a f]
+    refine ha _ _ _ (fun c hc => hm _ <| hs'.symm ▸ hc) ?_ (hf _ hs')
+    rw [← mem_support_iff, hs]
+    exact mem_insert_self a s
+
+/-- A finitely supported function can be built by adding up `single a b` for decreasing `a`.
+
+The lemma `induction_on_min` swaps the argument order in the sum. -/
+lemma induction_on_min₂ (f : ι →₀ M) (h0 : p 0)
+    (ha : ∀ (a b) (f : ι →₀ M), (∀ c ∈ f.support, a < c) → b ≠ 0 → p f → p (f + single a b)) :
+    p f :=
+  induction_on_max₂ (ι := ιᵒᵈ) f h0 ha
+
+end LinearOrder
+
 end AddZeroClass
 
 section AddMonoid
@@ -119,10 +293,22 @@ instance instAddMonoid : AddMonoid (ι →₀ M) :=
 
 end AddMonoid
 
-instance instAddCommMonoid [AddCommMonoid M] : AddCommMonoid (ι →₀ M) :=
+section AddCommMonoid
+variable [AddCommMonoid M]
+
+instance instAddCommMonoid : AddCommMonoid (ι →₀ M) :=
   fast_instance% DFunLike.coe_injective.addCommMonoid
     DFunLike.coe coe_zero coe_add (fun _ _ => rfl)
 
+lemma single_add_single_eq_single_add_single {k l m n : ι} {u v : M} (hu : u ≠ 0) (hv : v ≠ 0) :
+    single k u + single l v = single m u + single n v ↔
+      (k = m ∧ l = n) ∨ (u = v ∧ k = n ∧ l = m) ∨ (u + v = 0 ∧ k = l ∧ m = n) := by
+  classical
+    simp_rw [DFunLike.ext_iff, coe_add, single_eq_pi_single, ← funext_iff]
+    exact Pi.single_add_single_eq_single_add_single hu hv
+
+end AddCommMonoid
+
 instance instNeg [NegZeroClass G] : Neg (ι →₀ G) where neg := mapRange Neg.neg neg_zero
 
 @[simp, norm_cast] lemma coe_neg [NegZeroClass G] (g : ι →₀ G) : ⇑(-g) = -g := rfl
@@ -134,11 +320,6 @@ lemma mapRange_neg [NegZeroClass G] [NegZeroClass H] {f : G → H} {hf : f 0 = 0
     (hf' : ∀ x, f (-x) = -f x) (v : ι →₀ G) : mapRange f hf (-v) = -mapRange f hf v :=
   ext fun _ => by simp only [hf', neg_apply, mapRange_apply]
 
-lemma mapRange_neg' [AddGroup G] [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H]
-    {f : F} (v : ι →₀ G) :
-    mapRange f (map_zero f) (-v) = -mapRange f (map_zero f) v :=
-  mapRange_neg (map_neg f) v
-
 instance instSub [SubNegZeroMonoid G] : Sub (ι →₀ G) :=
   ⟨zipWith Sub.sub (sub_zero _)⟩
 
@@ -151,35 +332,70 @@ lemma mapRange_sub [SubNegZeroMonoid G] [SubNegZeroMonoid H] {f : G → H} {hf :
     mapRange f hf (v₁ - v₂) = mapRange f hf v₁ - mapRange f hf v₂ :=
   ext fun _ => by simp only [hf', sub_apply, mapRange_apply]
 
-lemma mapRange_sub' [AddGroup G] [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H]
+section AddGroup
+variable [AddGroup G] {p : ι → Prop} {v v' : ι →₀ G}
+
+lemma mapRange_neg' [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H]
+    {f : F} (v : ι →₀ G) :
+    mapRange f (map_zero f) (-v) = -mapRange f (map_zero f) v :=
+  mapRange_neg (map_neg f) v
+
+lemma mapRange_sub' [SubtractionMonoid H] [FunLike F G H] [AddMonoidHomClass F G H]
     {f : F} (v₁ v₂ : ι →₀ G) :
     mapRange f (map_zero f) (v₁ - v₂) = mapRange f (map_zero f) v₁ - mapRange f (map_zero f) v₂ :=
   mapRange_sub (map_sub f) v₁ v₂
 
 /-- Note the general `SMul` instance for `Finsupp` doesn't apply as `ℤ` is not distributive
 unless `F i`'s addition is commutative. -/
-instance instIntSMul [AddGroup G] : SMul ℤ (ι →₀ G) :=
+instance instIntSMul : SMul ℤ (ι →₀ G) :=
   ⟨fun n v => v.mapRange (n • ·) (zsmul_zero _)⟩
 
-instance instAddGroup [AddGroup G] : AddGroup (ι →₀ G) :=
+instance instAddGroup : AddGroup (ι →₀ G) :=
   fast_instance% DFunLike.coe_injective.addGroup DFunLike.coe coe_zero coe_add coe_neg coe_sub
     (fun _ _ => rfl) fun _ _ => rfl
 
-instance instAddCommGroup [AddCommGroup G] : AddCommGroup (ι →₀ G) :=
-  fast_instance%  DFunLike.coe_injective.addCommGroup DFunLike.coe coe_zero coe_add coe_neg coe_sub
-    (fun _ _ => rfl) fun _ _ => rfl
-
 @[simp]
-lemma support_neg [AddGroup G] (f : ι →₀ G) : support (-f) = support f :=
+lemma support_neg (f : ι →₀ G) : support (-f) = support f :=
   Finset.Subset.antisymm support_mapRange
     (calc
       support f = support (- -f) := congr_arg support (neg_neg _).symm
       _ ⊆ support (-f) := support_mapRange
       )
 
-lemma support_sub [DecidableEq ι] [AddGroup G] {f g : ι →₀ G} :
-    support (f - g) ⊆ support f ∪ support g := by
+lemma support_sub [DecidableEq ι] {f g : ι →₀ G} : support (f - g) ⊆ support f ∪ support g := by
   rw [sub_eq_add_neg, ← support_neg g]
   exact support_add
 
+lemma erase_eq_sub_single (f : ι →₀ G) (a : ι) : f.erase a = f - single a (f a) := by
+  ext a'
+  rcases eq_or_ne a a' with (rfl | h)
+  · simp
+  · simp [erase_ne h.symm, single_eq_of_ne h]
+
+lemma update_eq_sub_add_single (f : ι →₀ G) (a : ι) (b : G) :
+    f.update a b = f - single a (f a) + single a b := by
+  rw [update_eq_erase_add_single, erase_eq_sub_single]
+
+@[simp]
+lemma single_neg (a : ι) (b : G) : single a (-b) = -single a b :=
+  (singleAddHom a : G →+ _).map_neg b
+
+@[simp]
+lemma single_sub (a : ι) (b₁ b₂ : G) : single a (b₁ - b₂) = single a b₁ - single a b₂ :=
+  (singleAddHom a : G →+ _).map_sub b₁ b₂
+
+@[simp]
+lemma erase_neg (a : ι) (f : ι →₀ G) : erase a (-f) = -erase a f :=
+  (eraseAddHom a : (_ →₀ G) →+ _).map_neg f
+
+@[simp]
+lemma erase_sub (a : ι) (f₁ f₂ : ι →₀ G) : erase a (f₁ - f₂) = erase a f₁ - erase a f₂ :=
+  (eraseAddHom a : (_ →₀ G) →+ _).map_sub f₁ f₂
+
+end AddGroup
+
+instance instAddCommGroup [AddCommGroup G] : AddCommGroup (ι →₀ G) :=
+  fast_instance%  DFunLike.coe_injective.addCommGroup DFunLike.coe coe_zero coe_add coe_neg coe_sub
+    (fun _ _ => rfl) fun _ _ => rfl
+
 end Finsupp

Mathlib/Data/Finsupp/Ext.lean

@@ -3,9 +3,9 @@ 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, Kim Morrison
 -/
+import Mathlib.Algebra.Group.Finsupp
 import Mathlib.Algebra.Group.Submonoid.Basic
 import Mathlib.Algebra.Group.TypeTags.Hom
-import Mathlib.Data.Finsupp.Single
 
 /-!
 # Extensionality for maps on `Finsupp`

Mathlib/Data/Finsupp/Pointwise.lean

@@ -3,10 +3,10 @@ Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison
 -/
+import Mathlib.Algebra.Group.Finsupp
 import Mathlib.Algebra.Module.Defs
 import Mathlib.Algebra.Ring.InjSurj
 import Mathlib.Algebra.Ring.Pi
-import Mathlib.Data.Finsupp.Single
 
 /-!
 # The pointwise product on `Finsupp`.

Mathlib/Data/Finsupp/SMulWithZero.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kim Morrison
 -/
 import Mathlib.Algebra.Group.Action.Pi
+import Mathlib.Algebra.Group.Finsupp
 import Mathlib.Algebra.GroupWithZero.Action.Defs
-import Mathlib.Data.Finsupp.Single
 
 /-!
 # Scalar multiplication on `Finsupp`