support.lean

/-
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₂} [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₂}) :=
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
  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
  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 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₂} [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 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 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)) :=
by rw [of', ← finsupp.supported_eq_span_single, finsupp.mem_supported]

end span

end add_monoid_algebra