feat(algebra/monoid_algebra/support): lemmas about support and multip…

…lying with single (#16326)

The new lemmas use weaker assumptions and can be used to shorten some proofs.

src/algebra/monoid_algebra/support.lean

@@ -13,7 +13,55 @@ universes u₁ u₂ u₃
 namespace monoid_algebra
 
 open finset finsupp
-variables {k : Type u₁} {G : Type u₂} {R : Type u₃} [semiring k]
+variables {k : Type u₁} {G : Type u₂} [semiring k]
+
+lemma support_single_mul_subset [decidable_eq G] [has_mul G]
+  (f : monoid_algebra k G) (r : k) (a : G) :
+  (single a r * f : monoid_algebra k G).support ⊆ finset.image ((*) a) f.support :=
+begin
+  intros x hx,
+  contrapose hx,
+  have : ∀ y, a * y = x → f y = 0,
+  { simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, not_not] using hx },
+  simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, if_t_t, sum_zero, not_not],
+  exact finset.sum_eq_zero (by simp only [this, mem_support_iff, mul_zero, ne.def,
+    ite_eq_right_iff, eq_self_iff_true, implies_true_iff] {contextual := tt}),
+end
+
+lemma support_mul_single_subset [decidable_eq G] [has_mul G]
+  (f : monoid_algebra k G) (r : k) (a : G) :
+  (f * single a r).support ⊆ finset.image (* a) f.support :=
+begin
+  intros x hx,
+  contrapose hx,
+  have : ∀ y, y * a = x → f y = 0,
+  { simpa only [not_and', mem_image, mem_support_iff, exists_prop, not_exists, not_not] using hx },
+  simp only [mem_support_iff, mul_apply, sum_single_index, zero_mul, if_t_t, sum_zero, not_not],
+  exact finset.sum_eq_zero (by simp only [this, sum_single_index, ite_eq_right_iff,
+    eq_self_iff_true, implies_true_iff, zero_mul] {contextual := tt}),
+end
+
+lemma support_single_mul_eq_image [decidable_eq G] [has_mul G]
+  (f : monoid_algebra k G) {r : k} (hr : ∀ y, r * y = 0 ↔ y = 0) {x : G} (lx : is_left_regular x) :
+  (single x r * f : monoid_algebra k G).support = finset.image ((*) x) f.support :=
+begin
+  refine subset_antisymm (support_single_mul_subset f _ _) (λ y hy, _),
+  obtain ⟨y, yf, rfl⟩ : ∃ (a : G), a ∈ f.support ∧ x * a = y,
+  { simpa only [finset.mem_image, exists_prop] using hy },
+  simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index,
+    finsupp.sum_ite_eq', ne.def, not_false_iff, if_true, zero_mul, if_t_t, sum_zero, lx.eq_iff]
+end
+
+lemma support_mul_single_eq_image [decidable_eq G] [has_mul G]
+  (f : monoid_algebra k G) {r : k} (hr : ∀ y, y * r = 0 ↔ y = 0) {x : G} (rx : is_right_regular x) :
+  (f * single x r).support = finset.image (* x) f.support :=
+begin
+  refine subset_antisymm (support_mul_single_subset f _ _) (λ y hy, _),
+  obtain ⟨y, yf, rfl⟩ : ∃ (a : G), a ∈ f.support ∧ a * x = y,
+  { simpa only [finset.mem_image, exists_prop] using hy },
+  simp only [mul_apply, mem_support_iff.mp yf, hr, mem_support_iff, sum_single_index,
+    finsupp.sum_ite_eq', ne.def, not_false_iff, if_true, mul_zero, if_t_t, sum_zero, rx.eq_iff]
+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₂}) :=
@@ -24,47 +72,39 @@ 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] }
+  classical,
+  ext,
+  simp only [support_mul_single_eq_image f hr (is_right_regular_of_right_cancel_semigroup x),
+    mem_image, mem_map, mul_right_embedding_apply],
 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] }
+  classical,
+  ext,
+  simp only [support_single_mul_eq_image f hr (is_left_regular_of_left_cancel_semigroup x),
+    mem_image, mem_map, mul_left_embedding_apply],
 end
+
 section span
 
 variables [mul_one_class G]
 
-/-- An element of `monoid_algebra R M` is in the subalgebra generated by its support. -/
+/-- An element of `monoid_algebra k G` 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]
+variables {k : Type u₁} {G : 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₂}) :=
@@ -82,12 +122,12 @@ lemma support_single_mul [add_left_cancel_semigroup G]
 
 section span
 
-/-- An element of `add_monoid_algebra R M` is in the submodule generated by its support. -/
+/-- An element of `add_monoid_algebra k G` 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
+/-- An element of `add_monoid_algebra k G` 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)) :=