Mathlib.Algebra.MonoidAlgebra.Defs

MonoidAlgebra definition

: Type max u₁ u₂

Full source

/-- The monoid algebra over a semiring `k` generated by the monoid `G`.
It is the type of finite formal `k`-linear combinations of terms of `G`,
endowed with the convolution product.
-/
def MonoidAlgebra : Type max u₁ u₂ :=
  G →₀ k

Monoid algebra

Informal description

The monoid algebra $k[G]$ over a semiring $k$ generated by a monoid $G$ is the type of finite formal $k$-linear combinations of elements of $G$, equipped with the convolution product. Formally, it is defined as the type of finitely supported functions from $G$ to $k$, denoted $G \to₀ k$.

MonoidAlgebra.inhabited instance

: Inhabited (MonoidAlgebra k G)

Full source

instance MonoidAlgebra.inhabited : Inhabited (MonoidAlgebra k G) :=
  inferInstanceAs (Inhabited (G →₀ k))

Inhabitedness of Monoid Algebras

Informal description

The monoid algebra $k[G]$ over a semiring $k$ generated by a monoid $G$ is always inhabited (i.e., nonempty).

MonoidAlgebra.addCommMonoid instance

: AddCommMonoid (MonoidAlgebra k G)

Full source

instance MonoidAlgebra.addCommMonoid : AddCommMonoid (MonoidAlgebra k G) :=
  inferInstanceAs (AddCommMonoid (G →₀ k))

Additive Commutative Monoid Structure on Monoid Algebras

Informal description

The monoid algebra $k[G]$ over a semiring $k$ generated by a monoid $G$ forms an additive commutative monoid under pointwise addition of its finitely supported functions.

MonoidAlgebra.instIsCancelAdd instance

[IsCancelAdd k] : IsCancelAdd (MonoidAlgebra k G)

Full source

instance MonoidAlgebra.instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (MonoidAlgebra k G) :=
  inferInstanceAs (IsCancelAdd (G →₀ k))

Cancellative Addition in Monoid Algebras

Informal description

For any semiring $k$ with a cancellative addition and any monoid $G$, the monoid algebra $k[G]$ also has a cancellative addition operation. That is, for any $f, g, h \in k[G]$, if $f + h = g + h$ or $h + f = h + g$, then $f = g$.

MonoidAlgebra.coeFun instance

: CoeFun (MonoidAlgebra k G) fun _ => G → k

Full source

instance MonoidAlgebra.coeFun : CoeFun (MonoidAlgebra k G) fun _ => G → k :=
  inferInstanceAs (CoeFun (G →₀ k) _)

Function Representation of Monoid Algebra Elements

Informal description

The monoid algebra $k[G]$ can be treated as a function from $G$ to $k$, where each element of $k[G]$ is interpreted as its underlying function representation.

MonoidAlgebra.single abbrev

(a : G) (b : k) : MonoidAlgebra k G

Full source

abbrev single (a : G) (b : k) : MonoidAlgebra k G := Finsupp.single a b

Single generator element in monoid algebra

Informal description

For a monoid $G$ and a semiring $k$, the function $\text{single}(a, b)$ constructs an element of the monoid algebra $k[G]$ that has value $b$ at $a \in G$ and zero elsewhere. Formally, it is the finitely supported function $G \to k$ defined by: $$\text{single}(a, b)(g) = \begin{cases} b & \text{if } g = a \\ 0 & \text{otherwise} \end{cases}$$

MonoidAlgebra.single_zero theorem

(a : G) : (single a 0 : MonoidAlgebra k G) = 0

Full source

theorem single_zero (a : G) : (single a 0 : MonoidAlgebra k G) = 0 := Finsupp.single_zero a

Vanishing property of single generator with zero coefficient in monoid algebra

Informal description

For any element $a$ of a monoid $G$ and any semiring $k$, the element $\text{single}(a, 0)$ in the monoid algebra $k[G]$ is equal to the zero element of $k[G]$. Here, $\text{single}(a, b)$ denotes the element of $k[G]$ that takes the value $b$ at $a$ and zero elsewhere.

MonoidAlgebra.single_add theorem

(a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂

Full source

theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
  Finsupp.single_add a b₁ b₂

Additivity of Single Generator in Monoid Algebra

Informal description

For any element $a$ in a monoid $G$ and any elements $b_1, b_2$ in a semiring $k$, the single generator element in the monoid algebra $k[G]$ satisfies: \[ \text{single}(a, b_1 + b_2) = \text{single}(a, b_1) + \text{single}(a, b_2). \]

MonoidAlgebra.sum_single_index theorem

{N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) : (single a b).sum h = h a b

Full source

@[simp]
theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N}
    (h_zero : h a 0 = 0) :
    (single a b).sum h = h a b := Finsupp.sum_single_index h_zero

Summation of Single Generator in Monoid Algebra

Informal description

Let $G$ be a monoid, $k$ a semiring, and $N$ an additive commutative monoid. For any element $a \in G$, any coefficient $b \in k$, and any function $h : G \to k \to N$ satisfying $h(a, 0) = 0$, the sum of the monoid algebra element $\text{single}(a, b)$ over $h$ equals $h(a, b)$. That is, \[ \sum_{g \in G} h(g, \text{single}(a, b)(g)) = h(a, b). \]

MonoidAlgebra.sum_single theorem

(f : MonoidAlgebra k G) : f.sum single = f

Full source

@[simp]
theorem sum_single (f : MonoidAlgebra k G) : f.sum single = f :=
  Finsupp.sum_single f

Decomposition of Monoid Algebra Elements into Single Generators

Informal description

For any element $f$ in the monoid algebra $k[G]$, the sum over the support of $f$ of the single-point functions $\text{single}(a, f(a))$ equals $f$ itself. That is, \[ \sum_{a \in \operatorname{supp}(f)} \text{single}(a, f(a)) = f. \]

MonoidAlgebra.single_apply theorem

{a a' : G} {b : k} [Decidable (a = a')] : single a b a' = if a = a' then b else 0

Full source

theorem single_apply {a a' : G} {b : k} [Decidable (a = a')] :
    single a b a' = if a = a' then b else 0 :=
  Finsupp.single_apply

Evaluation of Single Generator in Monoid Algebra

Informal description

For any elements $a, a'$ in a monoid $G$ and any element $b$ in a semiring $k$, the evaluation of the monoid algebra element $\text{single}(a, b)$ at $a'$ is given by: $$(\text{single}(a, b))(a') = \begin{cases} b & \text{if } a = a' \\ 0 & \text{otherwise} \end{cases}$$

MonoidAlgebra.single_eq_zero theorem

{a : G} {b : k} : single a b = 0 ↔ b = 0

Full source

@[simp]
theorem single_eq_zero {a : G} {b : k} : singlesingle a b = 0 ↔ b = 0 := Finsupp.single_eq_zero

Zero Condition for Single Generator in Monoid Algebra

Informal description

For any element $a$ in a monoid $G$ and any element $b$ in a semiring $k$, the monoid algebra element $\text{single}(a, b)$ is equal to the zero element of $k[G]$ if and only if $b$ is equal to the zero element of $k$. In mathematical notation: $$\text{single}(a, b) = 0 \leftrightarrow b = 0$$

MonoidAlgebra.single_ne_zero theorem

{a : G} {b : k} : single a b ≠ 0 ↔ b ≠ 0

Full source

theorem single_ne_zero {a : G} {b : k} : singlesingle a b ≠ 0single a b ≠ 0 ↔ b ≠ 0 := Finsupp.single_ne_zero

Nonzero Condition for Single Generator in Monoid Algebra

Informal description

For any element $a$ in a monoid $G$ and any element $b$ in a semiring $k$, the monoid algebra element $\text{single}(a, b)$ is nonzero if and only if $b$ is nonzero. In mathematical notation: $$\text{single}(a, b) \neq 0 \leftrightarrow b \neq 0$$

MonoidAlgebra.liftNC definition

(f : k →+ R) (g : G → R) : MonoidAlgebra k G →+ R

Full source

/-- A non-commutative version of `MonoidAlgebra.lift`: given an additive homomorphism `f : k →+ R`
and a homomorphism `g : G → R`, returns the additive homomorphism from
`MonoidAlgebra k G` such that `liftNC f g (single a b) = f b * g a`. If `f` is a ring homomorphism
and the range of either `f` or `g` is in center of `R`, then the result is a ring homomorphism.  If
`R` is a `k`-algebra and `f = algebraMap k R`, then the result is an algebra homomorphism called
`MonoidAlgebra.lift`. -/
def liftNC (f : k →+ R) (g : G → R) : MonoidAlgebraMonoidAlgebra k G →+ R :=
  liftAddHom fun x : G => (AddMonoidHom.mulRight (g x)).comp f

Non-commutative lift of homomorphisms to monoid algebra

Informal description

Given an additive homomorphism $f \colon k \to^+ R$ and a multiplicative homomorphism $g \colon G \to R$, the function $\text{liftNC}(f, g) \colon k[G] \to^+ R$ is the additive homomorphism from the monoid algebra $k[G]$ to $R$ defined by linearly extending the map $\text{single}(a, b) \mapsto f(b) \cdot g(a)$ for all $a \in G$ and $b \in k$. More explicitly, for any finitely supported function $\varphi \in k[G]$, we have: $$\text{liftNC}(f, g)(\varphi) = \sum_{a \in \text{supp}(\varphi)} f(\varphi(a)) \cdot g(a)$$ If $f$ is a ring homomorphism and the range of either $f$ or $g$ lies in the center of $R$, then $\text{liftNC}(f, g)$ is a ring homomorphism. When $R$ is a $k$-algebra and $f$ is the algebra map $k \to R$, this construction yields an algebra homomorphism.

MonoidAlgebra.liftNC_single theorem

(f : k →+ R) (g : G → R) (a : G) (b : k) : liftNC f g (single a b) = f b * g a

Full source

@[simp]
theorem liftNC_single (f : k →+ R) (g : G → R) (a : G) (b : k) :
    liftNC f g (single a b) = f b * g a :=
  liftAddHom_apply_single _ _ _

Evaluation of Lifted Homomorphism on Single Generator in Monoid Algebra

Informal description

Let $k$ be a semiring and $G$ a monoid. Given an additive homomorphism $f \colon k \to^+ R$ and a multiplicative homomorphism $g \colon G \to R$, the evaluation of the lifted homomorphism $\text{liftNC}(f, g)$ on the single generator $\text{single}(a, b) \in k[G]$ (where $a \in G$ and $b \in k$) satisfies: \[ \text{liftNC}(f, g)(\text{single}(a, b)) = f(b) \cdot g(a). \]

MonoidAlgebra.mul' definition

(f g : MonoidAlgebra k G) : MonoidAlgebra k G

Full source

/-- The multiplication in a monoid algebra. We make it irreducible so that Lean doesn't unfold
it trying to unify two things that are different. -/
@[irreducible] def mul' (f g : MonoidAlgebra k G) : MonoidAlgebra k G :=
  f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)

Multiplication in monoid algebra

Informal description

The multiplication operation in the monoid algebra $k[G]$ is defined for two elements $f, g \in k[G]$ as the convolution product: $$(f * g)(a) = \sum_{a_1 a_2 = a} f(a_1) \cdot g(a_2)$$ where the sum is taken over all pairs $(a_1, a_2) \in G \times G$ such that $a_1 \cdot a_2 = a$ in $G$.

MonoidAlgebra.instMul instance

: Mul (MonoidAlgebra k G)

Full source

/-- The product of `f g : MonoidAlgebra k G` is the finitely supported function
  whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
  such that `x * y = a`. (Think of the group ring of a group.) -/
instance instMul : Mul (MonoidAlgebra k G) := ⟨MonoidAlgebra.mul'⟩

Multiplication Operation in Monoid Algebra

Informal description

The monoid algebra $k[G]$ is equipped with a multiplication operation defined as the convolution product: for any two elements $f, g \in k[G]$, their product $f * g$ is given by $$(f * g)(a) = \sum_{a_1 a_2 = a} f(a_1) \cdot g(a_2)$$ where the sum is taken over all pairs $(a_1, a_2) \in G \times G$ such that $a_1 \cdot a_2 = a$ in $G$.

MonoidAlgebra.mul_def theorem

{f g : MonoidAlgebra k G} : f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂)

Full source

theorem mul_def {f g : MonoidAlgebra k G} :
    f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ * a₂) (b₁ * b₂) := by
  with_unfolding_all rfl

Definition of Multiplication in Monoid Algebra via Double Sum

Informal description

For any two elements $f, g$ in the monoid algebra $k[G]$, their product $f * g$ is given by the double sum $$ f * g = \sum_{a_1 \in G} \sum_{a_2 \in G} \text{single}(a_1 \cdot a_2, f(a_1) \cdot g(a_2)) $$ where $\text{single}(a, b)$ denotes the element of $k[G]$ that has value $b$ at $a$ and zero elsewhere.

MonoidAlgebra.nonUnitalNonAssocSemiring instance

: NonUnitalNonAssocSemiring (MonoidAlgebra k G)

Full source

instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring (MonoidAlgebra k G) :=
  { Finsupp.instAddCommMonoid with
    -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
    left_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_add_index ?_ ?_)) ?_ <;>
        simp only [mul_add, mul_zero, single_zero, single_add, forall_true_iff, sum_add]
    right_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
        simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]
    zero_mul := fun f => by
      simp only [mul_def]
      exact sum_zero_index
    mul_zero := fun f => by
      simp only [mul_def]
      exact Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_zero_index)) sum_zero }

Non-unital Non-associative Semiring Structure on Monoid Algebra

Informal description

The monoid algebra $k[G]$ over a semiring $k$ generated by a monoid $G$ forms a non-unital, non-associative semiring under the convolution product. This means it has: - An addition operation $+$ forming an additive commutative monoid - A multiplication operation $*$ (convolution product) that distributes over addition - A zero element that is absorbing for multiplication without requiring: - A multiplicative identity - Associativity of multiplication - Commutativity of multiplication

MonoidAlgebra.liftNC_mul theorem

 {g_hom : Type*} [FunLike g_hom G R] [MulHomClass g_hom G R] (f : k →+* R) (g : g_hom) (a b : MonoidAlgebra k G)
  (h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g y)) :
  liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b

Full source

theorem liftNC_mul {g_hom : Type*} [FunLike g_hom G R] [MulHomClass g_hom G R]
    (f : k →+* R) (g : g_hom) (a b : MonoidAlgebra k G)
    (h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g y)) :
    liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b := by
  conv_rhs => rw [← sum_single a, ← sum_single b]
  -- Porting note: `(liftNC _ g).map_finsuppSum` → `map_finsuppSum`
  simp_rw [mul_def, map_finsuppSum, liftNC_single, Finsupp.sum_mul, Finsupp.mul_sum]
  refine Finset.sum_congr rfl fun y hy => Finset.sum_congr rfl fun x _hx => ?_
  simp [mul_assoc, (h_comm hy).left_comm]

Multiplicativity of Lifted Homomorphism in Monoid Algebra under Commutation Condition

Informal description

Let $k$ be a semiring, $G$ a monoid, and $R$ a non-associative semiring. Given a ring homomorphism $f \colon k \to R$ and a multiplicative homomorphism $g \colon G \to R$ (represented by a type $g\_hom$ with appropriate homomorphism properties), the lifted homomorphism $\text{liftNC}(f, g) \colon k[G] \to R$ satisfies the following multiplicative property: For any two elements $a, b \in k[G]$, if for every $x$ in the support of $a$ and every $y$ in the support of $b$, the elements $f(b(x))$ and $g(y)$ commute in $R$, then \[ \text{liftNC}(f, g)(a * b) = \text{liftNC}(f, g)(a) * \text{liftNC}(f, g)(b). \]

MonoidAlgebra.nonUnitalSemiring instance

: NonUnitalSemiring (MonoidAlgebra k G)

Full source

instance nonUnitalSemiring : NonUnitalSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalNonAssocSemiring with
    mul_assoc := fun f g h => by
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      simp only [mul_def]
      rw [sum_sum_index] <;> congr; on_goal 1 => ext a₁ b₁
      rw [sum_sum_index, sum_sum_index] <;> congr; on_goal 1 => ext a₂ b₂
      rw [sum_sum_index, sum_single_index] <;> congr; on_goal 1 => ext a₃ b₃
      on_goal 1 => rw [sum_single_index, mul_assoc, mul_assoc]
      all_goals simp only [single_zero, single_add, forall_true_iff, add_mul,
        mul_add, zero_mul, mul_zero, sum_zero, sum_add] }

Non-unital Semiring Structure on Monoid Algebra

Informal description

The monoid algebra $k[G]$ over a semiring $k$ generated by a monoid $G$ forms a non-unital semiring under the convolution product. This means it has: - An addition operation $+$ forming an additive commutative monoid - A multiplication operation $*$ (convolution product) that is associative and distributes over addition - A zero element that is absorbing for multiplication without requiring a multiplicative identity or commutativity of multiplication.

MonoidAlgebra.one instance

: One (MonoidAlgebra k G)

Full source

/-- The unit of the multiplication is `single 1 1`, i.e. the function
  that is `1` at `1` and zero elsewhere. -/
instance one : One (MonoidAlgebra k G) :=
  ⟨single 1 1⟩

Multiplicative Identity in Monoid Algebra

Informal description

The monoid algebra $k[G]$ has a multiplicative identity given by the function that is $1$ at the identity element of $G$ and zero elsewhere. Formally, this is the element $\text{single}(1, 1)$ where $\text{single}$ is the canonical embedding of $G \times k$ into $k[G]$.

MonoidAlgebra.one_def theorem

: (1 : MonoidAlgebra k G) = single 1 1

Full source

theorem one_def : (1 : MonoidAlgebra k G) = single 1 1 :=
  rfl

Identity Element in Monoid Algebra: $1 = \text{single}(1_G, 1_k)$

Informal description

The multiplicative identity element in the monoid algebra $k[G]$ is given by the function that maps the identity element of $G$ to $1 \in k$ and all other elements of $G$ to $0$. Formally, this is expressed as $1 = \text{single}(1_G, 1_k)$, where $\text{single}$ is the canonical embedding of $G \times k$ into $k[G]$.

MonoidAlgebra.liftNC_one theorem

{g_hom : Type*} [FunLike g_hom G R] [OneHomClass g_hom G R] (f : k →+* R) (g : g_hom) : liftNC (f : k →+ R) g 1 = 1

Full source

@[simp]
theorem liftNC_one {g_hom : Type*} [FunLike g_hom G R] [OneHomClass g_hom G R]
    (f : k →+* R) (g : g_hom) :
    liftNC (f : k →+ R) g 1 = 1 := by simp [one_def]

Lifted Homomorphism Preserves Identity in Monoid Algebra: $\text{liftNC}(f, g)(1) = 1$

Informal description

Let $k$ be a semiring, $G$ a monoid, and $R$ a non-associative semiring. Given a ring homomorphism $f \colon k \to R$ and a multiplicative homomorphism $g \colon G \to R$ that preserves the identity element (i.e., $g(1_G) = 1_R$), the lifted homomorphism $\text{liftNC}(f, g) \colon k[G] \to R$ satisfies $\text{liftNC}(f, g)(1_{k[G]}) = 1_R$. Here, $1_{k[G]}$ denotes the multiplicative identity in the monoid algebra $k[G]$, which is given by $\text{single}(1_G, 1_k)$.

MonoidAlgebra.nonAssocSemiring instance

: NonAssocSemiring (MonoidAlgebra k G)

Full source

instance nonAssocSemiring : NonAssocSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalNonAssocSemiring with
    natCast := fun n => single 1 n
    natCast_zero := by simp
    natCast_succ := fun _ => by simp; rfl
    one_mul := fun f => by
      simp only [mul_def, one_def, sum_single_index, zero_mul, single_zero, sum_zero, zero_add,
        one_mul, sum_single]
    mul_one := fun f => by
      simp only [mul_def, one_def, sum_single_index, mul_zero, single_zero, sum_zero, add_zero,
        mul_one, sum_single] }

Non-Associative Semiring Structure on Monoid Algebra

Informal description

The monoid algebra $k[G]$ over a semiring $k$ generated by a monoid $G$ forms a non-associative semiring. This means it has: - An addition operation $+$ forming an additive commutative monoid - A multiplication operation $*$ (convolution product) that distributes over addition - A zero element that is absorbing for multiplication - A multiplicative identity element (given by $\text{single}(1_G, 1_k)$) without requiring associativity of multiplication.

MonoidAlgebra.natCast_def theorem

(n : ℕ) : (n : MonoidAlgebra k G) = single (1 : G) (n : k)

Full source

theorem natCast_def (n : ℕ) : (n : MonoidAlgebra k G) = single (1 : G) (n : k) :=
  rfl

Canonical Inclusion of Natural Numbers in Monoid Algebra via Single Generator

Informal description

For any natural number $n$, the canonical inclusion of $n$ in the monoid algebra $k[G]$ is equal to the element $\text{single}(1_G, n)$, where $1_G$ is the multiplicative identity of $G$ and $n$ is interpreted as an element of $k$.

MonoidAlgebra.semiring instance

: Semiring (MonoidAlgebra k G)

Full source

instance semiring : Semiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalSemiring,
    MonoidAlgebra.nonAssocSemiring with }

Semiring Structure on Monoid Algebra

Informal description

For any semiring $k$ and monoid $G$, the monoid algebra $k[G]$ forms a semiring under the convolution product. This means it has: - An addition operation $+$ forming an additive commutative monoid - A multiplication operation $*$ (convolution product) that is associative and distributes over addition - A zero element that is absorbing for multiplication - A multiplicative identity element (given by $\text{single}(1_G, 1_k)$)

MonoidAlgebra.liftNCRingHom definition

(f : k →+* R) (g : G →* R) (h_comm : ∀ x y, Commute (f x) (g y)) : MonoidAlgebra k G →+* R

Full source

/-- `liftNC` as a `RingHom`, for when `f x` and `g y` commute -/
def liftNCRingHom (f : k →+* R) (g : G →* R) (h_comm : ∀ x y, Commute (f x) (g y)) :
    MonoidAlgebraMonoidAlgebra k G →+* R :=
  { liftNC (f : k →+ R) g with
    map_one' := liftNC_one _ _
    map_mul' := fun _a _b => liftNC_mul _ _ _ _ fun {_ _} _ => h_comm _ _ }

Ring homomorphism from monoid algebra induced by commuting homomorphisms

Informal description

Given a semiring homomorphism $ f \colon k \to R $ and a monoid homomorphism $ g \colon G \to R $ such that $ f(x) $ and $ g(y) $ commute for all $ x \in k $ and $ y \in G $, the function $ \text{liftNCRingHom}(f, g) \colon k[G] \to R $ is the ring homomorphism from the monoid algebra $ k[G] $ to $ R $ defined by linearly extending the map $ \text{single}(a, b) \mapsto f(b) \cdot g(a) $ for all $ a \in G $ and $ b \in k $. More explicitly, for any finitely supported function $ \varphi \in k[G] $, we have: \[ \text{liftNCRingHom}(f, g)(\varphi) = \sum_{a \in \text{supp}(\varphi)} f(\varphi(a)) \cdot g(a). \] This homomorphism preserves the multiplicative identity and the convolution product structure of the monoid algebra.

MonoidAlgebra.nonUnitalCommSemiring instance

[CommSemiring k] [CommSemigroup G] : NonUnitalCommSemiring (MonoidAlgebra k G)

Full source

instance nonUnitalCommSemiring [CommSemiring k] [CommSemigroup G] :
    NonUnitalCommSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalSemiring with
    mul_comm := fun f g => by
      simp only [mul_def, Finsupp.sum, mul_comm]
      rw [Finset.sum_comm]
      simp only [mul_comm] }

Non-unital Commutative Semiring Structure on Monoid Algebra

Informal description

For any commutative semiring $k$ and commutative semigroup $G$, the monoid algebra $k[G]$ forms a non-unital commutative semiring under the convolution product. This means it has: - An addition operation $+$ forming an additive commutative monoid - A commutative and associative multiplication operation $*$ (convolution product) that distributes over addition - A zero element that is absorbing for multiplication without requiring a multiplicative identity.

MonoidAlgebra.nontrivial instance

[Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial (MonoidAlgebra k G)

Full source

instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial (MonoidAlgebra k G) :=
  Finsupp.instNontrivial

Nontriviality of Monoid Algebras over Nontrivial Semirings

Informal description

For any nontrivial semiring $k$ and nonempty monoid $G$, the monoid algebra $k[G]$ is also nontrivial.

MonoidAlgebra.commSemiring instance

[CommSemiring k] [CommMonoid G] : CommSemiring (MonoidAlgebra k G)

Full source

instance commSemiring [CommSemiring k] [CommMonoid G] : CommSemiring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommSemiring, MonoidAlgebra.semiring with }

Commutative Semiring Structure on Monoid Algebra

Informal description

For any commutative semiring $k$ and commutative monoid $G$, the monoid algebra $k[G]$ forms a commutative semiring under the convolution product. This means it has: - An addition operation $+$ forming an additive commutative monoid - A commutative and associative multiplication operation $*$ (convolution product) that distributes over addition - A zero element that is absorbing for multiplication - A multiplicative identity element (given by $\text{single}(1_G, 1_k)$)

MonoidAlgebra.unique instance

[Semiring k] [Subsingleton k] : Unique (MonoidAlgebra k G)

Full source

instance unique [Semiring k] [Subsingleton k] : Unique (MonoidAlgebra k G) :=
  Finsupp.uniqueOfRight

Uniqueness of Monoid Algebra over a Subsingleton Semiring

Informal description

For any semiring $k$ with a unique term (i.e., $k$ is a subsingleton), the monoid algebra $k[G]$ also has a unique term.

MonoidAlgebra.addCommGroup instance

[Ring k] : AddCommGroup (MonoidAlgebra k G)

Full source

instance addCommGroup [Ring k] : AddCommGroup (MonoidAlgebra k G) :=
  Finsupp.instAddCommGroup

Additive Commutative Group Structure on Monoid Algebra

Informal description

For any ring $k$ and any type $G$, the monoid algebra $k[G]$ forms an additive commutative group under pointwise addition of functions.

MonoidAlgebra.nonUnitalNonAssocRing instance

[Ring k] [Mul G] : NonUnitalNonAssocRing (MonoidAlgebra k G)

Full source

instance nonUnitalNonAssocRing [Ring k] [Mul G] : NonUnitalNonAssocRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup, MonoidAlgebra.nonUnitalNonAssocSemiring with }

Non-unital Non-associative Ring Structure on Monoid Algebra

Informal description

For any ring $k$ and any type $G$ equipped with a multiplication operation, the monoid algebra $k[G]$ forms a non-unital, non-associative ring under pointwise addition and the convolution product.

MonoidAlgebra.nonUnitalRing instance

[Ring k] [Semigroup G] : NonUnitalRing (MonoidAlgebra k G)

Full source

instance nonUnitalRing [Ring k] [Semigroup G] : NonUnitalRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup, MonoidAlgebra.nonUnitalSemiring with }

Non-unital Ring Structure on Monoid Algebra of a Semigroup

Informal description

For any ring $k$ and any semigroup $G$, the monoid algebra $k[G]$ forms a non-unital ring under pointwise addition and the convolution product. This means it has: - An additive commutative group structure - A multiplication operation that is associative and distributes over addition - A zero element that is absorbing for multiplication without requiring a multiplicative identity.

MonoidAlgebra.nonAssocRing instance

[Ring k] [MulOneClass G] : NonAssocRing (MonoidAlgebra k G)

Full source

instance nonAssocRing [Ring k] [MulOneClass G] : NonAssocRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.addCommGroup,
    MonoidAlgebra.nonAssocSemiring with
    intCast := fun z => single 1 (z : k)
    intCast_ofNat n := by simp [natCast_def]
    intCast_negSucc n := by simp [natCast_def, one_def] }

Non-Associative Ring Structure on Monoid Algebra

Informal description

For any ring $k$ and any multiplicative monoid $G$, the monoid algebra $k[G]$ forms a non-associative ring. This means it has: - An addition operation $+$ forming an additive commutative group - A multiplication operation $*$ (convolution product) that distributes over addition - A zero element that is absorbing for multiplication - A multiplicative identity element (given by $\text{single}(1_G, 1_k)$) without requiring associativity of multiplication.

MonoidAlgebra.intCast_def theorem

[Ring k] [MulOneClass G] (z : ℤ) : (z : MonoidAlgebra k G) = single (1 : G) (z : k)

Full source

theorem intCast_def [Ring k] [MulOneClass G] (z : ℤ) :
    (z : MonoidAlgebra k G) = single (1 : G) (z : k) :=
  rfl

Integer Scalar Embedding in Monoid Algebra: $z = \text{single}(1_G, z)$

Informal description

For any ring $k$ and any multiplicative monoid $G$, the integer scalar $z \in \mathbb{Z}$ in the monoid algebra $k[G]$ is equal to the element $\text{single}(1_G, z)$, where $1_G$ is the identity element of $G$ and $z$ is interpreted as an element of $k$ via the canonical integer embedding.

MonoidAlgebra.ring instance

[Ring k] [Monoid G] : Ring (MonoidAlgebra k G)

Full source

instance ring [Ring k] [Monoid G] : Ring (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonAssocRing, MonoidAlgebra.semiring with }

Ring Structure on Monoid Algebra

Informal description

For any ring $k$ and monoid $G$, the monoid algebra $k[G]$ forms a ring under the convolution product. This means it has: - An addition operation $+$ forming an additive commutative group - A multiplication operation $*$ (convolution product) that is associative and distributes over addition - A zero element that is absorbing for multiplication - A multiplicative identity element (given by the function that maps the identity of $G$ to $1_k$ and all other elements to $0_k$)

MonoidAlgebra.nonUnitalCommRing instance

[CommRing k] [CommSemigroup G] : NonUnitalCommRing (MonoidAlgebra k G)

Full source

instance nonUnitalCommRing [CommRing k] [CommSemigroup G] :
    NonUnitalCommRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommSemiring, MonoidAlgebra.nonUnitalRing with }

Non-unital Commutative Ring Structure on Monoid Algebra of a Commutative Semigroup

Informal description

For any commutative ring $k$ and commutative semigroup $G$, the monoid algebra $k[G]$ forms a non-unital commutative ring under pointwise addition and the convolution product. This means it has: - An additive commutative group structure - A commutative and associative multiplication operation that distributes over addition - A zero element that is absorbing for multiplication without requiring a multiplicative identity.

MonoidAlgebra.commRing instance

[CommRing k] [CommMonoid G] : CommRing (MonoidAlgebra k G)

Full source

instance commRing [CommRing k] [CommMonoid G] : CommRing (MonoidAlgebra k G) :=
  { MonoidAlgebra.nonUnitalCommRing, MonoidAlgebra.ring with }

Commutative Ring Structure on Monoid Algebra of a Commutative Monoid

Informal description

For any commutative ring $k$ and commutative monoid $G$, the monoid algebra $k[G]$ forms a commutative ring under the convolution product. This means it has: - An addition operation $+$ forming an additive commutative group - A commutative and associative multiplication operation $*$ (convolution product) that distributes over addition - A zero element that is absorbing for multiplication - A multiplicative identity element (given by the function that maps the identity of $G$ to $1_k$ and all other elements to $0_k$)

MonoidAlgebra.smulZeroClass instance

[Semiring k] [SMulZeroClass R k] : SMulZeroClass R (MonoidAlgebra k G)

Full source

instance smulZeroClass [Semiring k] [SMulZeroClass R k] : SMulZeroClass R (MonoidAlgebra k G) :=
  Finsupp.smulZeroClass

Scalar Multiplication Preserving Zero on Monoid Algebras

Informal description

For any semiring $k$ and any type $R$ with a scalar multiplication action on $k$ that preserves zero (i.e., $r \cdot 0 = 0$ for all $r \in R$), the monoid algebra $k[G]$ inherits a scalar multiplication action from $R$ that also preserves zero. This action is defined pointwise: $(r \cdot f)(g) = r \cdot f(g)$ for any $f \in k[G]$ and $g \in G$.

MonoidAlgebra.noZeroSMulDivisors instance

[Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] : NoZeroSMulDivisors R (MonoidAlgebra k G)

Full source

instance noZeroSMulDivisors [Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] :
    NoZeroSMulDivisors R (MonoidAlgebra k G) :=
  Finsupp.noZeroSMulDivisors

No Zero Divisors in Scalar Multiplication of Monoid Algebras

Informal description

For any semiring $k$ and monoid $G$, if $R$ is a type with a zero element and a scalar multiplication action on $k$ that preserves zero, and if $R$ and $k$ have no zero divisors with respect to scalar multiplication (i.e., $r \cdot a = 0$ implies $r = 0$ or $a = 0$ for all $r \in R$ and $a \in k$), then the monoid algebra $k[G]$ also has no zero divisors with respect to the pointwise scalar multiplication from $R$.

MonoidAlgebra.distribSMul instance

[Semiring k] [DistribSMul R k] : DistribSMul R (MonoidAlgebra k G)

Full source

instance distribSMul [Semiring k] [DistribSMul R k] : DistribSMul R (MonoidAlgebra k G) :=
  Finsupp.distribSMul _ _

Distributive Scalar Multiplication on Monoid Algebras

Informal description

For any semiring $k$ and any monoid $G$, the monoid algebra $k[G]$ inherits a distributive scalar multiplication structure from $k$. That is, for any type $R$ with a distributive scalar multiplication action on $k$, the action extends pointwise to $k[G]$, satisfying $r \cdot (f + g) = r \cdot f + r \cdot g$ for all $r \in R$ and $f, g \in k[G]$.

MonoidAlgebra.distribMulAction instance

[Monoid R] [Semiring k] [DistribMulAction R k] : DistribMulAction R (MonoidAlgebra k G)

Full source

instance distribMulAction [Monoid R] [Semiring k] [DistribMulAction R k] :
    DistribMulAction R (MonoidAlgebra k G) :=
  Finsupp.distribMulAction G k

Distributive Multiplicative Action on Monoid Algebras

Informal description

For any monoid $R$ and semiring $k$ equipped with a distributive multiplicative action of $R$ on $k$, the monoid algebra $k[G]$ inherits a distributive multiplicative action from $R$. This action is defined pointwise, meaning that for any $r \in R$ and $f \in k[G]$, the action $(r \cdot f)(g) = r \cdot f(g)$ holds for all $g \in G$.

MonoidAlgebra.module instance

[Semiring R] [Semiring k] [Module R k] : Module R (MonoidAlgebra k G)

Full source

instance module [Semiring R] [Semiring k] [Module R k] : Module R (MonoidAlgebra k G) :=
  Finsupp.module G k

Module Structure on Monoid Algebras

Informal description

For any semiring $R$ and any semiring $k$ equipped with a module structure over $R$, the monoid algebra $k[G]$ forms a module over $R$ with pointwise scalar multiplication. That is, for any $r \in R$ and $f \in k[G]$, the scalar multiplication $(r \cdot f)(g) = r \cdot f(g)$ holds for all $g \in G$.

MonoidAlgebra.faithfulSMul instance

[Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] : FaithfulSMul R (MonoidAlgebra k G)

Full source

instance faithfulSMul [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
    FaithfulSMul R (MonoidAlgebra k G) :=
  Finsupp.faithfulSMul

Faithfulness of Scalar Multiplication on Monoid Algebras

Informal description

For any semiring $k$ and any type $R$ with a scalar multiplication action on $k$ that preserves zero, if the action of $R$ on $k$ is faithful (i.e., distinct elements of $R$ act differently on some element of $k$) and the monoid $G$ is nonempty, then the induced pointwise scalar multiplication action of $R$ on the monoid algebra $k[G]$ is also faithful.

MonoidAlgebra.isScalarTower instance

 [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] :
  IsScalarTower R S (MonoidAlgebra k G)

Full source

instance isScalarTower [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S]
    [IsScalarTower R S k] : IsScalarTower R S (MonoidAlgebra k G) :=
  Finsupp.isScalarTower G k

Scalar Tower Property for Monoid Algebras

Informal description

For any semiring $k$ and types $R$, $S$ with scalar multiplication actions on $k$ that preserve zero, if $R$ and $S$ form a scalar tower over $k$ (i.e., $(r \cdot s) \cdot m = r \cdot (s \cdot m)$ for all $r \in R$, $s \in S$, $m \in k$), then the monoid algebra $k[G]$ also forms a scalar tower with respect to the pointwise scalar multiplication.

MonoidAlgebra.smulCommClass instance

[Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] : SMulCommClass R S (MonoidAlgebra k G)

Full source

instance smulCommClass [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
    SMulCommClass R S (MonoidAlgebra k G) :=
  Finsupp.smulCommClass G k

Commutativity of Scalar Multiplication on Monoid Algebras

Informal description

For any semiring $k$ and any types $R$ and $S$ with scalar multiplication actions on $k$ that preserve zero, if the actions of $R$ and $S$ on $k$ commute, then the pointwise scalar multiplication actions of $R$ and $S$ on the monoid algebra $k[G]$ also commute. That is, for any $r \in R$, $s \in S$, and $f \in k[G]$, we have $r \cdot (s \cdot f) = s \cdot (r \cdot f)$.

MonoidAlgebra.isCentralScalar instance

 [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k] [IsCentralScalar R k] : IsCentralScalar R (MonoidAlgebra k G)

Full source

instance isCentralScalar [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k]
    [IsCentralScalar R k] : IsCentralScalar R (MonoidAlgebra k G) :=
  Finsupp.isCentralScalar G k

Central Scalar Property of Monoid Algebras

Informal description

For a semiring $k$ and a monoid $G$, if $R$ has a scalar multiplication action on $k$ that preserves zero and the actions of $R$ and its multiplicative opposite $R^\text{op}$ on $k$ coincide, then the monoid algebra $k[G]$ inherits this central scalar property. That is, for any $r \in R$ and $f \in k[G]$, the left and right scalar multiplications $r \cdot f$ and $f \cdot r$ (via $R^\text{op}$) are equal.

MonoidAlgebra.comapDistribMulActionSelf definition

[Group G] [Semiring k] : DistribMulAction G (MonoidAlgebra k G)

Full source

/-- This is not an instance as it conflicts with `MonoidAlgebra.distribMulAction` when `G = kˣ`.
-/
def comapDistribMulActionSelf [Group G] [Semiring k] : DistribMulAction G (MonoidAlgebra k G) :=
  Finsupp.comapDistribMulAction

Distributive multiplicative action of a group on its monoid algebra via domain action

Informal description

For a group $G$ and a semiring $k$, the monoid algebra $k[G]$ carries a distributive multiplicative action of $G$, where the action is defined by mapping the domain of finitely supported functions under the group action. Specifically, for any $g \in G$ and $f \in k[G]$, the action satisfies: 1. $g \cdot 0 = 0$ (preservation of zero) 2. $g \cdot (f_1 + f_2) = g \cdot f_1 + g \cdot f_2$ (distributivity over addition) This action is implemented by mapping the domain of $f$ under the left multiplication action of $G$ on itself.

MonoidAlgebra.smul_single theorem

[Semiring k] [SMulZeroClass R k] (a : G) (c : R) (b : k) : c • single a b = single a (c • b)

Full source

@[simp]
theorem smul_single [Semiring k] [SMulZeroClass R k] (a : G) (c : R) (b : k) :
    c • single a b = single a (c • b) :=
  Finsupp.smul_single _ _ _

Scalar multiplication commutes with single generator in monoid algebra: $c \cdot \text{single}(a, b) = \text{single}(a, c \cdot b)$

Informal description

Let $k$ be a semiring and $G$ a monoid. For any scalar $c$ in a type $R$ with a scalar multiplication action on $k$ that preserves zero, and for any elements $a \in G$ and $b \in k$, the scalar multiplication of $c$ with the monoid algebra element $\text{single}(a, b)$ is equal to $\text{single}(a, c \cdot b)$. In mathematical notation: $$c \cdot \text{single}(a, b) = \text{single}(a, c \cdot b).$$

MonoidAlgebra.ext theorem

[Semiring k] ⦃f g : MonoidAlgebra k G⦄ (H : ∀ (x : G), f x = g x) : f = g

Full source

/-- A copy of `Finsupp.ext` for `MonoidAlgebra`. -/
@[ext]
theorem ext [Semiring k] ⦃f g : MonoidAlgebra k G⦄ (H : ∀ (x : G), f x = g x) :
    f = g :=
  Finsupp.ext H

Extensionality for Monoid Algebra Elements

Informal description

For any semiring $k$ and any monoid $G$, if two elements $f, g$ of the monoid algebra $k[G]$ satisfy $f(x) = g(x)$ for all $x \in G$, then $f = g$.

MonoidAlgebra.singleAddHom abbrev

[Semiring k] (a : G) : k →+ MonoidAlgebra k G

Full source

/-- A copy of `Finsupp.singleAddHom` for `MonoidAlgebra`. -/
abbrev singleAddHom [Semiring k] (a : G) : k →+ MonoidAlgebra k G := Finsupp.singleAddHom a

Additive monoid homomorphism from coefficients to monoid algebra via single element

Informal description

For a semiring $k$ and a monoid $G$, the function $\operatorname{singleAddHom}(a) \colon k \to k[G]$ is an additive monoid homomorphism that maps each $b \in k$ to the monoid algebra element $\operatorname{single}(a, b)$, where $\operatorname{single}(a, b)$ is the element of the monoid algebra $k[G]$ that has coefficient $b$ at $a$ and zero elsewhere. More precisely, the homomorphism satisfies: 1. $\operatorname{singleAddHom}(a)(0) = \operatorname{single}(a, 0)$, and 2. $\operatorname{singleAddHom}(a)(b_1 + b_2) = \operatorname{singleAddHom}(a)(b_1) + \operatorname{singleAddHom}(a)(b_2)$ for all $b_1, b_2 \in k$.

MonoidAlgebra.singleAddHom_apply theorem

[Semiring k] (a : G) (b : k) : singleAddHom a b = single a b

Full source

@[simp] lemma singleAddHom_apply [Semiring k] (a : G) (b : k) :
  singleAddHom a b = single a b := rfl

Evaluation of the Single Generator Homomorphism in Monoid Algebra

Informal description

For a semiring $k$ and a monoid $G$, the additive monoid homomorphism $\operatorname{singleAddHom}(a) \colon k \to k[G]$ satisfies $\operatorname{singleAddHom}(a)(b) = \operatorname{single}(a, b)$ for all $b \in k$, where $\operatorname{single}(a, b)$ is the element of the monoid algebra $k[G]$ with coefficient $b$ at $a$ and zero elsewhere.

MonoidAlgebra.addHom_ext' theorem

 {N : Type*} [Semiring k] [AddZeroClass N] ⦃f g : MonoidAlgebra k G →+ N⦄
  (H : ∀ (x : G), AddMonoidHom.comp f (singleAddHom x) = AddMonoidHom.comp g (singleAddHom x)) : f = g

Full source

/-- A copy of `Finsupp.addHom_ext'` for `MonoidAlgebra`. -/
@[ext high]
theorem addHom_ext' {N : Type*} [Semiring k] [AddZeroClass N]
    ⦃f g : MonoidAlgebraMonoidAlgebra k G →+ N⦄
    (H : ∀ (x : G), AddMonoidHom.comp f (singleAddHom x) = AddMonoidHom.comp g (singleAddHom x)) :
    f = g :=
  Finsupp.addHom_ext' H

Extensionality of Additive Homomorphisms on Monoid Algebras via Single Elements

Informal description

Let $k$ be a semiring, $G$ a monoid, and $N$ an add-zero class. For any two additive monoid homomorphisms $f, g \colon k[G] \to^+ N$, if for every $x \in G$ the compositions $f \circ \operatorname{singleAddHom}(x)$ and $g \circ \operatorname{singleAddHom}(x)$ are equal, then $f = g$.

MonoidAlgebra.distribMulActionHom_ext' theorem

 {N : Type*} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k]
  {f g : MonoidAlgebra k G →+[R] N}
  (h : ∀ a : G, f.comp (DistribMulActionHom.single (M := k) a) = g.comp (DistribMulActionHom.single a)) : f = g

Full source

/-- A copy of `Finsupp.distribMulActionHom_ext'` for `MonoidAlgebra`. -/
@[ext]
theorem distribMulActionHom_ext' {N : Type*} [Monoid R] [Semiring k] [AddMonoid N]
    [DistribMulAction R N] [DistribMulAction R k]
    {f g : MonoidAlgebraMonoidAlgebra k G →+[R] N}
    (h : ∀ a : G,
      f.comp (DistribMulActionHom.single (M := k) a) = g.comp (DistribMulActionHom.single a)) :
    f = g :=
  Finsupp.distribMulActionHom_ext' h

Extensionality of Equivariant Additive Monoid Homomorphisms on Monoid Algebras via Single Generators

Informal description

Let $R$ be a monoid, $k$ a semiring, and $N$ an additive monoid equipped with a distributive multiplicative action of $R$. For any two equivariant additive monoid homomorphisms $f, g \colon k[G] \to N$ (where $k[G]$ is the monoid algebra over $k$ generated by $G$), if for every $a \in G$ the compositions $f \circ \operatorname{single}(a)$ and $g \circ \operatorname{single}(a)$ are equal (where $\operatorname{single}(a) \colon k \to k[G]$ is the single generator homomorphism), then $f = g$.

MonoidAlgebra.lsingle abbrev

[Semiring R] [Semiring k] [Module R k] (a : G) : k →ₗ[R] MonoidAlgebra k G

Full source

/-- A copy of `Finsupp.lsingle` for `MonoidAlgebra`. -/
abbrev lsingle [Semiring R] [Semiring k] [Module R k] (a : G) :
    k →ₗ[R] MonoidAlgebra k G := Finsupp.lsingle a

Linear Single-Point Embedding in Monoid Algebra

Informal description

For a semiring $R$, a semiring $k$ equipped with an $R$-module structure, and an element $a \in G$, the linear map $\operatorname{lsingle}(a) \colon k \to R[G]$ sends each $b \in k$ to the monoid algebra element that takes the value $b$ at $a$ and zero elsewhere. This map is linear with respect to the $R$-module structures on $k$ and $R[G]$.

MonoidAlgebra.lsingle_apply theorem

[Semiring R] [Semiring k] [Module R k] (a : G) (b : k) : lsingle (R := R) a b = single a b

Full source

@[simp]
lemma lsingle_apply [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
    lsingle (R := R) a b = single a b :=
  rfl

Equality of Linear Single-Point Embedding and Single Generator in Monoid Algebra

Informal description

Let $R$ be a semiring, $k$ a semiring equipped with an $R$-module structure, and $G$ a monoid. For any element $a \in G$ and $b \in k$, the linear single-point embedding $\operatorname{lsingle}(a)(b)$ in the monoid algebra $k[G]$ equals the single generator element $\operatorname{single}(a, b)$. In other words, the following equality holds: $$\operatorname{lsingle}(a)(b) = \operatorname{single}(a, b)$$ where $\operatorname{single}(a, b)$ is the element of $k[G]$ that takes value $b$ at $a$ and zero elsewhere.

MonoidAlgebra.lhom_ext' theorem

 {N : Type*} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] ⦃f g : MonoidAlgebra k G →ₗ[R] N⦄
  (H : ∀ (x : G), LinearMap.comp f (lsingle x) = LinearMap.comp g (lsingle x)) : f = g

Full source

/-- A copy of `Finsupp.lhom_ext'` for `MonoidAlgebra`. -/
@[ext high]
lemma lhom_ext' {N : Type*} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k]
    ⦃f g : MonoidAlgebraMonoidAlgebra k G →ₗ[R] N⦄
    (H : ∀ (x : G), LinearMap.comp f (lsingle x) = LinearMap.comp g (lsingle x)) :
    f = g :=
  Finsupp.lhom_ext' H

Extensionality of Linear Maps on Monoid Algebras via Single Embeddings

Informal description

Let $R$ be a semiring, $k$ a semiring equipped with an $R$-module structure, and $N$ an $R$-module. For any two $R$-linear maps $f, g \colon k[G] \to N$ from the monoid algebra $k[G]$ to $N$, if for every $x \in G$ the compositions $f \circ \operatorname{lsingle}(x)$ and $g \circ \operatorname{lsingle}(x)$ are equal as linear maps from $k$ to $N$, then $f = g$.

MonoidAlgebra.mul_apply theorem

 [DecidableEq G] [Mul G] (f g : MonoidAlgebra k G) (x : G) :
  (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0

Full source

theorem mul_apply [DecidableEq G] [Mul G] (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0 := by
  -- Porting note: `reducible` cannot be `local` so proof gets long.
  rw [mul_def, Finsupp.sum_apply]; congr; ext
  rw [Finsupp.sum_apply]; congr; ext
  apply single_apply

Evaluation of Product in Monoid Algebra via Double Sum

Informal description

Let $G$ be a multiplicative monoid with a decidable equality, and let $k$ be a semiring. For any two elements $f, g$ in the monoid algebra $k[G]$ and any $x \in G$, the evaluation of the product $f * g$ at $x$ is given by: $$(f * g)(x) = \sum_{a_1 \in G} \sum_{a_2 \in G} \begin{cases} f(a_1) \cdot g(a_2) & \text{if } a_1 \cdot a_2 = x \\ 0 & \text{otherwise} \end{cases}$$

MonoidAlgebra.mul_apply_antidiagonal theorem

 [Mul G] (f g : MonoidAlgebra k G) (x : G) (s : Finset (G × G)) (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 * p.2 = x) :
  (f * g) x = ∑ p ∈ s, f p.1 * g p.2

Full source

theorem mul_apply_antidiagonal [Mul G] (f g : MonoidAlgebra k G) (x : G) (s : Finset (G × G))
    (hs : ∀ {p : G × G}, p ∈ sp ∈ s ↔ p.1 * p.2 = x) : (f * g) x = ∑ p ∈ s, f p.1 * g p.2 := by
  classical exact
      let F : G × G → k := fun p => if p.1 * p.2 = x then f p.1 * g p.2 else 0
      calc
        (f * g) x = ∑ a₁ ∈ f.support, ∑ a₂ ∈ g.support, F (a₁, a₂) := mul_apply f g x
        _ = ∑ p ∈ f.support ×ˢ g.support, F p := by rw [Finset.sum_product]
        _ = ∑ p ∈ f.support ×ˢ g.support with p.1 * p.2 = x, f p.1 * g p.2 :=
          (Finset.sum_filter _ _).symm
        _ = ∑ p ∈ s with p.1 ∈ f.support ∧ p.2 ∈ g.support, f p.1 * g p.2 := by
          congr! 1; ext; simp only [mem_filter, mem_product, hs, and_comm]
        _ = ∑ p ∈ s, f p.1 * g p.2 :=
          sum_subset (filter_subset _ _) fun p hps hp => by
            simp only [mem_filter, mem_support_iff, not_and, Classical.not_not] at hp ⊢
            by_cases h1 : f p.1 = 0
            · rw [h1, zero_mul]
            · rw [hp hps h1, mul_zero]

Evaluation of Monoid Algebra Product via Antidiagonal Sum

Informal description

Let $G$ be a multiplicative monoid and $k$ a semiring. For any two elements $f, g$ in the monoid algebra $k[G]$ and any $x \in G$, if $s$ is a finite subset of $G \times G$ such that for any pair $(a_1, a_2) \in G \times G$, $(a_1, a_2) \in s$ if and only if $a_1 \cdot a_2 = x$, then the evaluation of the product $f * g$ at $x$ is given by: $$(f * g)(x) = \sum_{(a_1, a_2) \in s} f(a_1) \cdot g(a_2).$$

MonoidAlgebra.single_mul_single theorem

[Mul G] {a₁ a₂ : G} {b₁ b₂ : k} : single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂)

Full source

@[simp]
theorem single_mul_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} :
    single a₁ b₁ * single a₂ b₂ = single (a₁ * a₂) (b₁ * b₂) := by
  rw [mul_def]
  exact (sum_single_index (by simp only [zero_mul, single_zero, sum_zero])).trans
    (sum_single_index (by rw [mul_zero, single_zero]))

Product of Single Generators in Monoid Algebra: $\text{single}(a_1, b_1) * \text{single}(a_2, b_2) = \text{single}(a_1 a_2, b_1 b_2)$

Informal description

Let $G$ be a multiplicative monoid and $k$ a semiring. For any elements $a_1, a_2 \in G$ and coefficients $b_1, b_2 \in k$, the product of the single generators $\text{single}(a_1, b_1)$ and $\text{single}(a_2, b_2)$ in the monoid algebra $k[G]$ is given by: $$\text{single}(a_1, b_1) * \text{single}(a_2, b_2) = \text{single}(a_1 \cdot a_2, b_1 \cdot b_2).$$

MonoidAlgebra.single_commute_single theorem

 [Mul G] {a₁ a₂ : G} {b₁ b₂ : k} (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) : Commute (single a₁ b₁) (single a₂ b₂)

Full source

theorem single_commute_single [Mul G] {a₁ a₂ : G} {b₁ b₂ : k}
    (ha : Commute a₁ a₂) (hb : Commute b₁ b₂) :
    Commute (single a₁ b₁) (single a₂ b₂) :=
  single_mul_single.trans <| congr_arg₂ single ha hb |>.trans single_mul_single.symm

Commutation of Single Generators in Monoid Algebra under Commuting Conditions

Informal description

Let $G$ be a multiplicative monoid and $k$ a semiring. For any elements $a_1, a_2 \in G$ and coefficients $b_1, b_2 \in k$, if $a_1$ and $a_2$ commute in $G$ (i.e., $a_1 a_2 = a_2 a_1$) and $b_1$ and $b_2$ commute in $k$ (i.e., $b_1 b_2 = b_2 b_1$), then the single generators $\text{single}(a_1, b_1)$ and $\text{single}(a_2, b_2)$ commute in the monoid algebra $k[G]$.

MonoidAlgebra.single_commute theorem

 [Mul G] {a : G} {b : k} (ha : ∀ a', Commute a a') (hb : ∀ b', Commute b b') :
  ∀ f : MonoidAlgebra k G, Commute (single a b) f

Full source

theorem single_commute [Mul G] {a : G} {b : k} (ha : ∀ a', Commute a a') (hb : ∀ b', Commute b b') :
    ∀ f : MonoidAlgebra k G, Commute (single a b) f :=
  suffices AddMonoidHom.mulLeft (single a b) = AddMonoidHom.mulRight (single a b) from
    DFunLike.congr_fun this
  addHom_ext' fun a' => AddMonoidHom.ext fun b' => single_commute_single (ha a') (hb b')

Universal Commutation of Central Single Generator in Monoid Algebra

Informal description

Let $G$ be a multiplicative monoid and $k$ a semiring. For any element $a \in G$ that commutes with every element of $G$ (i.e., $a a' = a' a$ for all $a' \in G$) and any coefficient $b \in k$ that commutes with every element of $k$ (i.e., $b b' = b' b$ for all $b' \in k$), the single generator $\text{single}(a, b)$ commutes with every element $f$ of the monoid algebra $k[G]$.

MonoidAlgebra.single_pow theorem

[Monoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (a ^ n) (b ^ n)

Full source

@[simp]
theorem single_pow [Monoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (a ^ n) (b ^ n)
  | 0 => by
    simp only [pow_zero]
    rfl
  | n + 1 => by simp only [pow_succ, single_pow n, single_mul_single]

Power of Single Generator in Monoid Algebra: $\text{single}(a, b)^n = \text{single}(a^n, b^n)$

Informal description

Let $G$ be a monoid and $k$ a semiring. For any element $a \in G$, coefficient $b \in k$, and natural number $n$, the $n$-th power of the single generator $\text{single}(a, b)$ in the monoid algebra $k[G]$ is given by: $$\text{single}(a, b)^n = \text{single}(a^n, b^n).$$

MonoidAlgebra.ofMagma definition

[Mul G] : G →ₙ* MonoidAlgebra k G

Full source

/-- The embedding of a magma into its magma algebra. -/
@[simps]
def ofMagma [Mul G] : G →ₙ* MonoidAlgebra k G where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]

Magma embedding into its monoid algebra

Informal description

The function embeds a magma $G$ into its monoid algebra $k[G]$ by mapping each element $a \in G$ to the element $\text{single}(a, 1)$ in $k[G]$, where $\text{single}(a, 1)$ is the finitely supported function that takes the value $1$ at $a$ and $0$ elsewhere. This embedding preserves the magma structure, meaning that for any $a, b \in G$, the image of the product $a \cdot b$ is equal to the convolution product of the images of $a$ and $b$ in $k[G]$.

MonoidAlgebra.of definition

[MulOneClass G] : G →* MonoidAlgebra k G

Full source

/-- The embedding of a unital magma into its magma algebra. -/
@[simps]
def of [MulOneClass G] : G →* MonoidAlgebra k G :=
  { ofMagma k G with
    toFun := fun a => single a 1
    map_one' := rfl }

Embedding of a unital magma into its monoid algebra

Informal description

The function embeds a unital magma $G$ into its monoid algebra $k[G]$ by mapping each element $a \in G$ to the element $\text{single}(a, 1)$ in $k[G]$, where $\text{single}(a, 1)$ is the finitely supported function that takes the value $1$ at $a$ and $0$ elsewhere. This embedding preserves both the multiplicative structure and the identity element, meaning that for any $a, b \in G$, the image of the product $a \cdot b$ is equal to the convolution product of the images of $a$ and $b$ in $k[G]$, and the image of the identity element $1_G$ is the multiplicative identity in $k[G]$.

MonoidAlgebra.smul_single' theorem

(c : k) (a : G) (b : k) : c • single a b = single a (c * b)

Full source

/-- Copy of `Finsupp.smul_single'` that avoids the `MonoidAlgebra = Finsupp` defeq abuse. -/
theorem smul_single' (c : k) (a : G) (b : k) : c • single a b = single a (c * b) :=
  Finsupp.smul_single' c a b

Scalar Multiplication Commutes with Single Generator in Monoid Algebra: $c \cdot \text{single}(a, b) = \text{single}(a, c \cdot b)$

Informal description

For any elements $c, b$ in a semiring $k$ and any element $a$ in a monoid $G$, the scalar multiplication $c \cdot \text{single}(a, b)$ in the monoid algebra $k[G]$ is equal to $\text{single}(a, c \cdot b)$. In mathematical notation: $$c \cdot \text{single}(a, b) = \text{single}(a, c \cdot b).$$

MonoidAlgebra.smul_of theorem

[MulOneClass G] (g : G) (r : k) : r • of k G g = single g r

Full source

theorem smul_of [MulOneClass G] (g : G) (r : k) : r • of k G g = single g r := by
  simp

Scalar multiplication of embedded monoid elements in monoid algebra: $r \cdot \iota(g) = \text{single}(g, r)$

Informal description

Let $k$ be a semiring and $G$ a monoid with multiplicative identity. For any element $g \in G$ and scalar $r \in k$, the scalar multiple $r \cdot \iota(g)$ in the monoid algebra $k[G]$ equals the single generator $\text{single}(g, r)$, where $\iota: G \to k[G]$ is the canonical embedding that sends $g$ to $\text{single}(g, 1)$. In mathematical notation: $$r \cdot \iota(g) = \text{single}(g, r)$$ where $\iota(g) = \text{single}(g, 1)$ is the image of $g$ under the canonical embedding.

MonoidAlgebra.of_injective theorem

[MulOneClass G] [Nontrivial k] : Function.Injective (of k G)

Full source

theorem of_injective [MulOneClass G] [Nontrivial k] :
    Function.Injective (of k G) := fun a b h => by
  simpa using (single_eq_single_iff _ _ _ _).mp h

Injectivity of the Canonical Embedding into Monoid Algebra

Informal description

Let $k$ be a nontrivial semiring and $G$ a unital magma (i.e., a set with multiplication and identity element). The canonical embedding $\text{of} \colon G \to k[G]$, which maps each $g \in G$ to the element $\text{single}(g,1)$ in the monoid algebra $k[G]$, is injective.

MonoidAlgebra.of_commute theorem

[MulOneClass G] {a : G} (h : ∀ a', Commute a a') (f : MonoidAlgebra k G) : Commute (of k G a) f

Full source

theorem of_commute [MulOneClass G] {a : G} (h : ∀ a', Commute a a') (f : MonoidAlgebra k G) :
    Commute (of k G a) f :=
  single_commute h Commute.one_left f

Central Elements Embed into Center of Monoid Algebra

Informal description

Let $G$ be a monoid with identity and $k$ a semiring. For any element $a \in G$ that commutes with every element of $G$ (i.e., $a a' = a' a$ for all $a' \in G$), the image $\iota(a)$ of $a$ under the canonical embedding $\iota \colon G \to k[G]$ commutes with every element $f$ of the monoid algebra $k[G]$. Here $\iota(a) = \text{single}(a,1)$ is the element of $k[G]$ that takes value $1$ at $a$ and $0$ elsewhere.

MonoidAlgebra.singleHom definition

[MulOneClass G] : k × G →* MonoidAlgebra k G

Full source

/-- `Finsupp.single` as a `MonoidHom` from the product type into the monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`Finsupp.single`.
-/
@[simps]
def singleHom [MulOneClass G] : k × Gk × G →* MonoidAlgebra k G where
  toFun a := single a.2 a.1
  map_one' := rfl
  map_mul' _a _b := single_mul_single.symm

Monoid homomorphism embedding pairs into monoid algebra

Informal description

The function $\text{singleHom}$ maps a pair $(r, g)$ from $k \times G$ to the monoid algebra $k[G]$ as the finitely supported function $\text{single}(g, r)$, which has value $r$ at $g$ and zero elsewhere. This function is a monoid homomorphism, meaning it preserves the multiplicative identity and the multiplication operation. Specifically: - The multiplicative identity $(1_k, 1_G)$ is mapped to $\text{single}(1_G, 1_k)$, the multiplicative identity in $k[G]$. - The product of two pairs $(r_1, g_1) \cdot (r_2, g_2) = (r_1 r_2, g_1 g_2)$ is mapped to the convolution product $\text{single}(g_1 g_2, r_1 r_2)$ in $k[G]$.

MonoidAlgebra.mul_single_apply_aux theorem

 [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ a ∈ f.support, a * x = z ↔ a = y) :
  (f * single x r) z = f y * r

Full source

theorem mul_single_apply_aux [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G}
    (H : ∀ a ∈ f.support, a * x = z ↔ a = y) : (f * single x r) z = f y * r := by
  classical exact
    calc
      (f * single x r) z
      _ = sum f fun a b => ite (a * x = z) (b * r) 0 :=
        (mul_apply _ _ _).trans <| Finsupp.sum_congr fun _ _ => sum_single_index (by simp)

      _ = f.sum fun a b => ite (a = y) (b * r) 0 := Finsupp.sum_congr fun x hx => by
        simp only [H _ hx]
      _ = if y ∈ f.support then f y * r else 0 := f.support.sum_ite_eq' _ _
      _ = _ := by split_ifs with h <;> simp at h <;> simp [h]

Evaluation of Monoid Algebra Product at a Point via Single Generator

Informal description

Let $G$ be a multiplicative monoid and $k$ a semiring. Given an element $f \in k[G]$, coefficients $r \in k$, and elements $x, y, z \in G$, suppose that for every $a$ in the support of $f$, the equation $a \cdot x = z$ holds if and only if $a = y$. Then the evaluation of the convolution product $f * \text{single}(x, r)$ at $z$ is equal to $f(y) \cdot r$, i.e., $$(f * \text{single}(x, r))(z) = f(y) \cdot r.$$

MonoidAlgebra.mul_single_one_apply theorem

 [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
  (HMul.hMul (β := MonoidAlgebra k G) f (single 1 r)) x = f x * r

Full source

theorem mul_single_one_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (HMul.hMul (β := MonoidAlgebra k G) f (single 1 r)) x = f x * r :=
  f.mul_single_apply_aux fun a ha => by rw [mul_one]

Evaluation of Monoid Algebra Product with Identity Generator

Informal description

Let $G$ be a multiplicative monoid with identity element $1$, $k$ a semiring, and $f \in k[G]$ an element of the monoid algebra. For any coefficient $r \in k$ and any element $x \in G$, the evaluation of the convolution product $f * \text{single}(1, r)$ at $x$ is equal to $f(x) \cdot r$, i.e., $$(f * \text{single}(1, r))(x) = f(x) \cdot r.$$

MonoidAlgebra.mul_single_apply_of_not_exists_mul theorem

[Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G) (h : ¬∃ d, g' = d * g) : (x * single g r) g' = 0

Full source

theorem mul_single_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
    (h : ¬∃ d, g' = d * g) : (x * single g r) g' = 0 := by
  classical
    rw [mul_apply, Finsupp.sum_comm, Finsupp.sum_single_index]
    swap
    · simp_rw [Finsupp.sum, mul_zero, ite_self, Finset.sum_const_zero]
    · apply Finset.sum_eq_zero
      simp_rw [ite_eq_right_iff]
      rintro g'' _hg'' rfl
      exfalso
      exact h ⟨_, rfl⟩

Vanishing of Monoid Algebra Product When No Multiplicative Factor Exists

Informal description

Let $G$ be a multiplicative monoid and $k$ a semiring. For any $r \in k$, $g, g' \in G$, and $x \in k[G]$, if there does not exist $d \in G$ such that $g' = d \cdot g$, then the evaluation of the product $x * \text{single}(g, r)$ at $g'$ is zero, i.e., $(x * \text{single}(g, r))(g') = 0$.

MonoidAlgebra.single_mul_apply_aux theorem

 [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G} (H : ∀ a ∈ f.support, x * a = y ↔ a = z) :
  (single x r * f) y = r * f z

Full source

theorem single_mul_apply_aux [Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G}
    (H : ∀ a ∈ f.support, x * a = y ↔ a = z) : (single x r * f) y = r * f z := by
  classical exact
      have : (f.sum fun a b => ite (x * a = y) (0 * b) 0) = 0 := by simp
      calc
        (single x r * f) y
        _ = sum f fun a b => ite (x * a = y) (r * b) 0 :=
          (mul_apply _ _ _).trans <| sum_single_index this
        _ = f.sum fun a b => ite (a = z) (r * b) 0 := Finsupp.sum_congr fun x hx => by
          simp only [H _ hx]
        _ = if z ∈ f.support then r * f z else 0 := f.support.sum_ite_eq' _ _
        _ = _ := by split_ifs with h <;> simp at h <;> simp [h]

Evaluation of Convolution Product with Single Generator under Multiplicative Condition

Informal description

Let $G$ be a multiplicative monoid and $k$ a semiring. For any element $f \in k[G]$, coefficients $r \in k$, elements $x, y, z \in G$, and a hypothesis $H$ stating that for all $a$ in the support of $f$, the equation $x \cdot a = y$ holds if and only if $a = z$, we have: $$(\text{single}(x, r) * f)(y) = r \cdot f(z)$$ where $\text{single}(x, r)$ is the element of the monoid algebra $k[G]$ that takes value $r$ at $x$ and zero elsewhere, and $*$ denotes the convolution product in $k[G]$.

MonoidAlgebra.single_one_mul_apply theorem

[MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) : (single (1 : G) r * f) x = r * f x

Full source

theorem single_one_mul_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (single (1 : G) r * f) x = r * f x :=
  f.single_mul_apply_aux fun a ha => by rw [one_mul]

Evaluation of Convolution with Identity Element: $\text{single}(1, r) * f = r \cdot f$

Informal description

Let $G$ be a monoid with identity element $1$, $k$ a semiring, and $f \in k[G]$ an element of the monoid algebra. For any coefficient $r \in k$ and any element $x \in G$, the evaluation of the convolution product $\text{single}(1, r) * f$ at $x$ satisfies: $$(\text{single}(1, r) * f)(x) = r \cdot f(x)$$ where $\text{single}(1, r)$ is the element of $k[G]$ that takes value $r$ at $1$ and zero elsewhere.

MonoidAlgebra.single_mul_apply_of_not_exists_mul theorem

[Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G) (h : ¬∃ d, g' = g * d) : (single g r * x) g' = 0

Full source

theorem single_mul_apply_of_not_exists_mul [Mul G] (r : k) {g g' : G} (x : MonoidAlgebra k G)
    (h : ¬∃ d, g' = g * d) : (single g r * x) g' = 0 := by
  classical
    rw [mul_apply, Finsupp.sum_single_index]
    swap
    · simp_rw [Finsupp.sum, zero_mul, ite_self, Finset.sum_const_zero]
    · apply Finset.sum_eq_zero
      simp_rw [ite_eq_right_iff]
      rintro g'' _hg'' rfl
      exfalso
      exact h ⟨_, rfl⟩

Vanishing of convolution product when no multiplicative relation exists

Informal description

Let $G$ be a multiplicative monoid, $k$ a semiring, and $r \in k$. For any elements $g, g' \in G$ and any $x \in k[G]$, if there does not exist $d \in G$ such that $g' = g \cdot d$, then the evaluation of the product $\text{single}(g, r) * x$ at $g'$ is zero: $$(\text{single}(g, r) * x)(g') = 0$$ where $\text{single}(g, r)$ is the element of the monoid algebra $k[G]$ that takes value $r$ at $g$ and zero elsewhere, and $*$ denotes the convolution product in $k[G]$.

MonoidAlgebra.liftNC_smul theorem

 [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g : G →* R) (c : k) (φ : MonoidAlgebra k G) :
  liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ

Full source

theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g : G →* R) (c : k)
    (φ : MonoidAlgebra k G) : liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ := by
  suffices (liftNC (↑f) g).comp (smulAddHom k (MonoidAlgebra k G) c) =
      (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g) from
    DFunLike.congr_fun this φ
  ext
  simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
    AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]

Linearity of lifted homomorphism with respect to scalar multiplication in monoid algebra

Informal description

Let $k$ be a semiring, $G$ a monoid, and $R$ a semiring. Given a ring homomorphism $f \colon k \to R$ and a monoid homomorphism $g \colon G \to R$, for any scalar $c \in k$ and any element $\varphi \in k[G]$, the lifted homomorphism $\operatorname{liftNC}(f, g)$ satisfies: \[ \operatorname{liftNC}(f, g)(c \cdot \varphi) = f(c) \cdot \operatorname{liftNC}(f, g)(\varphi) \] where $\operatorname{liftNC}(f, g)$ is the additive homomorphism from $k[G]$ to $R$ defined by linearly extending the map $\text{single}(a, b) \mapsto f(b) \cdot g(a)$.

MonoidAlgebra.isScalarTower_self instance

[IsScalarTower R k k] : IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G)

Full source

instance isScalarTower_self [IsScalarTower R k k] :
    IsScalarTower R (MonoidAlgebra k G) (MonoidAlgebra k G) where
  smul_assoc t a b := by
    ext
    -- Porting note: `refine` & `rw` are required because `simp` behaves differently.
    classical
    simp only [smul_eq_mul, mul_apply]
    rw [coe_smul]
    refine Eq.trans (sum_smul_index' (g := a) (b := t) ?_) ?_ <;>
      simp only [mul_apply, Finsupp.smul_sum, smul_ite, smul_mul_assoc,
        zero_mul, ite_self, imp_true_iff, sum_zero, Pi.smul_apply, smul_zero]

Scalar Multiplication Tower Property for Monoid Algebras

Informal description

For any semiring $k$, monoid $G$, and type $R$ with a scalar multiplication action on $k$ that satisfies the tower property (i.e., $(r \cdot s) \cdot t = r \cdot (s \cdot t)$ for all $r \in R$, $s, t \in k$), the monoid algebra $k[G]$ inherits the scalar multiplication tower property from $k$. That is, for any $r \in R$ and $f, g \in k[G]$, we have $(r \cdot f) * g = r \cdot (f * g)$, where $*$ denotes the convolution product in $k[G]$.

MonoidAlgebra.smulCommClass_self instance

[SMulCommClass R k k] : SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G)

Full source

/-- Note that if `k` is a `CommSemiring` then we have `SMulCommClass k k k` and so we can take
`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication. -/
instance smulCommClass_self [SMulCommClass R k k] :
    SMulCommClass R (MonoidAlgebra k G) (MonoidAlgebra k G) where
  smul_comm t a b := by
    ext
    -- Porting note: `refine` & `rw` are required because `simp` behaves differently.
    classical
    simp only [smul_eq_mul, mul_apply]
    rw [coe_smul]
    refine Eq.symm (Eq.trans (congr_arg (sum a)
      (funext₂ fun a₁ b₁ => sum_smul_index' (g := b) (b := t) ?_)) ?_) <;>
    simp only [mul_apply, Finsupp.sum, Finset.smul_sum, smul_ite, mul_smul_comm,
      imp_true_iff, ite_eq_right_iff, Pi.smul_apply, mul_zero, smul_zero]

Commutativity of Scalar Multiplication with Monoid Algebra Multiplication

Informal description

For any semiring $k$, monoid $G$, and type $R$ such that the scalar multiplications by $R$ and $k$ on $k$ commute, the scalar multiplications by $R$ and the monoid algebra $k[G]$ on $k[G]$ also commute. That is, for any $r \in R$, $f \in k[G]$, and $g \in G$, we have: $$ r \cdot (f * g) = f * (r \cdot g). $$

MonoidAlgebra.smulCommClass_symm_self instance

[SMulCommClass k R k] : SMulCommClass (MonoidAlgebra k G) R (MonoidAlgebra k G)

Full source

instance smulCommClass_symm_self [SMulCommClass k R k] :
    SMulCommClass (MonoidAlgebra k G) R (MonoidAlgebra k G) :=
  ⟨fun t a b => by
    haveI := SMulCommClass.symm k R k
    rw [← smul_comm]⟩

Symmetry of Commuting Scalar Actions in Monoid Algebras

Informal description

For any semiring $k$, monoid $G$, and type $R$ such that the scalar multiplications by $k$ and $R$ on $k$ commute, the scalar multiplications by the monoid algebra $k[G]$ and $R$ on $k[G]$ also commute. That is, for any $f \in k[G]$, $r \in R$, and $g \in G$, we have: $$ f * (r \cdot g) = r \cdot (f * g). $$

MonoidAlgebra.single_one_comm theorem

[CommSemiring k] [MulOneClass G] (r : k) (f : MonoidAlgebra k G) : single (1 : G) r * f = f * single (1 : G) r

Full source

theorem single_one_comm [CommSemiring k] [MulOneClass G] (r : k) (f : MonoidAlgebra k G) :
    single (1 : G) r * f = f * single (1 : G) r :=
  single_commute Commute.one_left (Commute.all _) f

Commutativity of Identity-Based Single Generator in Monoid Algebra

Informal description

Let $k$ be a commutative semiring and $G$ a monoid. For any element $r \in k$ and any element $f$ of the monoid algebra $k[G]$, the convolution product of the single generator $\text{single}(1_G, r)$ (where $1_G$ is the identity of $G$) with $f$ commutes with $f$, i.e., $$\text{single}(1_G, r) * f = f * \text{single}(1_G, r).$$

MonoidAlgebra.singleOneRingHom definition

[Semiring k] [MulOneClass G] : k →+* MonoidAlgebra k G

Full source

/-- `Finsupp.single 1` as a `RingHom` -/
@[simps]
def singleOneRingHom [Semiring k] [MulOneClass G] : k →+* MonoidAlgebra k G :=
  { singleAddHom 1 with
    toFun := single 1
    map_one' := rfl
    map_mul' := fun x y => by simp }

Ring homomorphism embedding coefficients into monoid algebra via identity element

Informal description

The ring homomorphism $\text{singleOneRingHom} \colon k \to k[G]$ from a semiring $k$ to the monoid algebra $k[G]$ maps each element $b \in k$ to the monoid algebra element $\text{single}(1_G, b)$, where $1_G$ is the multiplicative identity of $G$. This homomorphism satisfies: 1. $\text{singleOneRingHom}(1_k) = \text{single}(1_G, 1_k)$ (preservation of multiplicative identity) 2. $\text{singleOneRingHom}(b_1 \cdot b_2) = \text{singleOneRingHom}(b_1) \cdot \text{singleOneRingHom}(b_2)$ (preservation of multiplication) 3. $\text{singleOneRingHom}(b_1 + b_2) = \text{singleOneRingHom}(b_1) + \text{singleOneRingHom}(b_2)$ (preservation of addition) 4. $\text{singleOneRingHom}(0_k) = \text{single}(1_G, 0_k)$ (preservation of zero)

MonoidAlgebra.ringHom_ext theorem

 {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R}
  (h₁ : ∀ b, f (single 1 b) = g (single 1 b)) (h_of : ∀ a, f (single a 1) = g (single a 1)) : f = g

Full source

/-- If two ring homomorphisms from `MonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal. -/
theorem ringHom_ext {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebraMonoidAlgebra k G →+* R}
    (h₁ : ∀ b, f (single 1 b) = g (single 1 b)) (h_of : ∀ a, f (single a 1) = g (single a 1)) :
    f = g :=
  RingHom.coe_addMonoidHom_injective <|
    addHom_ext fun a b => by
      rw [← single, ← one_mul a, ← mul_one b, ← single_mul_single]
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      erw [AddMonoidHom.coe_coe f, AddMonoidHom.coe_coe g]; rw [f.map_mul, g.map_mul, h₁, h_of]

Extensionality of Ring Homomorphisms on Monoid Algebra Generators

Informal description

Let $k$ be a semiring, $G$ a multiplicative monoid, and $R$ a semiring. For any two ring homomorphisms $f, g \colon k[G] \to R$, if: 1. $f(\text{single}(1_G, b)) = g(\text{single}(1_G, b))$ for all $b \in k$, and 2. $f(\text{single}(a, 1_k)) = g(\text{single}(a, 1_k))$ for all $a \in G$, then $f = g$.

MonoidAlgebra.ringHom_ext' theorem

 {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebra k G →+* R}
  (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom)
  (h_of : (f : MonoidAlgebra k G →* R).comp (of k G) = (g : MonoidAlgebra k G →* R).comp (of k G)) : f = g

Full source

/-- If two ring homomorphisms from `MonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' {R} [Semiring k] [MulOneClass G] [Semiring R] {f g : MonoidAlgebraMonoidAlgebra k G →+* R}
    (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom)
    (h_of :
      (f : MonoidAlgebraMonoidAlgebra k G →* R).comp (of k G) = (g : MonoidAlgebraMonoidAlgebra k G →* R).comp (of k G)) :
    f = g :=
  ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)

Extensionality of Ring Homomorphisms on Monoid Algebra via Coefficient and Generator Embeddings

Informal description

Let $k$ be a semiring, $G$ a multiplicative monoid, and $R$ a semiring. For any two ring homomorphisms $f, g \colon k[G] \to R$, if: 1. The compositions of $f$ and $g$ with the coefficient embedding $\text{singleOneRingHom} \colon k \to k[G]$ are equal, and 2. The compositions of $f$ and $g$ (as monoid homomorphisms) with the generator embedding $\text{of} \colon G \to k[G]$ are equal, then $f = g$.

MonoidAlgebra.induction_on theorem

 [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G) (hM : ∀ g, p (of k G g))
  (hadd : ∀ f g : MonoidAlgebra k G, p f → p g → p (f + g)) (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f

Full source

theorem induction_on [Semiring k] [Monoid G] {p : MonoidAlgebra k G → Prop} (f : MonoidAlgebra k G)
    (hM : ∀ g, p (of k G g)) (hadd : ∀ f g : MonoidAlgebra k G, p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f := by
  refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_
  · simpa using hsmul 0 (of k G 1) (hM 1)
  · convert hsmul r (of k G g) (hM g)
    simp

Induction Principle for Monoid Algebras

Informal description

Let $k$ be a semiring and $G$ a monoid. For any predicate $p$ on the monoid algebra $k[G]$, if the following conditions hold: 1. For every $g \in G$, $p$ holds for the image of $g$ under the canonical embedding $\text{of} \colon G \to k[G]$. 2. For any $f, g \in k[G]$, if $p(f)$ and $p(g)$ hold, then $p(f + g)$ holds. 3. For any $r \in k$ and $f \in k[G]$, if $p(f)$ holds, then $p(r \cdot f)$ holds, then $p(f)$ holds for all $f \in k[G]$.

MonoidAlgebra.prod_single theorem

 [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
  (∏ i ∈ s, single (a i) (b i)) = single (∏ i ∈ s, a i) (∏ i ∈ s, b i)

Full source

theorem prod_single [CommSemiring k] [CommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
    (∏ i ∈ s, single (a i) (b i)) = single (∏ i ∈ s, a i) (∏ i ∈ s, b i) :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons has, ih, single_mul_single, prod_cons has, prod_cons has]

Product of Single Generators in Monoid Algebra: $\prod_i \text{single}(a_i, b_i) = \text{single}(\prod_i a_i, \prod_i b_i)$

Informal description

Let $k$ be a commutative semiring and $G$ a commutative monoid. For any finite set $s$ indexed by $\iota$, and functions $a \colon \iota \to G$ and $b \colon \iota \to k$, the product of single generators in the monoid algebra $k[G]$ satisfies: $$\prod_{i \in s} \text{single}(a_i, b_i) = \text{single}\left(\prod_{i \in s} a_i, \prod_{i \in s} b_i\right),$$ where the left product is taken in $k[G]$ and the right products are taken in $G$ and $k$ respectively.

MonoidAlgebra.mul_single_apply theorem

(f : MonoidAlgebra k G) (r : k) (x y : G) : (f * single x r) y = f (y * x⁻¹) * r

Full source

@[simp]
theorem mul_single_apply (f : MonoidAlgebra k G) (r : k) (x y : G) :
    (f * single x r) y = f (y * x⁻¹) * r :=
  f.mul_single_apply_aux fun _a _ => eq_mul_inv_iff_mul_eq.symm

Evaluation of Convolution Product with Single Generator in Monoid Algebra: $(f * \text{single}(x, r))(y) = f(y \cdot x^{-1}) \cdot r$

Informal description

Let $k$ be a semiring and $G$ a group. For any element $f$ in the monoid algebra $k[G]$, any coefficient $r \in k$, and any elements $x, y \in G$, the evaluation of the convolution product $f * \text{single}(x, r)$ at $y$ is given by: $$(f * \text{single}(x, r))(y) = f(y \cdot x^{-1}) \cdot r.$$

MonoidAlgebra.single_mul_apply theorem

(r : k) (x : G) (f : MonoidAlgebra k G) (y : G) : (single x r * f) y = r * f (x⁻¹ * y)

Full source

@[simp]
theorem single_mul_apply (r : k) (x : G) (f : MonoidAlgebra k G) (y : G) :
    (single x r * f) y = r * f (x⁻¹ * y) :=
  f.single_mul_apply_aux fun _z _ => eq_inv_mul_iff_mul_eq.symm

Evaluation of Convolution Product with Single Generator: $(\text{single}(x, r) * f)(y) = r \cdot f(x^{-1}y)$

Informal description

Let $G$ be a group, $k$ a semiring, and $k[G]$ the monoid algebra of $G$ over $k$. For any coefficient $r \in k$, group elements $x, y \in G$, and element $f \in k[G]$, the evaluation of the convolution product $\text{single}(x, r) * f$ at $y$ is given by: $$(\text{single}(x, r) * f)(y) = r \cdot f(x^{-1} \cdot y)$$ where $\text{single}(x, r)$ denotes the element of $k[G]$ that takes value $r$ at $x$ and zero elsewhere, and $*$ denotes the convolution product in $k[G]$.

MonoidAlgebra.mul_apply_left theorem

(f g : MonoidAlgebra k G) (x : G) : (f * g) x = f.sum fun a b => b * g (a⁻¹ * x)

Full source

theorem mul_apply_left (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = f.sum fun a b => b * g (a⁻¹ * x) :=
  calc
    (f * g) x = sum f fun a b => (single a b * g) x := by
      rw [← Finsupp.sum_apply, ← Finsupp.sum_mul g f, f.sum_single]
    _ = _ := by simp only [single_mul_apply, Finsupp.sum]

Left Convolution Formula in Monoid Algebra: $(f * g)(x) = \sum_a f(a) \cdot g(a^{-1}x)$

Informal description

Let $k$ be a semiring and $G$ a group. For any two elements $f, g$ in the monoid algebra $k[G]$ and any $x \in G$, the evaluation of their convolution product $f * g$ at $x$ is given by: $$(f * g)(x) = \sum_{a \in G} f(a) \cdot g(a^{-1} \cdot x)$$ where the sum is taken over the support of $f$.

MonoidAlgebra.mul_apply_right theorem

(f g : MonoidAlgebra k G) (x : G) : (f * g) x = g.sum fun a b => f (x * a⁻¹) * b

Full source

theorem mul_apply_right (f g : MonoidAlgebra k G) (x : G) :
    (f * g) x = g.sum fun a b => f (x * a⁻¹) * b :=
  calc
    (f * g) x = sum g fun a b => (f * single a b) x := by
      rw [← Finsupp.sum_apply, ← Finsupp.mul_sum f g, g.sum_single]
    _ = _ := by simp only [mul_single_apply, Finsupp.sum]

Right Convolution Formula in Monoid Algebra: $(f * g)(x) = \sum_{a} f(x \cdot a^{-1}) \cdot g(a)$

Informal description

Let $k$ be a semiring and $G$ a group. For any two elements $f, g$ in the monoid algebra $k[G]$ and any $x \in G$, the evaluation of their convolution product $f * g$ at $x$ is given by: $$(f * g)(x) = \sum_{a \in \operatorname{supp}(g)} f(x \cdot a^{-1}) \cdot g(a)$$ where the sum is taken over the support of $g$.

MonoidAlgebra.opRingEquiv definition

[Monoid G] : (MonoidAlgebra k G)ᵐᵒᵖ ≃+* MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ

Full source

/-- The opposite of a `MonoidAlgebra R I` equivalent as a ring to
the `MonoidAlgebra Rᵐᵒᵖ Iᵐᵒᵖ` over the opposite ring, taking elements to their opposite. -/
@[simps! +simpRhs apply symm_apply]
protected noncomputable def opRingEquiv [Monoid G] :
    (MonoidAlgebra k G)ᵐᵒᵖ(MonoidAlgebra k G)ᵐᵒᵖ ≃+* MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ :=
  { opAddEquiv.symm.trans <|
      (Finsupp.mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ)).trans <| Finsupp.domCongr opEquiv with
    map_mul' := by
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      rw [Equiv.toFun_as_coe, AddEquiv.toEquiv_eq_coe]; erw [AddEquiv.coe_toEquiv]
      rw [← AddEquiv.coe_toAddMonoidHom]
      refine Iff.mpr (AddMonoidHom.map_mul_iff (R := (MonoidAlgebra k G)ᵐᵒᵖ)
        (S := MonoidAlgebra kᵐᵒᵖ Gᵐᵒᵖ) _) ?_
      ext
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      simp only [AddMonoidHom.coe_comp, AddEquiv.coe_toAddMonoidHom, opAddEquiv_apply,
        Function.comp_apply, singleAddHom_apply, AddMonoidHom.compr₂_apply, AddMonoidHom.coe_mul,
        AddMonoidHom.coe_mulLeft, AddMonoidHom.compl₂_apply]
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644
      erw [AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply, AddEquiv.trans_apply,
        AddEquiv.trans_apply, AddEquiv.trans_apply, MulOpposite.opAddEquiv_symm_apply]
      rw [MulOpposite.unop_mul (α := MonoidAlgebra k G), unop_op, unop_op, single_mul_single]
      simp }

Ring equivalence between opposite monoid algebra and monoid algebra over opposites

Informal description

The ring equivalence between the opposite of the monoid algebra $k[G]^\text{op}$ and the monoid algebra over the opposite ring $k^\text{op}$ and opposite monoid $G^\text{op}$, denoted $k^\text{op}[G^\text{op}]$. This equivalence maps an element $f \in k[G]^\text{op}$ to the element in $k^\text{op}[G^\text{op}]$ obtained by applying the opposite operation to both the coefficients and the monoid elements.

MonoidAlgebra.opRingEquiv_single theorem

[Monoid G] (r : k) (x : G) : MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r)

Full source

theorem opRingEquiv_single [Monoid G] (r : k) (x : G) :
    MonoidAlgebra.opRingEquiv (op (single x r)) = single (op x) (op r) := by simp

Ring Equivalence Preserves Single Elements: $\text{opRingEquiv}(\text{op}(\text{single}(x, r))) = \text{single}(\text{op}(x), \text{op}(r))$

Informal description

Let $G$ be a monoid and $k$ a semiring. For any element $x \in G$ and $r \in k$, the ring equivalence between the opposite monoid algebra $(k[G])^\text{op}$ and the monoid algebra $k^\text{op}[G^\text{op}]$ maps the element $\text{op}(\text{single}(x, r))$ to $\text{single}(\text{op}(x), \text{op}(r))$. In other words, the canonical ring isomorphism satisfies: $$\text{opRingEquiv}(\text{op}(\text{single}(x, r))) = \text{single}(\text{op}(x), \text{op}(r))$$ where: - $\text{single}(x, r)$ is the element of $k[G]$ with value $r$ at $x$ and zero elsewhere - $\text{op}$ denotes the canonical map to the opposite structure - $\text{opRingEquiv}$ is the ring equivalence between $(k[G])^\text{op}$ and $k^\text{op}[G^\text{op}]$

MonoidAlgebra.opRingEquiv_symm_single theorem

[Monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) : MonoidAlgebra.opRingEquiv.symm (single x r) = op (single x.unop r.unop)

Full source

theorem opRingEquiv_symm_single [Monoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
    MonoidAlgebra.opRingEquiv.symm (single x r) = op (single x.unop r.unop) := by simp

Inverse Ring Equivalence Preserves Single Elements in Opposite Monoid Algebra: $\text{opRingEquiv}^{-1}(\text{single}(x, r)) = \text{op}(\text{single}(x^\text{unop}, r^\text{unop}))$

Informal description

Let $G$ be a monoid and $k$ a semiring. For any element $x$ in the multiplicative opposite $G^\text{op}$ and any coefficient $r$ in the opposite semiring $k^\text{op}$, the inverse of the ring equivalence between $(k[G])^\text{op}$ and $k^\text{op}[G^\text{op}]$ maps the single generator element $\text{single}(x, r) \in k^\text{op}[G^\text{op}]$ to $\text{op}(\text{single}(x^\text{unop}, r^\text{unop})) \in (k[G])^\text{op}$. In mathematical notation: $$\text{opRingEquiv}^{-1}(\text{single}(x, r)) = \text{op}(\text{single}(x^\text{unop}, r^\text{unop}))$$ where: - $\text{single}(x, r)$ is the element of $k^\text{op}[G^\text{op}]$ with value $r$ at $x$ and zero elsewhere - $\text{op}$ denotes the canonical map to the opposite structure - $x^\text{unop}$ and $r^\text{unop}$ are the original elements in $G$ and $k$ respectively - $\text{opRingEquiv}^{-1}$ is the inverse of the ring equivalence between $(k[G])^\text{op}$ and $k^\text{op}[G^\text{op}]$

MonoidAlgebra.submoduleOfSMulMem definition

(W : Submodule k V) (h : ∀ (g : G) (v : V), v ∈ W → of k G g • v ∈ W) : Submodule (MonoidAlgebra k G) V

Full source

/-- A submodule over `k` which is stable under scalar multiplication by elements of `G` is a
submodule over `MonoidAlgebra k G` -/
def submoduleOfSMulMem (W : Submodule k V) (h : ∀ (g : G) (v : V), v ∈ W → ofof k G g • v ∈ W) :
    Submodule (MonoidAlgebra k G) V where
  carrier := W
  zero_mem' := W.zero_mem'
  add_mem' := W.add_mem'
  smul_mem' := by
    intro f v hv
    rw [← Finsupp.sum_single f, Finsupp.sum, Finset.sum_smul]
    simp_rw [← smul_of, smul_assoc]
    exact Submodule.sum_smul_mem W _ fun g _ => h g v hv

Submodule stable under monoid algebra action

Informal description

Given a submodule $W$ of a $k$-module $V$ that is stable under scalar multiplication by elements of $G$ (i.e., for any $g \in G$ and $v \in W$, the scalar product $g \cdot v$ remains in $W$), then $W$ forms a submodule over the monoid algebra $k[G]$. More precisely, the submodule $W$ inherits the structure of a $k[G]$-submodule, where the scalar multiplication by elements of $k[G]$ is defined via the convolution product. The stability condition ensures that the action of $k[G]$ on $W$ is well-defined.

MonoidAlgebra.isLocalHom_singleOneRingHom instance

[Semiring k] [Monoid G] : IsLocalHom (singleOneRingHom (k := k) (G := G))

Full source

instance isLocalHom_singleOneRingHom [Semiring k] [Monoid G] :
    IsLocalHom (singleOneRingHom (k := k) (G := G)) where
  map_nonunit x hx := by
    obtain ⟨⟨x, xi, hx, hxi⟩, rfl⟩ := hx
    simp_rw [MonoidAlgebra.ext_iff, singleOneRingHom_apply] at hx hxi ⊢
    specialize hx 1
    specialize hxi 1
    classical
    simp_rw [single_one_mul_apply, one_def, single_apply, if_pos] at hx
    simp_rw [mul_single_one_apply, one_def, single_apply, if_pos] at hxi
    exact ⟨⟨x, xi 1, hx, hxi⟩, rfl⟩

The embedding $k \to k[G]$ via the identity element is a local homomorphism

Informal description

For any semiring $k$ and monoid $G$, the ring homomorphism $\text{singleOneRingHom} \colon k \to k[G]$ that maps $b \in k$ to $\text{single}(1_G, b) \in k[G]$ is a local homomorphism. That is, for any $b \in k$, if $\text{single}(1_G, b)$ is a unit in $k[G]$, then $b$ is a unit in $k$.

AddMonoidAlgebra definition

Full source

/-- The monoid algebra over a semiring `k` generated by the additive monoid `G`, denoted by `k[G]`.
It is the type of finite formal `k`-linear combinations of terms of `G`,
endowed with the convolution product.
-/
def AddMonoidAlgebra :=
  G →₀ k

Additive monoid algebra

Informal description

The additive monoid algebra over a semiring $k$ generated by the additive monoid $G$, denoted by $k[G]$, is the type of finite formal $k$-linear combinations of elements of $G$, endowed with the convolution product. More precisely, it consists of finitely supported functions from $G$ to $k$ (i.e., functions that are zero everywhere except on a finite subset of $G$), where the multiplication is given by the convolution product: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.term_[_] definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
scoped[AddMonoidAlgebra] notation:9000 R:max "[" A "]" => AddMonoidAlgebra R A

Notation for additive monoid algebra

Informal description

The notation `R[A]` represents the additive monoid algebra of `A` over `R`, where `R` is a semiring and `A` is an additive monoid. This is defined as the type of finitely supported functions from `A` to `R` with a convolution product.

AddMonoidAlgebra.inhabited instance

: Inhabited k[G]

Full source

instance inhabited : Inhabited k[G] :=
  inferInstanceAs (Inhabited (G →₀ k))

Inhabitedness of Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ is inhabited, meaning there exists at least one element in $k[G]$.

AddMonoidAlgebra.addCommMonoid instance

: AddCommMonoid k[G]

Full source

instance addCommMonoid : AddCommMonoid k[G] :=
  inferInstanceAs (AddCommMonoid (G →₀ k))

Additive Commutative Monoid Structure on Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ forms an additive commutative monoid under pointwise addition. That is, for any semiring $k$ and additive monoid $G$, the set of finitely supported functions from $G$ to $k$ is equipped with a commutative addition operation where $(f + g)(a) = f(a) + g(a)$ for all $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.instIsCancelAdd instance

[IsCancelAdd k] : IsCancelAdd (AddMonoidAlgebra k G)

Full source

instance instIsCancelAdd [IsCancelAdd k] : IsCancelAdd (AddMonoidAlgebra k G) :=
  inferInstanceAs (IsCancelAdd (G →₀ k))

Cancellative Addition in Additive Monoid Algebra

Informal description

For any semiring $k$ with a cancellative addition and any additive monoid $G$, the additive monoid algebra $k[G]$ inherits a cancellative addition operation. That is, for any $f, g, h \in k[G]$, if $f + h = g + h$ or $h + f = h + g$, then $f = g$.

AddMonoidAlgebra.coeFun instance

: CoeFun k[G] fun _ => G → k

Full source

instance coeFun : CoeFun k[G] fun _ => G → k :=
  inferInstanceAs (CoeFun (G →₀ k) _)

Function-Like Structure on Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ can be treated as a function from $G$ to $k$, where $k[G]$ is the type of finitely supported functions from $G$ to $k$.

AddMonoidAlgebra.single abbrev

(a : G) (b : k) : k[G]

Full source

abbrev single (a : G) (b : k) : k[G] := Finsupp.single a b

Single generator in additive monoid algebra

Informal description

For an additive monoid $G$ and a semiring $k$, the function $\text{single}(a, b)$ constructs an element of the additive monoid algebra $k[G]$ that is zero everywhere except at $a \in G$, where it takes the value $b \in k$. More precisely, $\text{single}(a, b)$ is the finitely supported function from $G$ to $k$ defined by: \[ \text{single}(a, b)(x) = \begin{cases} b & \text{if } x = a, \\ 0 & \text{otherwise.} \end{cases} \]

AddMonoidAlgebra.single_zero theorem

(a : G) : (single a 0 : k[G]) = 0

Full source

theorem single_zero (a : G) : (single a 0 : k[G]) = 0 := Finsupp.single_zero a

Zero Element in Additive Monoid Algebra via Single Generator

Informal description

For any element $a$ in an additive monoid $G$ and any semiring $k$, the element $\text{single}(a, 0)$ in the additive monoid algebra $k[G]$ is equal to the zero function. That is, the finitely supported function that is zero everywhere (including at $a$) is equal to the additive identity in $k[G]$.

AddMonoidAlgebra.single_add theorem

(a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂

Full source

theorem single_add (a : G) (b₁ b₂ : k) : single a (b₁ + b₂) = single a b₁ + single a b₂ :=
  Finsupp.single_add a b₁ b₂

Additivity of Single Generator in Additive Monoid Algebra

Informal description

For any element $a$ in an additive monoid $G$ and any elements $b_1, b_2$ in a semiring $k$, the single generator function in the additive monoid algebra $k[G]$ satisfies: \[ \text{single}(a, b_1 + b_2) = \text{single}(a, b_1) + \text{single}(a, b_2). \]

AddMonoidAlgebra.sum_single_index theorem

{N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N} (h_zero : h a 0 = 0) : (single a b).sum h = h a b

Full source

@[simp]
theorem sum_single_index {N} [AddCommMonoid N] {a : G} {b : k} {h : G → k → N}
    (h_zero : h a 0 = 0) :
    (single a b).sum h = h a b := Finsupp.sum_single_index h_zero

Sum of Single Generator in Additive Monoid Algebra

Informal description

Let $G$ be an additive monoid, $k$ a semiring, and $N$ an additive commutative monoid. For any element $a \in G$, any $b \in k$, and any function $h : G \to k \to N$ satisfying $h(a, 0) = 0$, the sum of the single generator $\text{single}(a, b)$ over $h$ equals $h(a, b)$. That is, \[ \sum_{x \in G} \text{single}(a, b)(x) \cdot h(x) = h(a, b). \]

AddMonoidAlgebra.sum_single theorem

(f : k[G]) : f.sum single = f

Full source

@[simp]
theorem sum_single (f : k[G]) : f.sum single = f :=
  Finsupp.sum_single f

Sum of Single Generators Equals Original Function in Additive Monoid Algebra

Informal description

For any element $f$ in the additive monoid algebra $k[G]$, the sum over the support of $f$ of the single-point functions $\operatorname{single}(a, f(a))$ equals $f$ itself. That is, \[ \sum_{a \in \operatorname{supp}(f)} \operatorname{single}(a, f(a)) = f. \]

AddMonoidAlgebra.single_apply theorem

{a a' : G} {b : k} [Decidable (a = a')] : single a b a' = if a = a' then b else 0

Full source

theorem single_apply {a a' : G} {b : k} [Decidable (a = a')] :
    single a b a' = if a = a' then b else 0 :=
  Finsupp.single_apply

Evaluation of Single Generator in Additive Monoid Algebra

Informal description

For any elements $a, a'$ in an additive monoid $G$ and any element $b$ in a semiring $k$, the evaluation of the single generator $\text{single}(a, b)$ at $a'$ is given by: \[ \text{single}(a, b)(a') = \begin{cases} b & \text{if } a = a', \\ 0 & \text{otherwise.} \end{cases} \]

AddMonoidAlgebra.single_eq_zero theorem

{a : G} {b : k} : single a b = 0 ↔ b = 0

Full source

@[simp]
theorem single_eq_zero {a : G} {b : k} : singlesingle a b = 0 ↔ b = 0 := Finsupp.single_eq_zero

Zero Condition for Single Generator in Additive Monoid Algebra

Informal description

For any element $a$ in an additive monoid $G$ and any element $b$ in a semiring $k$, the single generator $\text{single}(a, b)$ in the additive monoid algebra $k[G]$ is equal to the zero function if and only if $b$ is equal to zero in $k$. In mathematical notation: $$\text{single}(a, b) = 0 \leftrightarrow b = 0$$

AddMonoidAlgebra.single_ne_zero theorem

{a : G} {b : k} : single a b ≠ 0 ↔ b ≠ 0

Full source

theorem single_ne_zero {a : G} {b : k} : singlesingle a b ≠ 0single a b ≠ 0 ↔ b ≠ 0 := Finsupp.single_ne_zero

Nonzero Condition for Single Generator in Additive Monoid Algebra

Informal description

For any element $a$ in an additive monoid $G$ and any element $b$ in a semiring $k$, the single generator $\text{single}(a, b)$ in the additive monoid algebra $k[G]$ is nonzero if and only if $b$ is nonzero. In mathematical notation: $$\text{single}(a, b) \neq 0 \leftrightarrow b \neq 0$$

AddMonoidAlgebra.liftNC definition

(f : k →+ R) (g : Multiplicative G → R) : k[G] →+ R

Full source

/-- A non-commutative version of `AddMonoidAlgebra.lift`: given an additive homomorphism
`f : k →+ R` and a map `g : Multiplicative G → R`, returns the additive
homomorphism from `k[G]` such that `liftNC f g (single a b) = f b * g a`. If `f`
is a ring homomorphism and the range of either `f` or `g` is in center of `R`, then the result is a
ring homomorphism.  If `R` is a `k`-algebra and `f = algebraMap k R`, then the result is an algebra
homomorphism called `AddMonoidAlgebra.lift`. -/
def liftNC (f : k →+ R) (g : Multiplicative G → R) : k[G]k[G] →+ R :=
  liftAddHom fun x : G => (AddMonoidHom.mulRight (g <| Multiplicative.ofAdd x)).comp f

Non-commutative lift for additive monoid algebra

Informal description

Given an additive homomorphism $f \colon k \to^+ R$ and a map $g \colon \text{Multiplicative}\,G \to R$, the function $\text{liftNC}\,f\,g \colon k[G] \to^+ R$ is the additive homomorphism from the additive monoid algebra $k[G]$ to $R$ defined by: $$\text{liftNC}\,f\,g\,(\text{single}\,a\,b) = f(b) \cdot g(\text{ofAdd}\,a)$$ for all $a \in G$ and $b \in k$. If $f$ is a ring homomorphism and the range of either $f$ or $g$ lies in the center of $R$, then $\text{liftNC}\,f\,g$ is a ring homomorphism. When $R$ is a $k$-algebra and $f$ is the algebra map $k \to R$, this construction yields an algebra homomorphism called $\text{AddMonoidAlgebra.lift}$.

AddMonoidAlgebra.liftNC_single theorem

 (f : k →+ R) (g : Multiplicative G → R) (a : G) (b : k) : liftNC f g (single a b) = f b * g (Multiplicative.ofAdd a)

Full source

@[simp]
theorem liftNC_single (f : k →+ R) (g : Multiplicative G → R) (a : G) (b : k) :
    liftNC f g (single a b) = f b * g (Multiplicative.ofAdd a) :=
  liftAddHom_apply_single _ _ _

Evaluation of Non-Commutative Lift on Single Generator in Additive Monoid Algebra

Informal description

For any additive monoid homomorphism $f \colon k \to^+ R$, any map $g \colon \text{Multiplicative}\,G \to R$, any element $a \in G$, and any element $b \in k$, the non-commutative lift $\text{liftNC}\,f\,g$ evaluated at the single generator $\text{single}(a, b)$ satisfies: \[ \text{liftNC}\,f\,g\,(\text{single}(a, b)) = f(b) \cdot g(\text{ofAdd}(a)) \] where $\text{ofAdd} \colon G \to \text{Multiplicative}\,G$ is the canonical embedding.

AddMonoidAlgebra.hasMul instance

: Mul k[G]

Full source

/-- The product of `f g : k[G]` is the finitely supported function
  whose value at `a` is the sum of `f x * g y` over all pairs `x, y`
  such that `x + y = a`. (Think of the product of multivariate
  polynomials where `α` is the additive monoid of monomial exponents.) -/
instance hasMul : Mul k[G] :=
  ⟨fun f g => MonoidAlgebra.mul' (G := Multiplicative G) f g⟩

Multiplication in Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ over a semiring $k$ generated by an additive monoid $G$ is equipped with a multiplication operation defined by convolution: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.mul_def theorem

{f g : k[G]} :
    f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ + a₂) (b₁ * b₂)

Full source

theorem mul_def {f g : k[G]} :
    f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => single (a₁ + a₂) (b₁ * b₂) :=
  MonoidAlgebra.mul_def (G := Multiplicative G)

Definition of Convolution Product in Additive Monoid Algebra

Informal description

For any two elements $f, g$ in the additive monoid algebra $k[G]$, their product $f * g$ is given by the double sum $$ f * g = \sum_{a_1 \in G} \sum_{a_2 \in G} \text{single}(a_1 + a_2, f(a_1) \cdot g(a_2)) $$ where $\text{single}(a, b)$ denotes the element of $k[G]$ that has value $b$ at $a$ and zero elsewhere.

AddMonoidAlgebra.nonUnitalNonAssocSemiring instance

: NonUnitalNonAssocSemiring k[G]

Full source

instance nonUnitalNonAssocSemiring : NonUnitalNonAssocSemiring k[G] :=
  { Finsupp.instAddCommMonoid with
    -- Porting note: `refine` & `exact` are required because `simp` behaves differently.
    left_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_add_index ?_ ?_)) ?_ <;>
        simp only [mul_add, mul_zero, single_zero, single_add, forall_true_iff, sum_add]
    right_distrib := fun f g h => by
      haveI := Classical.decEq G
      simp only [mul_def]
      refine Eq.trans (sum_add_index ?_ ?_) ?_ <;>
        simp only [add_mul, zero_mul, single_zero, single_add, forall_true_iff, sum_zero, sum_add]
    zero_mul := fun f => by
      simp only [mul_def]
      exact sum_zero_index
    mul_zero := fun f => by
      simp only [mul_def]
      exact Eq.trans (congr_arg (sum f) (funext₂ fun a₁ b₁ => sum_zero_index)) sum_zero
    nsmul := fun n f => n • f
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` → `refine Finsupp.ext fun _ => ?_`
    nsmul_zero := by
      intros
      refine Finsupp.ext fun _ => ?_
      simp [-nsmul_eq_mul, add_smul]
    nsmul_succ := by
      intros
      refine Finsupp.ext fun _ => ?_
      simp [-nsmul_eq_mul, add_smul] }

Non-unital Non-associative Semiring Structure on Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ over a semiring $k$ generated by an additive monoid $G$ forms a non-unital, non-associative semiring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative monoid 2. A multiplication operation (convolution product) that distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.liftNC_mul theorem

{g_hom : Type*}
    [FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R]
    (f : k →+* R) (g : g_hom) (a b : k[G])
    (h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g <| Multiplicative.ofAdd y)) :
    liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b

Full source

theorem liftNC_mul {g_hom : Type*}
    [FunLike g_hom (Multiplicative G) R] [MulHomClass g_hom (Multiplicative G) R]
    (f : k →+* R) (g : g_hom) (a b : k[G])
    (h_comm : ∀ {x y}, y ∈ a.support → Commute (f (b x)) (g <| Multiplicative.ofAdd y)) :
    liftNC (f : k →+ R) g (a * b) = liftNC (f : k →+ R) g a * liftNC (f : k →+ R) g b :=
  MonoidAlgebra.liftNC_mul f g _ _ @h_comm

Multiplicativity of Lifted Homomorphism in Additive Monoid Algebra under Commutation Condition

Informal description

Let $k$ be a semiring, $G$ an additive monoid, and $R$ a non-associative semiring. Given a ring homomorphism $f \colon k \to R$ and a multiplicative homomorphism $g \colon \text{Multiplicative}\,G \to R$, the lifted homomorphism $\text{liftNC}(f, g) \colon k[G] \to R$ satisfies the following multiplicative property: For any two elements $a, b \in k[G]$, if for every $x$ in the support of $a$ and every $y$ in the support of $b$, the elements $f(b(x))$ and $g(\text{ofAdd}\,y)$ commute in $R$, then \[ \text{liftNC}(f, g)(a * b) = \text{liftNC}(f, g)(a) * \text{liftNC}(f, g)(b). \]

AddMonoidAlgebra.one instance

: One k[G]

Full source

/-- The unit of the multiplication is `single 0 1`, i.e. the function
  that is `1` at `0` and zero elsewhere. -/
instance one : One k[G] :=
  ⟨single 0 1⟩

Multiplicative Identity in Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ has a multiplicative identity given by the function that is $1$ at $0$ and zero elsewhere. In other words, the element $1 \in k[G]$ is defined as $\text{single}(0, 1)$, where $\text{single}(a, b)$ denotes the function that is $b$ at $a$ and zero everywhere else.

AddMonoidAlgebra.one_def theorem

: (1 : k[G]) = single 0 1

Full source

theorem one_def : (1 : k[G]) = single 0 1 :=
  rfl

Definition of the Multiplicative Identity in Additive Monoid Algebra: $1 = \text{single}(0, 1)$

Informal description

The multiplicative identity element $1$ in the additive monoid algebra $k[G]$ is given by the function $\text{single}(0, 1)$, which takes the value $1$ at the additive identity $0 \in G$ and zero elsewhere.

AddMonoidAlgebra.liftNC_one theorem

 {g_hom : Type*} [FunLike g_hom (Multiplicative G) R] [OneHomClass g_hom (Multiplicative G) R] (f : k →+* R)
  (g : g_hom) : liftNC (f : k →+ R) g 1 = 1

Full source

@[simp]
theorem liftNC_one {g_hom : Type*}
    [FunLike g_hom (Multiplicative G) R] [OneHomClass g_hom (Multiplicative G) R]
    (f : k →+* R) (g : g_hom) : liftNC (f : k →+ R) g 1 = 1 :=
  MonoidAlgebra.liftNC_one f g

Lifted Homomorphism Preserves Identity in Additive Monoid Algebra: $\text{liftNC}(f, g)(1) = 1$

Informal description

Let $k$ be a semiring, $G$ an additive monoid, and $R$ a non-associative semiring. Given a ring homomorphism $f \colon k \to R$ and a multiplicative homomorphism $g \colon \text{Multiplicative}\,G \to R$ that preserves the identity element (i.e., $g(1) = 1$), the lifted homomorphism $\text{liftNC}(f, g) \colon k[G] \to R$ satisfies $\text{liftNC}(f, g)(1_{k[G]}) = 1_R$. Here, $1_{k[G]}$ denotes the multiplicative identity in the additive monoid algebra $k[G]$, which is given by the function that is $1$ at the additive identity $0 \in G$ and zero elsewhere.

AddMonoidAlgebra.nonUnitalSemiring instance

: NonUnitalSemiring k[G]

Full source

instance nonUnitalSemiring : NonUnitalSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalNonAssocSemiring with
    mul_assoc := fun f g h => by
      -- Porting note: `reducible` cannot be `local` so proof gets long.
      simp only [mul_def]
      rw [sum_sum_index] <;> congr; on_goal 1 => ext a₁ b₁
      rw [sum_sum_index, sum_sum_index] <;> congr; on_goal 1 => ext a₂ b₂
      rw [sum_sum_index, sum_single_index] <;> congr; on_goal 1 => ext a₃ b₃
      on_goal 1 => rw [sum_single_index, mul_assoc, add_assoc]
      all_goals simp only [single_zero, single_add, forall_true_iff, add_mul,
        mul_add, zero_mul, mul_zero, sum_zero, sum_add] }

Non-unital Semiring Structure on Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ over a semiring $k$ generated by an additive monoid $G$ forms a non-unital semiring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative monoid 2. A multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.nonAssocSemiring instance

: NonAssocSemiring k[G]

Full source

instance nonAssocSemiring : NonAssocSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalNonAssocSemiring with
    natCast := fun n => single 0 n
    natCast_zero := by simp
    natCast_succ := fun _ => by simp; rfl
    one_mul := fun f => by
      simp only [mul_def, one_def, sum_single_index, zero_mul, single_zero, sum_zero, zero_add,
        one_mul, sum_single]
    mul_one := fun f => by
      simp only [mul_def, one_def, sum_single_index, mul_zero, single_zero, sum_zero, add_zero,
        mul_one, sum_single] }

Non-associative Semiring Structure on Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ over a semiring $k$ generated by an additive monoid $G$ forms a non-associative semiring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative monoid 2. A multiplication operation (convolution product) that distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) 4. A multiplicative identity element (1) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.natCast_def theorem

(n : ℕ) : (n : k[G]) = single (0 : G) (n : k)

Full source

theorem natCast_def (n : ℕ) : (n : k[G]) = single (0 : G) (n : k) :=
  rfl

Natural Number Embedding in Additive Monoid Algebra

Informal description

For any natural number $n$, the canonical embedding of $n$ into the additive monoid algebra $k[G]$ is equal to the function that is zero everywhere except at the additive identity $0 \in G$, where it takes the value $n \in k$. In other words, the natural number $n$ is represented in $k[G]$ as: $$ n = \text{single}(0, n) $$ where $\text{single}(0, n)$ is the finitely supported function defined by: \[ \text{single}(0, n)(x) = \begin{cases} n & \text{if } x = 0, \\ 0 & \text{otherwise.} \end{cases} \]

AddMonoidAlgebra.smulZeroClass instance

[Semiring k] [SMulZeroClass R k] : SMulZeroClass R k[G]

Full source

instance smulZeroClass [Semiring k] [SMulZeroClass R k] : SMulZeroClass R k[G] :=
  Finsupp.smulZeroClass

Scalar Multiplication Preserving Zero in Additive Monoid Algebra

Informal description

For any semiring $k$ and any type $R$ with a scalar multiplication action on $k$ that preserves zero (i.e., $r \cdot 0 = 0$ for all $r \in R$), the additive monoid algebra $k[G]$ inherits a scalar multiplication action from $R$ that also preserves zero. This action is defined pointwise: $(r \cdot f)(a) = r \cdot f(a)$ for any $f \in k[G]$ and $a \in G$.

AddMonoidAlgebra.noZeroSMulDivisors instance

[Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] : NoZeroSMulDivisors R k[G]

Full source

instance noZeroSMulDivisors [Zero R] [Semiring k] [SMulZeroClass R k] [NoZeroSMulDivisors R k] :
    NoZeroSMulDivisors R k[G] :=
  Finsupp.noZeroSMulDivisors

No Zero Divisors in Scalar Multiplication of Additive Monoid Algebra

Informal description

For any semiring $k$ and any type $R$ with a zero element and a scalar multiplication action on $k$ that preserves zero, if $R$ and $k$ have no zero divisors with respect to scalar multiplication (i.e., $r \cdot x = 0$ implies $r = 0$ or $x = 0$ for all $r \in R$ and $x \in k$), then the additive monoid algebra $k[G]$ also has no zero divisors with respect to the pointwise scalar multiplication from $R$.

AddMonoidAlgebra.semiring instance

: Semiring k[G]

Full source

instance semiring : Semiring k[G] :=
  { AddMonoidAlgebra.nonUnitalSemiring,
    AddMonoidAlgebra.nonAssocSemiring with }

Semiring Structure on Additive Monoid Algebra

Informal description

The additive monoid algebra $k[G]$ over a semiring $k$ generated by an additive monoid $G$ forms a semiring under the convolution product. Specifically, it is equipped with: 1. An addition operation forming an additive commutative monoid 2. A multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) 4. A multiplicative identity element (1) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.liftNCRingHom definition

(f : k →+* R) (g : Multiplicative G →* R) (h_comm : ∀ x y, Commute (f x) (g y)) : k[G] →+* R

Full source

/-- `liftNC` as a `RingHom`, for when `f` and `g` commute -/
def liftNCRingHom (f : k →+* R) (g : MultiplicativeMultiplicative G →* R) (h_comm : ∀ x y, Commute (f x) (g y)) :
    k[G]k[G] →+* R :=
  { liftNC (f : k →+ R) g with
    map_one' := liftNC_one _ _
    map_mul' := fun _a _b => liftNC_mul _ _ _ _ fun {_ _} _ => h_comm _ _ }

Ring homomorphism lift for additive monoid algebra with commuting images

Informal description

Given a semiring homomorphism $ f \colon k \to R $ and a monoid homomorphism $ g \colon \text{Multiplicative}\,G \to R $ such that $ f(x) $ and $ g(y) $ commute for all $ x \in k $ and $ y \in G $, the function $ \text{liftNCRingHom}\,f\,g $ is the ring homomorphism from the additive monoid algebra $ k[G] $ to $ R $ defined by: \[ \text{liftNCRingHom}\,f\,g\,(\text{single}\,a\,b) = f(b) \cdot g(\text{ofAdd}\,a) \] for all $ a \in G $ and $ b \in k $. This extends the non-commutative lift $ \text{liftNC} $ to a ring homomorphism when the images of $ f $ and $ g $ commute pairwise.

AddMonoidAlgebra.nonUnitalCommSemiring instance

[CommSemiring k] [AddCommSemigroup G] : NonUnitalCommSemiring k[G]

Full source

instance nonUnitalCommSemiring [CommSemiring k] [AddCommSemigroup G] :
    NonUnitalCommSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalSemiring with
    mul_comm := @mul_comm (MonoidAlgebra k <| Multiplicative G) _ }

Non-unital Commutative Semiring Structure on Additive Monoid Algebra

Informal description

For any commutative semiring $k$ and any additive commutative semigroup $G$, the additive monoid algebra $k[G]$ forms a non-unital commutative semiring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative monoid 2. A commutative multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.nontrivial instance

[Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial k[G]

Full source

instance nontrivial [Semiring k] [Nontrivial k] [Nonempty G] : Nontrivial k[G] :=
  Finsupp.instNontrivial

Nontriviality of Additive Monoid Algebra

Informal description

For any semiring $k$ that is nontrivial and any nonempty additive monoid $G$, the additive monoid algebra $k[G]$ is also nontrivial.

AddMonoidAlgebra.commSemiring instance

[CommSemiring k] [AddCommMonoid G] : CommSemiring k[G]

Full source

instance commSemiring [CommSemiring k] [AddCommMonoid G] : CommSemiring k[G] :=
  { AddMonoidAlgebra.nonUnitalCommSemiring, AddMonoidAlgebra.semiring with }

Commutative Semiring Structure on Additive Monoid Algebra

Informal description

For any commutative semiring $k$ and any additive commutative monoid $G$, the additive monoid algebra $k[G]$ forms a commutative semiring under the convolution product. Specifically, it is equipped with: 1. An addition operation forming an additive commutative monoid 2. A commutative multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) 4. A multiplicative identity element (1) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.unique instance

[Semiring k] [Subsingleton k] : Unique k[G]

Full source

instance unique [Semiring k] [Subsingleton k] : Unique k[G] :=
  Finsupp.uniqueOfRight

Uniqueness of Additive Monoid Algebra over a Subsingleton Semiring

Informal description

For any semiring $k$ and any additive monoid $G$, if $k$ is a subsingleton (i.e., has at most one element), then the additive monoid algebra $k[G]$ has a unique element.

AddMonoidAlgebra.addCommGroup instance

[Ring k] : AddCommGroup k[G]

Full source

instance addCommGroup [Ring k] : AddCommGroup k[G] :=
  Finsupp.instAddCommGroup

Additive Commutative Group Structure on Monoid Algebras over Rings

Informal description

For any ring $k$ and any additive monoid $G$, the additive monoid algebra $k[G]$ forms an additive commutative group under pointwise addition.

AddMonoidAlgebra.nonUnitalNonAssocRing instance

[Ring k] [Add G] : NonUnitalNonAssocRing k[G]

Full source

instance nonUnitalNonAssocRing [Ring k] [Add G] : NonUnitalNonAssocRing k[G] :=
  { AddMonoidAlgebra.addCommGroup, AddMonoidAlgebra.nonUnitalNonAssocSemiring with }

Non-unital Non-associative Ring Structure on Additive Monoid Algebra

Informal description

For any ring $k$ and any additive monoid $G$, the additive monoid algebra $k[G]$ forms a non-unital, non-associative ring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative group 2. A multiplication operation (convolution product) that distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.nonUnitalRing instance

[Ring k] [AddSemigroup G] : NonUnitalRing k[G]

Full source

instance nonUnitalRing [Ring k] [AddSemigroup G] : NonUnitalRing k[G] :=
  { AddMonoidAlgebra.addCommGroup, AddMonoidAlgebra.nonUnitalSemiring with }

Non-unital Ring Structure on Additive Monoid Algebra

Informal description

For any ring $k$ and any additive semigroup $G$, the additive monoid algebra $k[G]$ forms a non-unital ring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative group 2. A multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.nonAssocRing instance

[Ring k] [AddZeroClass G] : NonAssocRing k[G]

Full source

instance nonAssocRing [Ring k] [AddZeroClass G] : NonAssocRing k[G] :=
  { AddMonoidAlgebra.addCommGroup,
    AddMonoidAlgebra.nonAssocSemiring with
    intCast := fun z => single 0 (z : k)
    intCast_ofNat := fun n => by simp [natCast_def]
    intCast_negSucc := fun n => by simp [natCast_def, one_def] }

Non-associative Ring Structure on Additive Monoid Algebra

Informal description

For any ring $k$ and any additive monoid $G$ with a zero element, the additive monoid algebra $k[G]$ forms a non-associative ring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative group 2. A multiplication operation (convolution product) that distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) 4. A multiplicative identity element (1) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.intCast_def theorem

[Ring k] [AddZeroClass G] (z : ℤ) : (z : k[G]) = single (0 : G) (z : k)

Full source

theorem intCast_def [Ring k] [AddZeroClass G] (z : ℤ) :
    (z : k[G]) = single (0 : G) (z : k) :=
  rfl

Integer Casting in Additive Monoid Algebra: $(z : k[G]) = \text{single}(0, z)$

Informal description

For any ring $k$ and any additive monoid $G$ with a zero element, the integer casting operation in the additive monoid algebra $k[G]$ is defined by mapping an integer $z \in \mathbb{Z}$ to the element $\text{single}(0_G, z_k)$, where $0_G$ is the zero element of $G$ and $z_k$ is the image of $z$ under the canonical map $\mathbb{Z} \to k$. In other words, the integer $z$ is represented in $k[G]$ as the finitely supported function that is zero everywhere except at the additive identity $0_G \in G$, where it takes the value $z_k \in k$.

AddMonoidAlgebra.ring instance

[Ring k] [AddMonoid G] : Ring k[G]

Full source

instance ring [Ring k] [AddMonoid G] : Ring k[G] :=
  { AddMonoidAlgebra.nonAssocRing, AddMonoidAlgebra.semiring with }

Ring Structure on Additive Monoid Algebra

Informal description

For any ring $k$ and any additive monoid $G$, the additive monoid algebra $k[G]$ forms a ring under the convolution product. Specifically, it is equipped with: 1. An addition operation forming an additive commutative group 2. A multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) 4. A multiplicative identity element (1) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.nonUnitalCommRing instance

[CommRing k] [AddCommSemigroup G] : NonUnitalCommRing k[G]

Full source

instance nonUnitalCommRing [CommRing k] [AddCommSemigroup G] :
    NonUnitalCommRing k[G] :=
  { AddMonoidAlgebra.nonUnitalCommSemiring, AddMonoidAlgebra.nonUnitalRing with }

Non-unital Commutative Ring Structure on Additive Monoid Algebras

Informal description

For any commutative ring $k$ and any additive commutative semigroup $G$, the additive monoid algebra $k[G]$ forms a non-unital commutative ring under the convolution product. Specifically, it satisfies: 1. An addition operation forming an additive commutative group 2. A commutative multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.commRing instance

[CommRing k] [AddCommMonoid G] : CommRing k[G]

Full source

instance commRing [CommRing k] [AddCommMonoid G] : CommRing k[G] :=
  { AddMonoidAlgebra.nonUnitalCommRing, AddMonoidAlgebra.ring with }

Commutative Ring Structure on Additive Monoid Algebras

Informal description

For any commutative ring $k$ and any additive commutative monoid $G$, the additive monoid algebra $k[G]$ forms a commutative ring under the convolution product. Specifically, it is equipped with: 1. An addition operation forming an additive commutative group 2. A commutative multiplication operation (convolution product) that is associative and distributes over addition 3. A zero element that is absorbing for multiplication (i.e., $0 * f = f * 0 = 0$ for all $f \in k[G]$) 4. A multiplicative identity element (1) The convolution product is defined by: $$(f * g)(a) = \sum_{b+c=a} f(b) \cdot g(c)$$ for $f, g \in k[G]$ and $a \in G$.

AddMonoidAlgebra.distribSMul instance

[Semiring k] [DistribSMul R k] : DistribSMul R k[G]

Full source

instance distribSMul [Semiring k] [DistribSMul R k] : DistribSMul R k[G] :=
  Finsupp.distribSMul G k

Distributive Scalar Multiplication on Additive Monoid Algebras

Informal description

For any semiring $k$ and any additive monoid $G$, if $R$ has a distributive scalar multiplication action on $k$, then the additive monoid algebra $k[G]$ inherits a distributive scalar multiplication action from $R$. This action is defined pointwise: $(r \cdot f)(a) = r \cdot f(a)$ for any $r \in R$, $f \in k[G]$, and $a \in G$.

AddMonoidAlgebra.distribMulAction instance

[Monoid R] [Semiring k] [DistribMulAction R k] : DistribMulAction R k[G]

Full source

instance distribMulAction [Monoid R] [Semiring k] [DistribMulAction R k] :
    DistribMulAction R k[G] :=
  Finsupp.distribMulAction G k

Distributive Multiplicative Action on Additive Monoid Algebra

Informal description

For any monoid $R$ and semiring $k$ equipped with a distributive multiplicative action of $R$ on $k$, the additive monoid algebra $k[G]$ inherits a distributive multiplicative action from $R$. This action is defined pointwise, meaning that for any $r \in R$, $f \in k[G]$, and $a \in G$, we have $(r \cdot f)(a) = r \cdot f(a)$.

AddMonoidAlgebra.faithfulSMul instance

[Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] : FaithfulSMul R k[G]

Full source

instance faithfulSMul [Semiring k] [SMulZeroClass R k] [FaithfulSMul R k] [Nonempty G] :
    FaithfulSMul R k[G] :=
  Finsupp.faithfulSMul

Faithfulness of Scalar Multiplication in Additive Monoid Algebras

Informal description

For any semiring $k$, any type $R$ with a scalar multiplication action on $k$ that preserves zero, and any nonempty additive monoid $G$, if the scalar multiplication action of $R$ on $k$ is faithful (i.e., distinct elements of $R$ act differently on some element of $k$), then the induced scalar multiplication action of $R$ on the additive monoid algebra $k[G]$ is also faithful.

AddMonoidAlgebra.module instance

[Semiring R] [Semiring k] [Module R k] : Module R k[G]

Full source

instance module [Semiring R] [Semiring k] [Module R k] : Module R k[G] :=
  Finsupp.module G k

Module Structure on Additive Monoid Algebra

Informal description

For any semiring $R$ and semiring $k$ equipped with a module structure over $R$, the additive monoid algebra $k[G]$ forms a module over $R$ with pointwise scalar multiplication. That is, for any $r \in R$ and $f \in k[G]$, the scalar multiplication is defined by $(r \cdot f)(a) = r \cdot f(a)$ for all $a \in G$.

AddMonoidAlgebra.isScalarTower instance

[Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S] [IsScalarTower R S k] : IsScalarTower R S k[G]

Full source

instance isScalarTower [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMul R S]
    [IsScalarTower R S k] : IsScalarTower R S k[G] :=
  Finsupp.isScalarTower G k

Scalar Tower Property for Additive Monoid Algebra

Informal description

For any semiring $k$ and any types $R$ and $S$ with scalar multiplication actions on $k$ that preserve zero, if $R$ and $S$ form a scalar tower over $k$ (i.e., $(r \cdot s) \cdot x = r \cdot (s \cdot x)$ for all $r \in R$, $s \in S$, $x \in k$), then the additive monoid algebra $k[G]$ also forms a scalar tower with respect to the pointwise scalar multiplication.

AddMonoidAlgebra.smulCommClass instance

[Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] : SMulCommClass R S k[G]

Full source

instance smulCommClass [Semiring k] [SMulZeroClass R k] [SMulZeroClass S k] [SMulCommClass R S k] :
    SMulCommClass R S k[G] :=
  Finsupp.smulCommClass G k

Commutativity of Scalar Multiplication in Additive Monoid Algebra

Informal description

For any semiring $k$ and any types $R$ and $S$ with scalar multiplication actions on $k$ that preserve zero, if the actions of $R$ and $S$ on $k$ commute, then the pointwise scalar multiplication actions of $R$ and $S$ on the additive monoid algebra $k[G]$ also commute. That is, for any $r \in R$, $s \in S$, and $f \in k[G]$, we have $r \cdot (s \cdot f) = s \cdot (r \cdot f)$.

AddMonoidAlgebra.isCentralScalar instance

[Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k] [IsCentralScalar R k] : IsCentralScalar R k[G]

Full source

instance isCentralScalar [Semiring k] [SMulZeroClass R k] [SMulZeroClass Rᵐᵒᵖ k]
    [IsCentralScalar R k] : IsCentralScalar R k[G] :=
  Finsupp.isCentralScalar G k

Central Scalar Property for Additive Monoid Algebra

Informal description

For any semiring $k$ and any type $R$ with a scalar multiplication action on $k$ that preserves zero, if the left and right scalar multiplication actions of $R$ on $k$ coincide (i.e., $r \cdot x = x \cdot r$ for all $r \in R$ and $x \in k$), then the pointwise scalar multiplication actions of $R$ on the additive monoid algebra $k[G]$ also satisfy this central scalar property.

AddMonoidAlgebra.smul_single theorem

[Semiring k] [SMulZeroClass R k] (a : G) (c : R) (b : k) : c • single a b = single a (c • b)

Full source

@[simp]
theorem smul_single [Semiring k] [SMulZeroClass R k] (a : G) (c : R) (b : k) :
    c • single a b = single a (c • b) :=
  Finsupp.smul_single _ _ _

Scalar multiplication commutes with single generator in additive monoid algebra: $c \cdot \text{single}(a, b) = \text{single}(a, c \cdot b)$

Informal description

Let $k$ be a semiring and $R$ be a type with a scalar multiplication action on $k$ that preserves zero. For any element $a$ in an additive monoid $G$, any scalar $c \in R$, and any element $b \in k$, the scalar multiple $c \cdot \text{single}(a, b)$ in the additive monoid algebra $k[G]$ is equal to $\text{single}(a, c \cdot b)$. In mathematical notation: $$c \cdot \text{single}(a, b) = \text{single}(a, c \cdot b).$$

AddMonoidAlgebra.ext theorem

[Semiring k] ⦃f g : AddMonoidAlgebra k G⦄ (H : ∀ (x : G), f x = g x) : f = g

Full source

/-- A copy of `Finsupp.ext` for `AddMonoidAlgebra`. -/
@[ext]
theorem ext [Semiring k] ⦃f g : AddMonoidAlgebra k G⦄ (H : ∀ (x : G), f x = g x) :
    f = g :=
  Finsupp.ext H

Extensionality for Additive Monoid Algebra

Informal description

For any semiring $k$ and any additive monoid $G$, if two elements $f, g$ in the additive monoid algebra $k[G]$ satisfy $f(x) = g(x)$ for all $x \in G$, then $f = g$.

AddMonoidAlgebra.singleAddHom abbrev

[Semiring k] (a : G) : k →+ AddMonoidAlgebra k G

Full source

/-- A copy of `Finsupp.singleAddHom` for `AddMonoidAlgebra`. -/
abbrev singleAddHom [Semiring k] (a : G) : k →+ AddMonoidAlgebra k G := Finsupp.singleAddHom a

Additive Monoid Homomorphism from Semiring to Additive Monoid Algebra via Single-Point Support

Informal description

For a semiring $k$ and an additive monoid $G$, the function $\operatorname{singleAddHom}(a) \colon k \to k[G]$ is an additive monoid homomorphism that maps each element $b \in k$ to the finitely supported function $\operatorname{single}(a, b) \in k[G]$, where $\operatorname{single}(a, b)$ is the function that takes the value $b$ at $a$ and zero elsewhere. More precisely, $\operatorname{singleAddHom}(a)$ satisfies: 1. $\operatorname{singleAddHom}(a)(0) = \operatorname{single}(a, 0)$, and 2. $\operatorname{singleAddHom}(a)(b_1 + b_2) = \operatorname{singleAddHom}(a)(b_1) + \operatorname{singleAddHom}(a)(b_2)$ for all $b_1, b_2 \in k$.

AddMonoidAlgebra.singleAddHom_apply theorem

[Semiring k] (a : G) (b : k) : singleAddHom a b = single a b

Full source

@[simp] lemma singleAddHom_apply [Semiring k] (a : G) (b : k) :
  singleAddHom a b = single a b := rfl

Evaluation of Single-Point Additive Monoid Homomorphism: $\operatorname{singleAddHom}(a)(b) = \operatorname{single}(a, b)$

Informal description

For any semiring $k$ and any additive monoid $G$, the additive monoid homomorphism $\operatorname{singleAddHom}(a) \colon k \to k[G]$ satisfies $\operatorname{singleAddHom}(a)(b) = \operatorname{single}(a, b)$ for all $b \in k$, where $\operatorname{single}(a, b)$ is the function in $k[G]$ that takes the value $b$ at $a$ and zero elsewhere.

AddMonoidAlgebra.addHom_ext' theorem

 {N : Type*} [Semiring k] [AddZeroClass N] ⦃f g : AddMonoidAlgebra k G →+ N⦄
  (H : ∀ (x : G), AddMonoidHom.comp f (singleAddHom x) = AddMonoidHom.comp g (singleAddHom x)) : f = g

Full source

/-- A copy of `Finsupp.addHom_ext'` for `AddMonoidAlgebra`. -/
@[ext high]
theorem addHom_ext' {N : Type*} [Semiring k] [AddZeroClass N]
    ⦃f g : AddMonoidAlgebraAddMonoidAlgebra k G →+ N⦄
    (H : ∀ (x : G), AddMonoidHom.comp f (singleAddHom x) = AddMonoidHom.comp g (singleAddHom x)) :
    f = g :=
  Finsupp.addHom_ext' H

Extensionality of Additive Monoid Homomorphisms on Additive Monoid Algebra via Single Functions

Informal description

Let $k$ be a semiring, $G$ an additive monoid, and $N$ an add-zero class. For any two additive monoid homomorphisms $f, g \colon k[G] \to^+ N$, if for every $x \in G$ the compositions $f \circ \operatorname{singleAddHom}(x)$ and $g \circ \operatorname{singleAddHom}(x)$ are equal, then $f = g$.

AddMonoidAlgebra.distribMulActionHom_ext' theorem

 {N : Type*} [Monoid R] [Semiring k] [AddMonoid N] [DistribMulAction R N] [DistribMulAction R k]
  {f g : AddMonoidAlgebra k G →+[R] N}
  (h : ∀ a : G, f.comp (DistribMulActionHom.single (M := k) a) = g.comp (DistribMulActionHom.single a)) : f = g

Full source

/-- A copy of `Finsupp.distribMulActionHom_ext'` for `AddMonoidAlgebra`. -/
@[ext]
theorem distribMulActionHom_ext' {N : Type*} [Monoid R] [Semiring k] [AddMonoid N]
    [DistribMulAction R N] [DistribMulAction R k]
    {f g : AddMonoidAlgebraAddMonoidAlgebra k G →+[R] N}
    (h : ∀ a : G,
      f.comp (DistribMulActionHom.single (M := k) a) = g.comp (DistribMulActionHom.single a)) :
    f = g :=
  Finsupp.distribMulActionHom_ext' h

Extensionality of Equivariant Additive Monoid Homomorphisms on Additive Monoid Algebra via Single-Point Compositions

Informal description

Let $R$ be a monoid, $k$ a semiring, and $N$ an additive monoid equipped with a distributive multiplicative action of $R$. For any two equivariant additive monoid homomorphisms $f, g \colon k[G] \to N$, if for every $a \in G$ the compositions $f \circ \operatorname{single}(a)$ and $g \circ \operatorname{single}(a)$ are equal, then $f = g$. Here, $\operatorname{single}(a) \colon k \to k[G]$ is the map sending $b \in k$ to the function in $k[G]$ that takes the value $b$ at $a$ and zero elsewhere.

AddMonoidAlgebra.lsingle abbrev

[Semiring R] [Semiring k] [Module R k] (a : G) : k →ₗ[R] AddMonoidAlgebra k G

Full source

/-- A copy of `Finsupp.lsingle` for `AddMonoidAlgebra`. -/
abbrev lsingle [Semiring R] [Semiring k] [Module R k] (a : G) :
    k →ₗ[R] AddMonoidAlgebra k G := Finsupp.lsingle a

Linear single-point embedding map for additive monoid algebra

Informal description

For a semiring $R$, a semiring $k$ equipped with an $R$-module structure, and an element $a \in G$, the linear map $\operatorname{lsingle}(a) \colon k \to R[G]$ sends each element $b \in k$ to the formal linear combination $b \cdot a$ in the additive monoid algebra $R[G]$. More precisely, $\operatorname{lsingle}(a)(b)$ is the finitely supported function from $G$ to $k$ that takes the value $b$ at $a$ and zero elsewhere. This map is linear with respect to the $R$-module structures on $k$ and $R[G]$.

AddMonoidAlgebra.lsingle_apply theorem

[Semiring R] [Semiring k] [Module R k] (a : G) (b : k) : lsingle (R := R) a b = single a b

Full source

@[simp] lemma lsingle_apply [Semiring R] [Semiring k] [Module R k] (a : G) (b : k) :
  lsingle (R := R) a b = single a b := rfl

Linear Single-Point Embedding Equals Single Generator in Additive Monoid Algebra

Informal description

For a semiring $R$, a semiring $k$ equipped with an $R$-module structure, and an element $a \in G$, the linear map $\operatorname{lsingle}(a) \colon k \to R[G]$ satisfies $\operatorname{lsingle}(a)(b) = \operatorname{single}(a, b)$ for all $b \in k$, where $\operatorname{single}(a, b)$ is the element of the additive monoid algebra $R[G]$ that is zero everywhere except at $a$, where it takes the value $b$.

AddMonoidAlgebra.lhom_ext' theorem

 {N : Type*} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k] ⦃f g : AddMonoidAlgebra k G →ₗ[R] N⦄
  (H : ∀ (x : G), LinearMap.comp f (lsingle x) = LinearMap.comp g (lsingle x)) : f = g

Full source

/-- A copy of `Finsupp.lhom_ext'` for `AddMonoidAlgebra`. -/
@[ext high]
lemma lhom_ext' {N : Type*} [Semiring R] [Semiring k] [AddCommMonoid N] [Module R N] [Module R k]
    ⦃f g : AddMonoidAlgebraAddMonoidAlgebra k G →ₗ[R] N⦄
    (H : ∀ (x : G), LinearMap.comp f (lsingle x) = LinearMap.comp g (lsingle x)) :
    f = g :=
  Finsupp.lhom_ext' H

Extensionality of Linear Maps on Additive Monoid Algebra via Single Embeddings

Informal description

Let $R$ be a semiring, $k$ a semiring equipped with an $R$-module structure, and $N$ an $R$-module. For any two $R$-linear maps $f, g \colon k[G] \to N$, if for every $x \in G$ the compositions $f \circ \operatorname{lsingle}(x)$ and $g \circ \operatorname{lsingle}(x)$ are equal as linear maps from $k$ to $N$, then $f = g$.

AddMonoidAlgebra.mul_apply theorem

[DecidableEq G] [Add G] (f g : k[G]) (x : G) :
    (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ + a₂ = x then b₁ * b₂ else 0

Full source

theorem mul_apply [DecidableEq G] [Add G] (f g : k[G]) (x : G) :
    (f * g) x = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => if a₁ + a₂ = x then b₁ * b₂ else 0 :=
  @MonoidAlgebra.mul_apply k (Multiplicative G) _ _ _ _ _ _

Evaluation Formula for Product in Additive Monoid Algebra

Informal description

Let $G$ be an additive monoid with decidable equality, and let $k$ be a semiring. For any two elements $f, g$ in the additive monoid algebra $k[G]$ and any $x \in G$, the evaluation of the product $f * g$ at $x$ is given by: $$(f * g)(x) = \sum_{a_1 \in G} \sum_{a_2 \in G} \begin{cases} f(a_1) \cdot g(a_2) & \text{if } a_1 + a_2 = x \\ 0 & \text{otherwise} \end{cases}$$

AddMonoidAlgebra.mul_apply_antidiagonal theorem

[Add G] (f g : k[G]) (x : G) (s : Finset (G × G))
    (hs : ∀ {p : G × G}, p ∈ s ↔ p.1 + p.2 = x) : (f * g) x = ∑ p ∈ s, f p.1 * g p.2

Full source

theorem mul_apply_antidiagonal [Add G] (f g : k[G]) (x : G) (s : Finset (G × G))
    (hs : ∀ {p : G × G}, p ∈ sp ∈ s ↔ p.1 + p.2 = x) : (f * g) x = ∑ p ∈ s, f p.1 * g p.2 :=
  @MonoidAlgebra.mul_apply_antidiagonal k (Multiplicative G) _ _ _ _ _ s @hs

Evaluation of Additive Monoid Algebra Product via Antidiagonal Sum

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any two elements $f, g$ in the additive monoid algebra $k[G]$ and any $x \in G$, if $s$ is a finite subset of $G \times G$ such that for any pair $(a_1, a_2) \in G \times G$, $(a_1, a_2) \in s$ if and only if $a_1 + a_2 = x$, then the evaluation of the product $f * g$ at $x$ is given by: $$(f * g)(x) = \sum_{(a_1, a_2) \in s} f(a_1) \cdot g(a_2).$$

AddMonoidAlgebra.single_mul_single theorem

[Add G] {a₁ a₂ : G} {b₁ b₂ : k} : single a₁ b₁ * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂)

Full source

theorem single_mul_single [Add G] {a₁ a₂ : G} {b₁ b₂ : k} :
    single a₁ b₁ * single a₂ b₂ = single (a₁ + a₂) (b₁ * b₂) :=
  @MonoidAlgebra.single_mul_single k (Multiplicative G) _ _ _ _ _ _

Product of Single Generators in Additive Monoid Algebra: $\text{single}(a_1, b_1) * \text{single}(a_2, b_2) = \text{single}(a_1 + a_2, b_1 b_2)$

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any elements $a_1, a_2 \in G$ and coefficients $b_1, b_2 \in k$, the product of the single generators $\text{single}(a_1, b_1)$ and $\text{single}(a_2, b_2)$ in the additive monoid algebra $k[G]$ is given by: $$\text{single}(a_1, b_1) * \text{single}(a_2, b_2) = \text{single}(a_1 + a_2, b_1 \cdot b_2).$$

AddMonoidAlgebra.single_commute_single theorem

 [Add G] {a₁ a₂ : G} {b₁ b₂ : k} (ha : AddCommute a₁ a₂) (hb : Commute b₁ b₂) : Commute (single a₁ b₁) (single a₂ b₂)

Full source

theorem single_commute_single [Add G] {a₁ a₂ : G} {b₁ b₂ : k}
    (ha : AddCommute a₁ a₂) (hb : Commute b₁ b₂) :
    Commute (single a₁ b₁) (single a₂ b₂) :=
  @MonoidAlgebra.single_commute_single k (Multiplicative G) _ _ _ _ _ _ ha hb

Commutation of Single Generators in Additive Monoid Algebra under Additive and Multiplicative Commuting Conditions

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any elements $a_1, a_2 \in G$ and coefficients $b_1, b_2 \in k$, if $a_1$ and $a_2$ additively commute (i.e., $a_1 + a_2 = a_2 + a_1$) and $b_1$ and $b_2$ commute (i.e., $b_1 b_2 = b_2 b_1$), then the single generators $\text{single}(a_1, b_1)$ and $\text{single}(a_2, b_2)$ commute in the additive monoid algebra $k[G]$.

AddMonoidAlgebra.single_pow theorem

[AddMonoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (n • a) (b ^ n)

Full source

theorem single_pow [AddMonoid G] {a : G} {b : k} : ∀ n : ℕ, single a b ^ n = single (n • a) (b ^ n)
  | 0 => by
    simp only [pow_zero, zero_nsmul]
    rfl
  | n + 1 => by
    rw [pow_succ, pow_succ, single_pow n, single_mul_single, add_nsmul, one_nsmul]

Power of Single Generator in Additive Monoid Algebra: $\text{single}(a, b)^n = \text{single}(n \cdot a, b^n)$

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any element $a \in G$, coefficient $b \in k$, and natural number $n$, the $n$-th power of the single generator $\text{single}(a, b)$ in the additive monoid algebra $k[G]$ is given by: $$\text{single}(a, b)^n = \text{single}(n \cdot a, b^n),$$ where $n \cdot a$ denotes the $n$-fold sum of $a$ in $G$ and $b^n$ denotes the $n$-th power of $b$ in $k$.

AddMonoidAlgebra.ofMagma definition

[Add G] : Multiplicative G →ₙ* k[G]

Full source

/-- The embedding of an additive magma into its additive magma algebra. -/
@[simps]
def ofMagma [Add G] : MultiplicativeMultiplicative G →ₙ* k[G] where
  toFun a := single a 1
  map_mul' a b := by simp only [mul_def, mul_one, sum_single_index, single_eq_zero, mul_zero]; rfl

Embedding of additive magma into its magma algebra

Informal description

The embedding of an additive magma $G$ into its additive magma algebra $k[G]$, viewed as a non-unital multiplicative homomorphism from the multiplicative version of $G$ to $k[G]$. Concretely, this maps an element $a$ of $G$ to the element $\text{single}(a, 1)$ in $k[G]$, where $\text{single}(a, 1)$ is the finitely supported function that takes the value $1$ at $a$ and $0$ elsewhere. The homomorphism property means it preserves the multiplication operation, which in the multiplicative version of $G$ corresponds to addition in $G$.

AddMonoidAlgebra.of definition

[AddZeroClass G] : Multiplicative G →* k[G]

Full source

/-- Embedding of a magma with zero into its magma algebra. -/
def of [AddZeroClass G] : MultiplicativeMultiplicative G →* k[G] :=
  { ofMagma k G with
    toFun := fun a => single a 1
    map_one' := rfl }

Embedding of additive monoid into its monoid algebra

Informal description

The embedding of an additive monoid $G$ into its monoid algebra $k[G]$, viewed as a multiplicative monoid homomorphism from the multiplicative version of $G$ to $k[G]$. Concretely, this maps an element $a$ of $G$ to the element $\text{single}(a, 1)$ in $k[G]$, where $\text{single}(a, 1)$ is the finitely supported function that takes the value $1$ at $a$ and $0$ elsewhere. The homomorphism property means it preserves both the multiplicative identity (mapping the additive identity of $G$ to the multiplicative identity of $k[G]$) and the multiplication operation (which in the multiplicative version of $G$ corresponds to addition in $G$).

AddMonoidAlgebra.of' definition

: G → k[G]

Full source

/-- Embedding of a magma with zero `G`, into its magma algebra, having `G` as source. -/
def of' : G → k[G] := fun a => single a 1

Canonical embedding of an additive monoid into its monoid algebra

Informal description

The function maps an element $a$ of an additive monoid $G$ to the element $\text{single}(a, 1)$ in the additive monoid algebra $k[G]$, where $\text{single}(a, 1)$ is the finitely supported function that takes the value $1$ at $a$ and $0$ elsewhere.

AddMonoidAlgebra.of_apply theorem

[AddZeroClass G] (a : Multiplicative G) : of k G a = single a.toAdd 1

Full source

@[simp]
theorem of_apply [AddZeroClass G] (a : Multiplicative G) :
    of k G a = single a.toAdd 1 :=
  rfl

Embedding of Multiplicative Monoid into Additive Monoid Algebra Maps Elements to Single Generators

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any element $a$ in the multiplicative version of $G$, the embedding $\text{of} \colon \text{Multiplicative}\, G \to k[G]$ satisfies $\text{of}(a) = \text{single}(a_{\text{add}}, 1)$, where $a_{\text{add}}$ is the additive counterpart of $a$ under the equivalence $\text{Multiplicative}\, G \simeq G$, and $\text{single}(a_{\text{add}}, 1)$ is the finitely supported function in $k[G]$ that takes the value $1$ at $a_{\text{add}}$ and $0$ elsewhere.

AddMonoidAlgebra.of'_apply theorem

(a : G) : of' k G a = single a 1

Full source

@[simp]
theorem of'_apply (a : G) : of' k G a = single a 1 :=
  rfl

Canonical embedding equals single generator in additive monoid algebra

Informal description

For any element $a$ of an additive monoid $G$ and semiring $k$, the canonical embedding $\text{of}'$ into the additive monoid algebra $k[G]$ satisfies $\text{of}'(a) = \text{single}(a, 1)$, where $\text{single}(a, 1)$ is the finitely supported function that takes the value $1$ at $a$ and $0$ elsewhere.

AddMonoidAlgebra.of'_eq_of theorem

[AddZeroClass G] (a : G) : of' k G a = of k G (.ofAdd a)

Full source

theorem of'_eq_of [AddZeroClass G] (a : G) : of' k G a = of k G (.ofAdd a) := rfl

Equality of Canonical Embeddings in Additive Monoid Algebra

Informal description

For any element $a$ of an additive monoid $G$ with an additive zero class structure, the canonical embedding $\mathrm{of}'$ into the additive monoid algebra $k[G]$ equals the composition of the embedding $\mathrm{of}$ with the multiplicative type tag construction, i.e., $\mathrm{of}'(a) = \mathrm{of}(a)$ where $a$ is viewed in the multiplicative version of $G$.

AddMonoidAlgebra.of_injective theorem

[Nontrivial k] [AddZeroClass G] : Function.Injective (of k G)

Full source

theorem of_injective [Nontrivial k] [AddZeroClass G] : Function.Injective (of k G) :=
  MonoidAlgebra.of_injective

Injectivity of the Canonical Embedding into Additive Monoid Algebra

Informal description

Let $k$ be a nontrivial semiring and $G$ an additive monoid with a zero element. The canonical embedding $\mathrm{of} \colon G \to k[G]$, which maps each $a \in G$ to the element $\mathrm{single}(a, 1)$ in the additive monoid algebra $k[G]$, is injective.

AddMonoidAlgebra.of'_commute theorem

[AddZeroClass G] {a : G} (h : ∀ a', AddCommute a a') (f : AddMonoidAlgebra k G) : Commute (of' k G a) f

Full source

theorem of'_commute [AddZeroClass G] {a : G} (h : ∀ a', AddCommute a a')
    (f : AddMonoidAlgebra k G) :
    Commute (of' k G a) f :=
  MonoidAlgebra.of_commute (G := Multiplicative G) h f

Central Elements Embed into Center of Additive Monoid Algebra

Informal description

Let $G$ be an additive monoid with a zero element and $k$ a semiring. For any element $a \in G$ that additively commutes with every element of $G$ (i.e., $a + a' = a' + a$ for all $a' \in G$), the image $\iota(a)$ of $a$ under the canonical embedding $\iota \colon G \to k[G]$ commutes with every element $f$ of the additive monoid algebra $k[G]$. Here $\iota(a) = \text{single}(a,1)$ is the element of $k[G]$ that takes value $1$ at $a$ and $0$ elsewhere.

AddMonoidAlgebra.singleHom definition

[AddZeroClass G] : k × Multiplicative G →* k[G]

Full source

/-- `Finsupp.single` as a `MonoidHom` from the product type into the additive monoid algebra.

Note the order of the elements of the product are reversed compared to the arguments of
`Finsupp.single`.
-/
@[simps]
def singleHom [AddZeroClass G] : k × Multiplicative Gk × Multiplicative G →* k[G] where
  toFun a := single a.2.toAdd a.1
  map_one' := rfl
  map_mul' _a _b := single_mul_single.symm

Monoid homomorphism from pairs to additive monoid algebra via single-point functions

Informal description

The function `singleHom` is a monoid homomorphism from the product type $k \times \text{Multiplicative}\,G$ to the additive monoid algebra $k[G]$, defined by mapping a pair $(b, a)$ to the finitely supported function $\text{single}(a, b)$, which is zero everywhere except at $a \in G$ where it takes the value $b \in k$.

AddMonoidAlgebra.smul_single' theorem

(c : k) (a : G) (b : k) : c • single a b = single a (c * b)

Full source

/-- Copy of `Finsupp.smul_single'` that avoids the `AddMonoidAlgebra = Finsupp` defeq abuse. -/
theorem smul_single' (c : k) (a : G) (b : k) : c • single a b = single a (c * b) :=
  Finsupp.smul_single' c a b

Scalar Multiplication Commutes with Single-Point Function in Additive Monoid Algebra: $c \cdot (\text{single}\, a\, b) = \text{single}\, a\, (c \cdot b)$

Informal description

For any scalar $c \in k$, any element $a \in G$, and any element $b \in k$, the scalar multiple $c \cdot (\text{single}\, a\, b)$ in the additive monoid algebra $k[G]$ is equal to the single-point function $\text{single}\, a\, (c \cdot b)$. In mathematical notation: $$c \cdot (\text{single}\, a\, b) = \text{single}\, a\, (c \cdot b).$$

AddMonoidAlgebra.mul_single_apply_aux theorem

[Add G] (f : k[G]) (r : k) (x y z : G)
    (H : ∀ a ∈ f.support, a + x = z ↔ a = y) : (f * single x r) z = f y * r

Full source

theorem mul_single_apply_aux [Add G] (f : k[G]) (r : k) (x y z : G)
    (H : ∀ a ∈ f.support, a + x = z ↔ a = y) : (f * single x r) z = f y * r :=
  @MonoidAlgebra.mul_single_apply_aux k (Multiplicative G) _ _ _ _ _ _ _ H

Evaluation of Additive Monoid Algebra Product at a Point via Single Generator

Informal description

Let $G$ be an additive monoid and $k$ a semiring. Given an element $f \in k[G]$, coefficients $r \in k$, and elements $x, y, z \in G$, suppose that for every $a$ in the support of $f$, the equation $a + x = z$ holds if and only if $a = y$. Then the evaluation of the convolution product $f * \text{single}(x, r)$ at $z$ is equal to $f(y) \cdot r$, i.e., $$(f * \text{single}(x, r))(z) = f(y) \cdot r.$$

AddMonoidAlgebra.mul_single_zero_apply theorem

[AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (f * single (0 : G) r) x = f x * r

Full source

theorem mul_single_zero_apply [AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (f * single (0 : G) r) x = f x * r :=
  f.mul_single_apply_aux r _ _ _ fun a _ => by rw [add_zero]

Evaluation of Convolution Product with Zero-Point Function in Additive Monoid Algebra: $(f * \text{single}(0, r))(x) = f(x) \cdot r$

Informal description

Let $G$ be an additive monoid with a zero element and $k$ a semiring. For any element $f$ in the additive monoid algebra $k[G]$, any coefficient $r \in k$, and any element $x \in G$, the evaluation of the convolution product $f * \text{single}(0, r)$ at $x$ satisfies: $$(f * \text{single}(0, r))(x) = f(x) \cdot r.$$

AddMonoidAlgebra.mul_single_apply_of_not_exists_add theorem

[Add G] (r : k) {g g' : G} (x : k[G])
    (h : ¬∃ d, g' = d + g) : (x * single g r) g' = 0

Full source

theorem mul_single_apply_of_not_exists_add [Add G] (r : k) {g g' : G} (x : k[G])
    (h : ¬∃ d, g' = d + g) : (x * single g r) g' = 0 :=
  @MonoidAlgebra.mul_single_apply_of_not_exists_mul k (Multiplicative G) _ _ _ _ _ _ h

Vanishing of Additive Monoid Algebra Product When No Additive Factor Exists

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any $r \in k$, $g, g' \in G$, and $x \in k[G]$, if there does not exist $d \in G$ such that $g' = d + g$, then the evaluation of the product $x * \text{single}(g, r)$ at $g'$ is zero, i.e., $(x * \text{single}(g, r))(g') = 0$.

AddMonoidAlgebra.single_mul_apply_aux theorem

[Add G] (f : k[G]) (r : k) (x y z : G)
    (H : ∀ a ∈ f.support, x + a = y ↔ a = z) : (single x r * f) y = r * f z

Full source

theorem single_mul_apply_aux [Add G] (f : k[G]) (r : k) (x y z : G)
    (H : ∀ a ∈ f.support, x + a = y ↔ a = z) : (single x r * f) y = r * f z :=
  @MonoidAlgebra.single_mul_apply_aux k (Multiplicative G) _ _ _ _ _ _ _ H

Evaluation of Additive Convolution Product with Single Generator under Additive Condition

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any element $f \in k[G]$, coefficients $r \in k$, elements $x, y, z \in G$, and a hypothesis $H$ stating that for all $a$ in the support of $f$, the equation $x + a = y$ holds if and only if $a = z$, we have: $$(\text{single}(x, r) * f)(y) = r \cdot f(z)$$ where $\text{single}(x, r)$ is the element of the additive monoid algebra $k[G]$ that takes value $r$ at $x$ and zero elsewhere, and $*$ denotes the convolution product in $k[G]$.

AddMonoidAlgebra.single_zero_mul_apply theorem

[AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (single (0 : G) r * f) x = r * f x

Full source

theorem single_zero_mul_apply [AddZeroClass G] (f : k[G]) (r : k) (x : G) :
    (single (0 : G) r * f) x = r * f x :=
  f.single_mul_apply_aux r _ _ _ fun a _ => by rw [zero_add]

Convolution with Single Zero Element in Additive Monoid Algebra

Informal description

Let $G$ be an additive monoid with a zero element, $k$ a semiring, $f \in k[G]$, $r \in k$, and $x \in G$. Then the evaluation of the convolution product $\text{single}(0, r) * f$ at $x$ satisfies: $$(\text{single}(0, r) * f)(x) = r \cdot f(x)$$ where $\text{single}(0, r)$ is the element of the additive monoid algebra $k[G]$ that takes value $r$ at $0$ and zero elsewhere.

AddMonoidAlgebra.single_mul_apply_of_not_exists_add theorem

[Add G] (r : k) {g g' : G} (x : k[G])
    (h : ¬∃ d, g' = g + d) : (single g r * x) g' = 0

Full source

theorem single_mul_apply_of_not_exists_add [Add G] (r : k) {g g' : G} (x : k[G])
    (h : ¬∃ d, g' = g + d) : (single g r * x) g' = 0 :=
  @MonoidAlgebra.single_mul_apply_of_not_exists_mul k (Multiplicative G) _ _ _ _ _ _ h

Vanishing of Additive Convolution Product When No Additive Relation Exists

Informal description

Let $G$ be an additive monoid and $k$ a semiring. For any elements $g, g' \in G$ and any $x \in k[G]$, if there does not exist $d \in G$ such that $g' = g + d$, then the evaluation of the convolution product $\text{single}(g, r) * x$ at $g'$ is zero: $$(\text{single}(g, r) * x)(g') = 0$$ where $\text{single}(g, r)$ is the element of the additive monoid algebra $k[G]$ that takes value $r$ at $g$ and zero elsewhere.

AddMonoidAlgebra.mul_single_apply theorem

[AddGroup G] (f : k[G]) (r : k) (x y : G) :
    (f * single x r) y = f (y - x) * r

Full source

theorem mul_single_apply [AddGroup G] (f : k[G]) (r : k) (x y : G) :
    (f * single x r) y = f (y - x) * r :=
  (sub_eq_add_neg y x).symm ▸ @MonoidAlgebra.mul_single_apply k (Multiplicative G) _ _ _ _ _ _

Evaluation of Convolution Product with Single Generator in Additive Monoid Algebra: $(f * \text{single}(x, r))(y) = f(y - x) \cdot r$

Informal description

Let $k$ be a semiring and $G$ an additive group. For any element $f$ in the additive monoid algebra $k[G]$, any coefficient $r \in k$, and any elements $x, y \in G$, the evaluation of the convolution product $f * \text{single}(x, r)$ at $y$ is given by: $$(f * \text{single}(x, r))(y) = f(y - x) \cdot r.$$

AddMonoidAlgebra.single_mul_apply theorem

[AddGroup G] (r : k) (x : G) (f : k[G]) (y : G) :
    (single x r * f) y = r * f (-x + y)

Full source

theorem single_mul_apply [AddGroup G] (r : k) (x : G) (f : k[G]) (y : G) :
    (single x r * f) y = r * f (-x + y) :=
  @MonoidAlgebra.single_mul_apply k (Multiplicative G) _ _ _ _ _ _

Evaluation of Additive Convolution Product: $(\text{single}(x, r) * f)(y) = r \cdot f(-x + y)$

Informal description

Let $G$ be an additive group, $k$ a semiring, and $k[G]$ the additive monoid algebra of $G$ over $k$. For any coefficient $r \in k$, group elements $x, y \in G$, and element $f \in k[G]$, the evaluation of the convolution product $\text{single}(x, r) * f$ at $y$ is given by: $$(\text{single}(x, r) * f)(y) = r \cdot f(-x + y)$$ where $\text{single}(x, r)$ denotes the element of $k[G]$ that takes value $r$ at $x$ and zero elsewhere, and $*$ denotes the convolution product in $k[G]$.

AddMonoidAlgebra.liftNC_smul theorem

 {R : Type*} [AddZeroClass G] [Semiring R] (f : k →+* R) (g : Multiplicative G →* R) (c : k) (φ : MonoidAlgebra k G) :
  liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ

Full source

theorem liftNC_smul {R : Type*} [AddZeroClass G] [Semiring R] (f : k →+* R)
    (g : MultiplicativeMultiplicative G →* R) (c : k) (φ : MonoidAlgebra k G) :
    liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ :=
  @MonoidAlgebra.liftNC_smul k (Multiplicative G) _ _ _ _ f g c φ

Linearity of lifted homomorphism with respect to scalar multiplication in additive monoid algebra

Informal description

Let $k$ be a semiring, $G$ an additive monoid, and $R$ a semiring. Given a ring homomorphism $f \colon k \to R$ and a monoid homomorphism $g \colon \text{Multiplicative}\,G \to R$, for any scalar $c \in k$ and any element $\varphi \in k[G]$, the lifted homomorphism $\operatorname{liftNC}(f, g)$ satisfies: \[ \operatorname{liftNC}(f, g)(c \cdot \varphi) = f(c) \cdot \operatorname{liftNC}(f, g)(\varphi) \] where $\operatorname{liftNC}(f, g)$ is the additive homomorphism from $k[G]$ to $R$ defined by linearly extending the map $\text{single}(a, b) \mapsto f(b) \cdot g(\text{ofAdd}\,a)$.

AddMonoidAlgebra.induction_on theorem

[AddMonoid G] {p : k[G] → Prop} (f : k[G])
    (hM : ∀ g, p (of k G (Multiplicative.ofAdd g)))
    (hadd : ∀ f g : k[G], p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f

Full source

theorem induction_on [AddMonoid G] {p : k[G] → Prop} (f : k[G])
    (hM : ∀ g, p (of k G (Multiplicative.ofAdd g)))
    (hadd : ∀ f g : k[G], p f → p g → p (f + g))
    (hsmul : ∀ (r : k) (f), p f → p (r • f)) : p f := by
  refine Finsupp.induction_linear f ?_ (fun f g hf hg => hadd f g hf hg) fun g r => ?_
  · simpa using hsmul 0 (of k G (Multiplicative.ofAdd 0)) (hM 0)
  · convert hsmul r (of k G (Multiplicative.ofAdd g)) (hM g)
    simp

Induction Principle for Additive Monoid Algebras

Informal description

Let $k$ be a semiring and $G$ be an additive monoid. For any predicate $p$ on the additive monoid algebra $k[G]$ and any element $f \in k[G]$, if the following conditions hold: 1. For every $g \in G$, $p(\text{of}(g))$ holds, where $\text{of}(g)$ is the embedding of $g$ into $k[G]$. 2. For any $f_1, f_2 \in k[G]$, if $p(f_1)$ and $p(f_2)$ hold, then $p(f_1 + f_2)$ holds. 3. For any $r \in k$ and $f' \in k[G]$, if $p(f')$ holds, then $p(r \cdot f')$ holds, then $p(f)$ holds for all $f \in k[G]$.

AddMonoidAlgebra.isScalarTower_self instance

[IsScalarTower R k k] : IsScalarTower R k[G] k[G]

Full source

instance isScalarTower_self [IsScalarTower R k k] :
    IsScalarTower R k[G] k[G] :=
  @MonoidAlgebra.isScalarTower_self k (Multiplicative G) R _ _ _ _

Scalar Multiplication Tower Property for Additive Monoid Algebras

Informal description

For any semiring $k$, additive monoid $G$, and type $R$ with a scalar multiplication action on $k$ that satisfies the tower property (i.e., $(r \cdot s) \cdot t = r \cdot (s \cdot t)$ for all $r \in R$, $s, t \in k$), the additive monoid algebra $k[G]$ inherits the scalar multiplication tower property from $k$. That is, for any $r \in R$ and $f, g \in k[G]$, we have $(r \cdot f) * g = r \cdot (f * g)$, where $*$ denotes the convolution product in $k[G]$.

AddMonoidAlgebra.smulCommClass_self instance

[SMulCommClass R k k] : SMulCommClass R k[G] k[G]

Full source

/-- Note that if `k` is a `CommSemiring` then we have `SMulCommClass k k k` and so we can take
`R = k` in the below. In other words, if the coefficients are commutative amongst themselves, they
also commute with the algebra multiplication. -/
instance smulCommClass_self [SMulCommClass R k k] :
    SMulCommClass R k[G] k[G] :=
  @MonoidAlgebra.smulCommClass_self k (Multiplicative G) R _ _ _ _

Commutativity of Scalar Multiplication with Additive Monoid Algebra Multiplication

Informal description

For any semiring $k$, additive monoid $G$, and type $R$ such that the scalar multiplications by $R$ and $k$ on $k$ commute, the scalar multiplications by $R$ and the additive monoid algebra $k[G]$ on $k[G]$ also commute. That is, for any $r \in R$, $f \in k[G]$, and $g \in k[G]$, we have: $$ r \cdot (f * g) = f * (r \cdot g). $$

AddMonoidAlgebra.smulCommClass_symm_self instance

[SMulCommClass k R k] : SMulCommClass k[G] R k[G]

Full source

instance smulCommClass_symm_self [SMulCommClass k R k] :
    SMulCommClass k[G] R k[G] :=
  @MonoidAlgebra.smulCommClass_symm_self k (Multiplicative G) R _ _ _ _

Commutativity of Scalar Multiplication with Additive Monoid Algebra Multiplication

Informal description

For any semiring $k$, additive monoid $G$, and type $R$ such that the scalar multiplications by $k$ and $R$ on $k$ commute, the scalar multiplications by the additive monoid algebra $k[G]$ and $R$ on $k[G]$ also commute. That is, for any $f \in k[G]$, $r \in R$, and $g \in k[G]$, we have: $$ f * (r \cdot g) = r \cdot (f * g). $$

AddMonoidAlgebra.singleZeroRingHom definition

[Semiring k] [AddMonoid G] : k →+* k[G]

Full source

/-- `Finsupp.single 0` as a `RingHom` -/
@[simps]
def singleZeroRingHom [Semiring k] [AddMonoid G] : k →+* k[G] :=
  { singleAddHom 0 with
    toFun := single 0
    map_one' := rfl
    map_mul' := fun x y => by simp only [Finsupp.singleAddHom, single_mul_single, zero_add] }

Ring homomorphism embedding $k$ into $k[G]$ via zero support

Informal description

The ring homomorphism from a semiring $k$ to the additive monoid algebra $k[G]$, defined by mapping each element $b \in k$ to the function $\text{single}(0, b) \in k[G]$, where $\text{single}(0, b)$ is the function that takes the value $b$ at the additive identity $0 \in G$ and zero elsewhere. This homomorphism satisfies: 1. $\text{single}(0, 1) = 1$ (preservation of multiplicative identity) 2. $\text{single}(0, x \cdot y) = \text{single}(0, x) * \text{single}(0, y)$ (preservation of multiplication) 3. $\text{single}(0, x + y) = \text{single}(0, x) + \text{single}(0, y)$ (preservation of addition)

AddMonoidAlgebra.ringHom_ext theorem

 {R} [Semiring k] [AddMonoid G] [Semiring R] {f g : k[G] →+* R} (h₀ : ∀ b, f (single 0 b) = g (single 0 b))
  (h_of : ∀ a, f (single a 1) = g (single a 1)) : f = g

Full source

/-- If two ring homomorphisms from `k[G]` are equal on all `single a 1`
and `single 0 b`, then they are equal. -/
theorem ringHom_ext {R} [Semiring k] [AddMonoid G] [Semiring R] {f g : k[G]k[G] →+* R}
    (h₀ : ∀ b, f (single 0 b) = g (single 0 b)) (h_of : ∀ a, f (single a 1) = g (single a 1)) :
    f = g :=
  @MonoidAlgebra.ringHom_ext k (Multiplicative G) R _ _ _ _ _ h₀ h_of

Extensionality of Ring Homomorphisms on Additive Monoid Algebra Generators

Informal description

Let $k$ be a semiring, $G$ an additive monoid, and $R$ a semiring. For any two ring homomorphisms $f, g \colon k[G] \to R$, if: 1. $f(\text{single}(0, b)) = g(\text{single}(0, b))$ for all $b \in k$, and 2. $f(\text{single}(a, 1)) = g(\text{single}(a, 1))$ for all $a \in G$, then $f = g$. Here $\text{single}(a, b)$ denotes the element of $k[G]$ that is $b$ at $a$ and zero elsewhere.

AddMonoidAlgebra.ringHom_ext' theorem

 {R} [Semiring k] [AddMonoid G] [Semiring R] {f g : k[G] →+* R}
  (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom)
  (h_of : (f : k[G] →* R).comp (of k G) = (g : k[G] →* R).comp (of k G)) : f = g

Full source

/-- If two ring homomorphisms from `k[G]` are equal on all `single a 1`
and `single 0 b`, then they are equal.

See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' {R} [Semiring k] [AddMonoid G] [Semiring R] {f g : k[G]k[G] →+* R}
    (h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom)
    (h_of : (f : k[G]k[G] →* R).comp (of k G) = (g : k[G]k[G] →* R).comp (of k G)) :
    f = g :=
  ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)

Extensionality of Ring Homomorphisms on Additive Monoid Algebra via Compositions

Informal description

Let $k$ be a semiring, $G$ an additive monoid, and $R$ a semiring. For any two ring homomorphisms $f, g \colon k[G] \to R$, if: 1. The compositions $f \circ \iota = g \circ \iota$, where $\iota \colon k \to k[G]$ is the embedding of $k$ via $\text{single}(0, \cdot)$, and 2. The compositions $\tilde{f} \circ \eta = \tilde{g} \circ \eta$, where $\tilde{f}, \tilde{g} \colon k[G] \to R$ are the multiplicative monoid homomorphisms underlying $f$ and $g$, and $\eta \colon G \to k[G]$ is the embedding of $G$ via $\text{single}(\cdot, 1)$, then $f = g$. Here $\text{single}(a, b)$ denotes the element of $k[G]$ that is $b$ at $a$ and zero elsewhere.

AddMonoidAlgebra.opRingEquiv definition

[AddCommMonoid G] : k[G]ᵐᵒᵖ ≃+* kᵐᵒᵖ[G]

Full source

/-- The opposite of an `R[I]` is ring equivalent to
the `AddMonoidAlgebra Rᵐᵒᵖ I` over the opposite ring, taking elements to their opposite. -/
@[simps! +simpRhs apply symm_apply]
protected noncomputable def opRingEquiv [AddCommMonoid G] :
    k[G]k[G]ᵐᵒᵖk[G]ᵐᵒᵖ ≃+* kᵐᵒᵖ[G] :=
  { opAddEquiv.symm.trans (mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ)) with
    map_mul' := by
      let f : k[G]k[G]ᵐᵒᵖk[G]ᵐᵒᵖ ≃+ kᵐᵒᵖ[G] :=
        opAddEquiv.symm.trans (mapRange.addEquiv (opAddEquiv : k ≃+ kᵐᵒᵖ))
      show ∀ (x y : k[G]k[G]ᵐᵒᵖ), f (x * y) = f x * f y
      rw [← AddEquiv.coe_toAddMonoidHom, AddMonoidHom.map_mul_iff]
      ext i₁ r₁ i₂ r₂ : 6
      dsimp only [f, AddMonoidHom.compr₂_apply, AddMonoidHom.compl₂_apply,
        AddMonoidHom.comp_apply, AddMonoidHom.coe_coe,
        AddEquiv.toAddMonoidHom_eq_coe, AddEquiv.coe_addMonoidHom_trans,
        singleAddHom_apply, opAddEquiv_apply, opAddEquiv_symm_apply,
        AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft, unop_mul, unop_op]
      -- Defeq abuse. Probably `k[G]` vs `G →₀ k`.
      erw [mapRange.addEquiv_apply, mapRange.addEquiv_apply, mapRange.addEquiv_apply]
      rw [single_mul_single, mapRange_single, mapRange_single, mapRange_single, single_mul_single]
      simp only [opAddEquiv_apply, op_mul, add_comm] }

Ring equivalence between opposite of additive monoid algebra and monoid algebra over opposite ring

Informal description

The opposite of the additive monoid algebra $k[G]^\text{op}$ is ring equivalent to the additive monoid algebra $k^\text{op}[G]$ over the opposite ring, where elements are mapped to their opposites. More precisely, there exists a ring equivalence (bijective homomorphism preserving both addition and multiplication) between: - The opposite algebra $(k[G])^\text{op}$ (where multiplication is reversed) - The algebra $k^\text{op}[G]$ (where coefficients come from the opposite ring $k^\text{op}$) The equivalence maps an element $\text{op}(f) \in (k[G])^\text{op}$ to the function in $k^\text{op}[G]$ obtained by applying the opposite operation to each coefficient of $f$.

AddMonoidAlgebra.opRingEquiv_single theorem

[AddCommMonoid G] (r : k) (x : G) : AddMonoidAlgebra.opRingEquiv (op (single x r)) = single x (op r)

Full source

theorem opRingEquiv_single [AddCommMonoid G] (r : k) (x : G) :
    AddMonoidAlgebra.opRingEquiv (op (single x r)) = single x (op r) := by simp

Ring equivalence preserves single generators in opposite additive monoid algebras

Informal description

For any additive commutative monoid $G$ and semiring $k$, the ring equivalence between the opposite of the additive monoid algebra $k[G]^\text{op}$ and the additive monoid algebra over the opposite ring $k^\text{op}[G]$ maps the opposite of the single generator $\text{op}(\text{single}(x, r))$ to $\text{single}(x, \text{op}(r))$, where $x \in G$ and $r \in k$.

AddMonoidAlgebra.opRingEquiv_symm_single theorem

 [AddCommMonoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) : AddMonoidAlgebra.opRingEquiv.symm (single x r) = op (single x r.unop)

Full source

theorem opRingEquiv_symm_single [AddCommMonoid G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
    AddMonoidAlgebra.opRingEquiv.symm (single x r) = op (single x r.unop) := by simp

Inverse Ring Equivalence Maps Single Generators in Opposite Additive Monoid Algebras

Informal description

For any additive commutative monoid $G$ and semiring $k$, the inverse of the ring equivalence between $(k[G])^\text{op}$ and $k^\text{op}[G]$ maps the single generator $\text{single}(x, r)$ in $k^\text{op}[G]$ (where $x \in G^\text{op}$ and $r \in k^\text{op}$) to $\text{op}(\text{single}(x, r^\text{unop}))$ in $(k[G])^\text{op}$.

AddMonoidAlgebra.prod_single theorem

 [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
  (∏ i ∈ s, single (a i) (b i)) = single (∑ i ∈ s, a i) (∏ i ∈ s, b i)

Full source

theorem prod_single [CommSemiring k] [AddCommMonoid G] {s : Finset ι} {a : ι → G} {b : ι → k} :
    (∏ i ∈ s, single (a i) (b i)) = single (∑ i ∈ s, a i) (∏ i ∈ s, b i) :=
  Finset.cons_induction_on s rfl fun a s has ih => by
    rw [prod_cons has, ih, single_mul_single, sum_cons has, prod_cons has]

Product of Single Generators in Additive Monoid Algebra: $\prod_i \text{single}(a_i, b_i) = \text{single}(\sum_i a_i, \prod_i b_i)$

Informal description

Let $k$ be a commutative semiring and $G$ an additive commutative monoid. For any finite set $s$ and functions $a : s \to G$, $b : s \to k$, the product of single generators in the additive monoid algebra $k[G]$ satisfies: $$ \prod_{i \in s} \text{single}(a_i, b_i) = \text{single}\left(\sum_{i \in s} a_i, \prod_{i \in s} b_i\right) $$ where $\text{single}(x, y)$ denotes the element of $k[G]$ that is $y$ at $x$ and zero elsewhere.

AddMonoidAlgebra.isLocalHom_singleZeroRingHom instance

[Semiring k] [AddMonoid G] : IsLocalHom (singleZeroRingHom (k := k) (G := G))

Full source

instance isLocalHom_singleZeroRingHom [Semiring k] [AddMonoid G] :
    IsLocalHom (singleZeroRingHom (k := k) (G := G)) :=
  MonoidAlgebra.isLocalHom_singleOneRingHom (G := Multiplicative G)

The embedding $k \to k[G]$ via the zero element is a local homomorphism

Informal description

For any semiring $k$ and additive monoid $G$, the ring homomorphism $\text{singleZeroRingHom} \colon k \to k[G]$ that maps $b \in k$ to $\text{single}(0_G, b) \in k[G]$ is a local homomorphism. That is, for any $b \in k$, if $\text{single}(0_G, b)$ is a unit in $k[G]$, then $b$ is a unit in $k$.

Notation

Implementation note