Mathlib.Algebra.MonoidAlgebra.Support

MonoidAlgebra.support_mul theorem

[Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) : (a * b).support ⊆ a.support * b.support

Full source

theorem support_mul [Mul G] [DecidableEq G] (a b : MonoidAlgebra k G) :
    (a * b).support ⊆ a.support * b.support := by
  rw [MonoidAlgebra.mul_def]
  exact support_sum.trans <| biUnion_subset.2 fun _x hx ↦
    support_sum.trans <| biUnion_subset.2 fun _y hy ↦
      support_single_subset.trans <| singleton_subset_iff.2 <| mem_image₂_of_mem hx hy

Support of Product in Monoid Algebra is Contained in Product of Supports

Informal description

Let $G$ be a monoid with a decidable equality and $k$ a semiring. For any two elements $a, b$ in the monoid algebra $k[G]$, the support of their product $a * b$ is contained in the pointwise product of their supports, i.e., \[ \operatorname{supp}(a * b) \subseteq \operatorname{supp}(a) * \operatorname{supp}(b), \] where $\operatorname{supp}(a) * \operatorname{supp}(b) = \{g_1 \cdot g_2 \mid g_1 \in \operatorname{supp}(a), g_2 \in \operatorname{supp}(b)\}$.

MonoidAlgebra.support_single_mul_subset theorem

 [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
  (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support

Full source

theorem support_single_mul_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
    (single a r * f : MonoidAlgebra k G).support ⊆ Finset.image (a * ·) f.support :=
  (support_mul _ _).trans <| (Finset.image₂_subset_right support_single_subset).trans <| by
    rw [Finset.image₂_singleton_left]

Support of Left-Multiplication by Single Generator in Monoid Algebra is Contained in Left-Translated Support

Informal description

Let $G$ be a monoid with decidable equality and $k$ a semiring. For any element $f$ in the monoid algebra $k[G]$, any scalar $r \in k$, and any element $a \in G$, the support of the product $\text{single}(a, r) * f$ is contained in the image of the support of $f$ under left multiplication by $a$, i.e., \[ \operatorname{supp}(\text{single}(a, r) * f) \subseteq \{a \cdot g \mid g \in \operatorname{supp}(f)\}. \]

MonoidAlgebra.support_mul_single_subset theorem

 [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
  (f * single a r).support ⊆ Finset.image (· * a) f.support

Full source

theorem support_mul_single_subset [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) (r : k) (a : G) :
    (f * single a r).support ⊆ Finset.image (· * a) f.support :=
  (support_mul _ _).trans <| (Finset.image₂_subset_left support_single_subset).trans <| by
    rw [Finset.image₂_singleton_right]

Support of Right Multiplication by a Single Generator in Monoid Algebra is Contained in Right Translation of Support

Informal description

Let $G$ be a monoid with decidable equality and $k$ a semiring. For any element $f$ in the monoid algebra $k[G]$, any scalar $r \in k$, and any element $a \in G$, the support of the product $f * \text{single}(a, r)$ is contained in the image of the support of $f$ under the right multiplication map by $a$, i.e., \[ \operatorname{supp}(f * \text{single}(a, r)) \subseteq \{ g * a \mid g \in \operatorname{supp}(f) \}. \]

MonoidAlgebra.support_single_mul_eq_image theorem

 [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k} (hr : ∀ y, r * y = 0 ↔ y = 0) {x : G} (lx : IsLeftRegular x) :
  (single x r * f : MonoidAlgebra k G).support = Finset.image (x * ·) f.support

Full source

theorem support_single_mul_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
    (hr : ∀ y, r * y = 0 ↔ y = 0) {x : G} (lx : IsLeftRegular x) :
    (single x r * f : MonoidAlgebra k G).support = Finset.image (x * ·) f.support := by
  refine subset_antisymm (support_single_mul_subset f _ _) fun y hy => ?_
  obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ x * a = y := by
    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, not_false_iff, if_true, zero_mul, ite_self, sum_zero, lx.eq_iff]

Support of Left-Multiplication by Single Generator in Monoid Algebra Equals Left-Translated Support

Informal description

Let $G$ be a monoid with decidable equality, $k$ a semiring, and $f \in k[G]$ an element of the monoid algebra. For any scalar $r \in k$ satisfying $\forall y, r \cdot y = 0 \leftrightarrow y = 0$ and any element $x \in G$ that is left regular (i.e., left multiplication by $x$ is injective), the support of the product $\text{single}(x, r) * f$ is equal to the image of the support of $f$ under left multiplication by $x$. That is, \[ \operatorname{supp}(\text{single}(x, r) * f) = \{x \cdot g \mid g \in \operatorname{supp}(f)\}. \]

MonoidAlgebra.support_mul_single_eq_image theorem

 [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k} (hr : ∀ y, y * r = 0 ↔ y = 0) {x : G} (rx : IsRightRegular x) :
  (f * single x r).support = Finset.image (· * x) f.support

Full source

theorem support_mul_single_eq_image [DecidableEq G] [Mul G] (f : MonoidAlgebra k G) {r : k}
    (hr : ∀ y, y * r = 0 ↔ y = 0) {x : G} (rx : IsRightRegular x) :
    (f * single x r).support = Finset.image (· * x) f.support := by
  refine subset_antisymm (support_mul_single_subset f _ _) fun y hy => ?_
  obtain ⟨y, yf, rfl⟩ : ∃ a : G, a ∈ f.support ∧ a * x = y := by
    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, not_false_iff, if_true, mul_zero, ite_self, sum_zero, rx.eq_iff]

Support of Right Multiplication by a Single Generator Equals Right Translation of Support in Monoid Algebra

Informal description

Let $G$ be a monoid with decidable equality and $k$ a semiring. For any element $f$ in the monoid algebra $k[G]$, any scalar $r \in k$ such that $y \cdot r = 0$ if and only if $y = 0$ for all $y \in k$, and any right-regular element $x \in G$, the support of the product $f * \text{single}(x, r)$ is equal to the image of the support of $f$ under right multiplication by $x$, i.e., \[ \operatorname{supp}(f * \text{single}(x, r)) = \{ g * x \mid g \in \operatorname{supp}(f) \}. \]

MonoidAlgebra.support_mul_single theorem

 [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
  (f * single x r).support = f.support.map (mulRightEmbedding x)

Full source

theorem support_mul_single [Mul G] [IsRightCancelMul G] (f : MonoidAlgebra k G) (r : k)
    (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
    (f * single x r).support = f.support.map (mulRightEmbedding x) := by
  classical
    ext
    simp only [support_mul_single_eq_image f hr (IsRightRegular.all x),
      mem_image, mem_map, mulRightEmbedding_apply]

Support of Right Multiplication by Single Generator in Monoid Algebra Equals Right-Translated Support

Informal description

Let $G$ be a right-cancellative multiplicative monoid, $k$ a semiring, and $f \in k[G]$ an element of the monoid algebra. For any scalar $r \in k$ such that $y \cdot r = 0$ if and only if $y = 0$ for all $y \in k$, and any element $x \in G$, the support of the product $f * \text{single}(x, r)$ is equal to the image of the support of $f$ under the right multiplication map $g \mapsto g * x$. That is, \[ \operatorname{supp}(f * \text{single}(x, r)) = \{ g * x \mid g \in \operatorname{supp}(f) \}. \]

MonoidAlgebra.support_single_mul theorem

 [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k) (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
  (single x r * f : MonoidAlgebra k G).support = f.support.map (mulLeftEmbedding x)

Full source

theorem support_single_mul [Mul G] [IsLeftCancelMul G] (f : MonoidAlgebra k G) (r : k)
    (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
    (single x r * f : MonoidAlgebra k G).support = f.support.map (mulLeftEmbedding x) := by
  classical
    ext
    simp only [support_single_mul_eq_image f hr (IsLeftRegular.all x), mem_image,
      mem_map, mulLeftEmbedding_apply]

Support of Left-Multiplication by Single Generator in Monoid Algebra Equals Left-Translated Support

Informal description

Let $G$ be a left-cancellative multiplicative monoid, $k$ a semiring, and $f \in k[G]$ an element of the monoid algebra. For any scalar $r \in k$ such that $r \cdot y = 0$ if and only if $y = 0$ for all $y \in k$, and any element $x \in G$, the support of the product $\text{single}(x, r) * f$ is equal to the image of the support of $f$ under the left multiplication embedding by $x$. That is, \[ \operatorname{supp}(\text{single}(x, r) * f) = \{x \cdot g \mid g \in \operatorname{supp}(f)\}. \]

MonoidAlgebra.support_one_subset theorem

[One G] : (1 : MonoidAlgebra k G).support ⊆ 1

Full source

lemma support_one_subset [One G] : (1 : MonoidAlgebra k G).support ⊆ 1 :=
  Finsupp.support_single_subset

Support of the identity in a monoid algebra is contained in $\{1\}$

Informal description

For any monoid $G$ and semiring $k$, the support of the multiplicative identity element $1$ in the monoid algebra $k[G]$ is a subset of the singleton set $\{1\}$, where $1$ is the multiplicative identity of $G$.

MonoidAlgebra.support_one theorem

[One G] [NeZero (1 : k)] : (1 : MonoidAlgebra k G).support = 1

Full source

@[simp]
lemma support_one [One G] [NeZero (1 : k)] : (1 : MonoidAlgebra k G).support = 1 :=
  Finsupp.support_single_ne_zero _ one_ne_zero

Support of Identity in Monoid Algebra: $\text{supp}(1) = \{1\}$

Informal description

Let $k$ be a semiring with $1 \neq 0$ and $G$ be a monoid. The support of the multiplicative identity $1$ in the monoid algebra $k[G]$ is exactly the singleton set $\{1\}$, where $1$ denotes the identity element of $G$.

MonoidAlgebra.mem_span_support theorem

(f : MonoidAlgebra k G) : f ∈ Submodule.span k (of k G '' (f.support : Set G))

Full source

/-- An element of `MonoidAlgebra k G` is in the subalgebra generated by its support. -/
theorem mem_span_support (f : MonoidAlgebra k G) :
    f ∈ Submodule.span k (of k G '' (f.support : Set G)) := by
  erw [of, MonoidHom.coe_mk, ← supported_eq_span_single, Finsupp.mem_supported]

Span Property of Monoid Algebra Elements: $f \in \operatorname{span}_k \{\text{of}(g) \mid g \in \operatorname{supp}(f)\}$

Informal description

For any element $f$ in the monoid algebra $k[G]$, $f$ lies in the $k$-linear span of the image of its support under the canonical embedding $\text{of} \colon G \to k[G]$. That is, $f \in \operatorname{span}_k \{\text{of}(g) \mid g \in \operatorname{supp}(f)\}$.

AddMonoidAlgebra.support_mul theorem

[DecidableEq G] [Add G] (a b : k[G]) :
    (a * b).support ⊆ a.support + b.support

Full source

theorem support_mul [DecidableEq G] [Add G] (a b : k[G]) :
    (a * b).support ⊆ a.support + b.support :=
  @MonoidAlgebra.support_mul k (Multiplicative G) _ _ _ _ _

Support of Product in Additive Monoid Algebra is Contained in Minkowski Sum of Supports

Informal description

Let $G$ be an additive monoid with decidable equality and $k$ a semiring. For any two elements $a, b$ in the additive monoid algebra $k[G]$, the support of their product $a * b$ is contained in the Minkowski sum of their supports, i.e., \[ \operatorname{supp}(a * b) \subseteq \operatorname{supp}(a) + \operatorname{supp}(b), \] where $\operatorname{supp}(a) + \operatorname{supp}(b) = \{g_1 + g_2 \mid g_1 \in \operatorname{supp}(a), g_2 \in \operatorname{supp}(b)\}$.

AddMonoidAlgebra.support_mul_single theorem

[Add G] [IsRightCancelAdd G] (f : k[G]) (r : k)
    (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
    (f * single x r : k[G]).support = f.support.map (addRightEmbedding x)

Full source

theorem support_mul_single [Add G] [IsRightCancelAdd G] (f : k[G]) (r : k)
    (hr : ∀ y, y * r = 0 ↔ y = 0) (x : G) :
    (f * single x r : k[G]).support = f.support.map (addRightEmbedding x) :=
  MonoidAlgebra.support_mul_single (G := Multiplicative G) _ _ hr _

Support of Right Multiplication by Single Generator in Additive Monoid Algebra Equals Right-Translated Support

Informal description

Let $G$ be an additive monoid with right-cancellative addition, $k$ a semiring, and $f \in k[G]$ an element of the additive monoid algebra. For any scalar $r \in k$ such that $y \cdot r = 0$ if and only if $y = 0$ for all $y \in k$, and any element $x \in G$, the support of the product $f * \text{single}(x, r)$ is equal to the image of the support of $f$ under the right addition map $g \mapsto g + x$. That is, \[ \operatorname{supp}(f * \text{single}(x, r)) = \{ g + x \mid g \in \operatorname{supp}(f) \}. \]

AddMonoidAlgebra.support_single_mul theorem

[Add G] [IsLeftCancelAdd G] (f : k[G]) (r : k)
    (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
    (single x r * f : k[G]).support = f.support.map (addLeftEmbedding x)

Full source

theorem support_single_mul [Add G] [IsLeftCancelAdd G] (f : k[G]) (r : k)
    (hr : ∀ y, r * y = 0 ↔ y = 0) (x : G) :
    (single x r * f : k[G]).support = f.support.map (addLeftEmbedding x) :=
  MonoidAlgebra.support_single_mul (G := Multiplicative G) _ _ hr _

Support of Left-Multiplication by Single Generator in Additive Monoid Algebra Equals Left-Translated Support

Informal description

Let $G$ be an additive monoid with left-cancellative addition, $k$ a semiring, and $f \in k[G]$ an element of the additive monoid algebra. For any scalar $r \in k$ such that $r \cdot y = 0$ if and only if $y = 0$ for all $y \in k$, and any element $x \in G$, the support of the product $\text{single}(x, r) * f$ is equal to the image of the support of $f$ under the left addition embedding by $x$. That is, \[ \operatorname{supp}(\text{single}(x, r) * f) = \{x + g \mid g \in \operatorname{supp}(f)\}. \]

AddMonoidAlgebra.support_one_subset theorem

[Zero G] : (1 : k[G]).support ⊆ 0

Full source

lemma support_one_subset [Zero G] : (1 : k[G]).support ⊆ 0 := Finsupp.support_single_subset

Support of the Identity in Additive Monoid Algebra is Subset of Zero

Informal description

For any additive monoid $G$ with a zero element and any semiring $k$, the support of the multiplicative identity $1$ in the additive monoid algebra $k[G]$ is a subset of the singleton set $\{0\}$.

AddMonoidAlgebra.support_one theorem

[Zero G] [NeZero (1 : k)] : (1 : k[G]).support = 0

Full source

@[simp]
lemma support_one [Zero G] [NeZero (1 : k)] : (1 : k[G]).support = 0 :=
  Finsupp.support_single_ne_zero _ one_ne_zero

Support of Identity in Additive Monoid Algebra: $\text{supp}(1) = \{0\}$

Informal description

Let $k$ be a semiring with $1 \neq 0$ and $G$ be an additive monoid with zero. Then the support of the multiplicative identity $1$ in the additive monoid algebra $k[G]$ is exactly the singleton set $\{0\}$.

AddMonoidAlgebra.mem_span_support theorem

[AddZeroClass G] (f : k[G]) :
    f ∈ Submodule.span k (of k G '' (f.support : Set G))

Full source

/-- An element of `k[G]` is in the submodule generated by its support. -/
theorem mem_span_support [AddZeroClass G] (f : k[G]) :
    f ∈ Submodule.span k (of k G '' (f.support : Set G)) := by
  erw [of, MonoidHom.coe_mk, ← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

Element of Additive Monoid Algebra Lies in Span of Its Support

Informal description

For any additive monoid $G$ with a zero element and any semiring $k$, every element $f$ of the additive monoid algebra $k[G]$ lies in the $k$-linear span of the image of its support under the canonical embedding $\text{of} : G \to k[G]$. That is, \[ f \in \operatorname{span}_k \{\text{of}(g) \mid g \in \operatorname{supp}(f)\}, \] where $\operatorname{supp}(f) = \{g \in G \mid f(g) \neq 0\}$ is the support of $f$.

AddMonoidAlgebra.mem_span_support' theorem

(f : k[G]) :
    f ∈ Submodule.span k (of' k G '' (f.support : Set G))

Full source

/-- An element of `k[G]` is in the subalgebra generated by its support, using
unbundled inclusion. -/
theorem mem_span_support' (f : k[G]) :
    f ∈ Submodule.span k (of' k G '' (f.support : Set G)) := by
  delta of'
  rw [← Finsupp.supported_eq_span_single, Finsupp.mem_supported]

Element of Additive Monoid Algebra Lies in Span of Its Support

Informal description

For any element $f$ in the additive monoid algebra $k[G]$, $f$ lies in the $k$-linear span of the image of its support under the canonical embedding $\text{of}' : G \to k[G]$. That is, \[ f \in \operatorname{span}_k \{\text{of}'(g) \mid g \in \operatorname{supp}(f)\}. \]