refactor(algebra/monoid_algebra/{ basic + support } + import dust): m…

…ove lemmas to a new "support" file (#16322)

This PR moves some lemmas from `algebra/monoid_algebra/basic` to the new file `algebra/monoid_algebra/support`.

[Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/splitting.20support.20from.20algebra.2Fmonoid_algebra.2Fbasic)

src/algebra/monoid_algebra/basic.lean

@@ -338,11 +338,6 @@ calc (f * g) x = (∑ a₁ in f.support, ∑ a₂ in g.support, F (a₁, a₂))
     { rw [hp hps h1, mul_zero] }
   end
 
-lemma support_mul [has_mul G] [decidable_eq G] (a b : monoid_algebra k G) :
-  (a * b).support ⊆ a.support.bUnion (λa₁, b.support.bUnion $ λa₂, {a₁ * a₂}) :=
-subset.trans support_sum $ bUnion_mono $ assume a₁ _,
-  subset.trans support_sum $ bUnion_mono $ assume a₂ _, support_single_subset
-
 @[simp] lemma single_mul_single [has_mul G] {a₁ a₂ : G} {b₁ b₂ : k} :
   (single a₁ b₁ : monoid_algebra k G) * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂) :=
 (sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
@@ -426,20 +421,6 @@ lemma mul_single_one_apply [mul_one_class G] (f : monoid_algebra k G) (r : k) (x
   (f * single 1 r) x = f x * r :=
 f.mul_single_apply_aux $ λ a, by rw [mul_one]
 
-lemma support_mul_single [right_cancel_semigroup G]
-  (f : monoid_algebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
-  (f * single x r).support = f.support.map (mul_right_embedding x) :=
-begin
-  ext y, simp only [mem_support_iff, mem_map, exists_prop, mul_right_embedding_apply],
-  by_cases H : ∃ a, a * x = y,
-  { rcases H with ⟨a, rfl⟩,
-    rw [mul_single_apply_aux f (λ _, mul_left_inj x)],
-    simp [hr] },
-  { push_neg at H,
-    classical,
-    simp [mul_apply, H] }
-end
-
 lemma single_mul_apply_aux [has_mul G] (f : monoid_algebra k G) {r : k} {x y z : G}
   (H : ∀ a, x * a = y ↔ a = z) :
   (single x r * f) y = r * f z :=
@@ -455,20 +436,6 @@ lemma single_one_mul_apply [mul_one_class G] (f : monoid_algebra k G) (r : k) (x
   (single 1 r * f) x = r * f x :=
 f.single_mul_apply_aux $ λ a, by rw [one_mul]
 
-lemma support_single_mul [left_cancel_semigroup G]
-  (f : monoid_algebra k G) (r : k) (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
-  (single x r * f).support = f.support.map (mul_left_embedding x) :=
-begin
-  ext y, simp only [mem_support_iff, mem_map, exists_prop, mul_left_embedding_apply],
-  by_cases H : ∃ a, x * a = y,
-  { rcases H with ⟨a, rfl⟩,
-    rw [single_mul_apply_aux f (λ _, mul_right_inj x)],
-    simp [hr] },
-  { push_neg at H,
-    classical,
-    simp [mul_apply, H] }
-end
-
 lemma lift_nc_smul [mul_one_class G] {R : Type*} [semiring R] (f : k →+* R) (g : G →* R) (c : k)
   (φ : monoid_algebra k G) :
   lift_nc (f : k →+ R) g (c • φ) = f c * lift_nc (f : k →+ R) g φ :=
@@ -841,17 +808,6 @@ calc (f * g) x = sum g (λ a b, (f * single a b) x) :
 
 end
 
-section span
-
-variables [semiring k] [mul_one_class G]
-
-/-- An element of `monoid_algebra R M` is in the subalgebra generated by its support. -/
-lemma mem_span_support (f : monoid_algebra k G) :
-  f ∈ submodule.span k (of k G '' (f.support : set G)) :=
-by rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported]
-
-end span
-
 section opposite
 
 open finsupp mul_opposite
@@ -1153,7 +1109,7 @@ finsupp.is_central_scalar G k
 because we've never discussed actions of additive groups. -/
 
 end derived_instances
-
+.
 section misc_theorems
 
 variables [semiring k]
@@ -1167,10 +1123,6 @@ lemma mul_apply_antidiagonal [has_add G] (f g : add_monoid_algebra k G) (x : G)
   (f * g) x = ∑ p in s, (f p.1 * g p.2) :=
 @monoid_algebra.mul_apply_antidiagonal k (multiplicative G) _ _ _ _ _ s @hs
 
-lemma support_mul [decidable_eq G] [has_add G] (a b : add_monoid_algebra k G) :
-  (a * b).support ⊆ a.support.bUnion (λa₁, b.support.bUnion $ λa₂, {a₁ + a₂}) :=
-@monoid_algebra.support_mul k (multiplicative G) _ _ _ _ _
-
 lemma single_mul_single [has_add G] {a₁ a₂ : G} {b₁ b₂ : k} :
   (single a₁ b₁ * single a₂ b₂ : add_monoid_algebra k G) = single (a₁ + a₂) (b₁ * b₂) :=
 @monoid_algebra.single_mul_single k (multiplicative G) _ _ _ _ _ _
@@ -1276,16 +1228,6 @@ lemma single_mul_apply [add_group G] (r : k) (x : G) (f : add_monoid_algebra k G
   (single x r * f : add_monoid_algebra k G) y = r * f (- x + y) :=
 @monoid_algebra.single_mul_apply k (multiplicative G) _ _ _ _ _ _
 
-lemma support_mul_single [add_right_cancel_semigroup G]
-  (f : add_monoid_algebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
-  (f * single x r : add_monoid_algebra k G).support = f.support.map (add_right_embedding x) :=
-@monoid_algebra.support_mul_single k (multiplicative G) _ _ _ _ hr _
-
-lemma support_single_mul [add_left_cancel_semigroup G]
-  (f : add_monoid_algebra k G) (r : k) (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
-  (single x r * f : add_monoid_algebra k G).support = f.support.map (add_left_embedding x) :=
-@monoid_algebra.support_single_mul k (multiplicative G) _ _ _ _ hr _
-
 lemma lift_nc_smul {R : Type*} [add_zero_class G] [semiring R] (f : k →+* R)
   (g : multiplicative G →* R) (c : k) (φ : monoid_algebra k G) :
   lift_nc (f : k →+ R) g (c • φ) = f c * lift_nc (f : k →+ R) g φ :=
@@ -1314,23 +1256,6 @@ def map_domain_ring_hom (k : Type*) [semiring k] {H F : Type*} [add_monoid G] [a
 
 end misc_theorems
 
-section span
-
-variables [semiring k]
-
-/-- An element of `add_monoid_algebra R M` is in the submodule generated by its support. -/
-lemma mem_span_support [add_zero_class G] (f : add_monoid_algebra k G) :
-  f ∈ submodule.span k (of k G '' (f.support : set G)) :=
-by rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported]
-
-/-- An element of `add_monoid_algebra R M` is in the subalgebra generated by its support, using
-unbundled inclusion. -/
-lemma mem_span_support' (f : add_monoid_algebra k G) :
-  f ∈ submodule.span k (of' k G '' (f.support : set G)) :=
-by rw [of', ← finsupp.supported_eq_span_single, finsupp.mem_supported]
-
-end span
-
 end add_monoid_algebra
 
 /-!

src/algebra/monoid_algebra/degree.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa
 -/
-import algebra.monoid_algebra.basic
+import algebra.monoid_algebra.support
 
 /-!
 # Lemmas about the `sup` and `inf` of the support of `add_monoid_algebra`

src/algebra/monoid_algebra/grading.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import linear_algebra.finsupp
-import algebra.monoid_algebra.basic
+import algebra.monoid_algebra.support
 import algebra.direct_sum.internal
 import ring_theory.graded_algebra.basic
 

src/algebra/monoid_algebra/support.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2022 Damiano Testa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Damiano Testa
+-/
+import algebra.monoid_algebra.basic
+
+/-!
+#  Lemmas about the support of a finitely supported function
+-/
+
+universes u₁ u₂ u₃
+namespace monoid_algebra
+
+open finset finsupp
+variables {k : Type u₁} {G : Type u₂} {R : Type u₃} [semiring k]
+
+lemma support_mul [has_mul G] [decidable_eq G] (a b : monoid_algebra k G) :
+  (a * b).support ⊆ a.support.bUnion (λa₁, b.support.bUnion $ λa₂, {a₁ * a₂}) :=
+subset.trans support_sum $ bUnion_mono $ assume a₁ _,
+  subset.trans support_sum $ bUnion_mono $ assume a₂ _, support_single_subset
+
+lemma support_mul_single [right_cancel_semigroup G]
+  (f : monoid_algebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
+  (f * single x r).support = f.support.map (mul_right_embedding x) :=
+begin
+  ext y, simp only [mem_support_iff, mem_map, exists_prop, mul_right_embedding_apply],
+  by_cases H : ∃ a, a * x = y,
+  { rcases H with ⟨a, rfl⟩,
+    rw [mul_single_apply_aux f (λ _, mul_left_inj x)],
+    simp [hr] },
+  { push_neg at H,
+    classical,
+    simp [mul_apply, H] }
+end
+
+lemma support_single_mul [left_cancel_semigroup G]
+  (f : monoid_algebra k G) (r : k) (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
+  (single x r * f : monoid_algebra k G).support = f.support.map (mul_left_embedding x) :=
+begin
+  ext y, simp only [mem_support_iff, mem_map, exists_prop, mul_left_embedding_apply],
+  by_cases H : ∃ a, x * a = y,
+  { rcases H with ⟨a, rfl⟩,
+    rw [single_mul_apply_aux f (λ _, mul_right_inj x)],
+    simp [hr] },
+  { push_neg at H,
+    classical,
+    simp [mul_apply, H] }
+end
+section span
+
+variables [mul_one_class G]
+
+/-- An element of `monoid_algebra R M` is in the subalgebra generated by its support. -/
+lemma mem_span_support (f : monoid_algebra k G) :
+  f ∈ submodule.span k (of k G '' (f.support : set G)) :=
+by rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported]
+
+end span
+
+
+end monoid_algebra
+
+namespace add_monoid_algebra
+
+open finset finsupp mul_opposite
+variables {k : Type u₁} {G : Type u₂} {R : Type u₃} [semiring k]
+
+lemma support_mul [decidable_eq G] [has_add G] (a b : add_monoid_algebra k G) :
+  (a * b).support ⊆ a.support.bUnion (λa₁, b.support.bUnion $ λa₂, {a₁ + a₂}) :=
+@monoid_algebra.support_mul k (multiplicative G) _ _ _ _ _
+
+lemma support_mul_single [add_right_cancel_semigroup G]
+  (f : add_monoid_algebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
+  (f * single x r : add_monoid_algebra k G).support = f.support.map (add_right_embedding x) :=
+@monoid_algebra.support_mul_single k (multiplicative G) _ _ _ _ hr _
+
+lemma support_single_mul [add_left_cancel_semigroup G]
+  (f : add_monoid_algebra k G) (r : k) (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
+  (single x r * f : add_monoid_algebra k G).support = f.support.map (add_left_embedding x) :=
+@monoid_algebra.support_single_mul k (multiplicative G) _ _ _ _ hr _
+
+section span
+
+/-- An element of `add_monoid_algebra R M` is in the submodule generated by its support. -/
+lemma mem_span_support [add_zero_class G] (f : add_monoid_algebra k G) :
+  f ∈ submodule.span k (of k G '' (f.support : set G)) :=
+by rw [of, monoid_hom.coe_mk, ← finsupp.supported_eq_span_single, finsupp.mem_supported]
+
+/-- An element of `add_monoid_algebra R M` is in the subalgebra generated by its support, using
+unbundled inclusion. -/
+lemma mem_span_support' (f : add_monoid_algebra k G) :
+  f ∈ submodule.span k (of' k G '' (f.support : set G)) :=
+by rw [of', ← finsupp.supported_eq_span_single, finsupp.mem_supported]
+
+end span
+
+end add_monoid_algebra

src/data/mv_polynomial/basic.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl, Johan Commelin, Mario Carneiro
 
 import ring_theory.adjoin.basic
 import data.finsupp.antidiagonal
-import algebra.monoid_algebra.basic
+import algebra.monoid_algebra.support
 import order.symm_diff
 
 /-!