doc-next-gen

Mathlib.Algebra.MonoidAlgebra.Basic

Module docstring

{"# Monoid algebras

","### Multiplicative monoids ","#### Non-unital, non-associative algebra structure ","#### Algebra structure ","#### Non-unital, non-associative algebra structure ","#### Algebra structure "}

MonoidAlgebra.nonUnitalAlgHom_ext theorem
[DistribMulAction k A] {φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A} (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂
Full source 
/-- A non_unital `k`-algebra homomorphism from `MonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`. -/
theorem nonUnitalAlgHom_ext [DistribMulAction k A] {φ₁ φ₂ : MonoidAlgebraMonoidAlgebra k G →ₙₐ[k] A}
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  NonUnitalAlgHom.to_distribMulActionHom_injective <|
    Finsupp.distribMulActionHom_ext' fun a => DistribMulActionHom.ext_ring (h a)
Uniqueness of Non-unital Algebra Homomorphisms on Monoid Algebras via Single Generators
Informal description
Let $k$ be a semiring and $G$ a monoid. For any two non-unital $k$-algebra homomorphisms $\phi_1, \phi_2 \colon k[G] \to A$ (where $A$ is a non-unital $k$-algebra), if $\phi_1$ and $\phi_2$ agree on all elements of the form $\text{single}(x, 1)$ for $x \in G$, then $\phi_1 = \phi_2$.
MonoidAlgebra.nonUnitalAlgHom_ext' theorem
[DistribMulAction k A] {φ₁ φ₂ : MonoidAlgebra k G →ₙₐ[k] A} (h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G)) : φ₁ = φ₂
Full source 
/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem nonUnitalAlgHom_ext' [DistribMulAction k A] {φ₁ φ₂ : MonoidAlgebraMonoidAlgebra k G →ₙₐ[k] A}
    (h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G)) : φ₁ = φ₂ :=
  nonUnitalAlgHom_ext k <| DFunLike.congr_fun h
Uniqueness of Non-unital Algebra Homomorphisms via Composition with Canonical Embedding
Informal description
Let $k$ be a semiring and $G$ a multiplicative magma. For any two non-unital $k$-algebra homomorphisms $\phi_1, \phi_2 \colon k[G] \to A$ (where $A$ is a non-unital $k$-algebra), if the compositions of $\phi_1$ and $\phi_2$ with the canonical embedding $\text{ofMagma}_k \colon G \to k[G]$ are equal, then $\phi_1 = \phi_2$.
MonoidAlgebra.liftMagma definition
[Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (G →ₙ* A) ≃ (MonoidAlgebra k G →ₙₐ[k] A)
Full source 
/-- The functor `G ↦ MonoidAlgebra k G`, from the category of magmas to the category of non-unital,
non-associative algebras over `k` is adjoint to the forgetful functor in the other direction. -/
@[simps apply_apply symm_apply]
def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :
    (G →ₙ* A) ≃ (MonoidAlgebra k G →ₙₐ[k] A) where
  toFun f :=
    { liftAddHom fun x => (smulAddHom k A).flip (f x) with
      toFun := fun a => a.sum fun m t => t • f m
      map_smul' := fun t' a => by
        rw [Finsupp.smul_sum, sum_smul_index']
        · simp_rw [smul_assoc, MonoidHom.id_apply]
        · intro m
          exact zero_smul k (f m)
      map_mul' := fun a₁ a₂ => by
        let g : G → k → A := fun m t => t • f m
        have h₁ : ∀ m, g m 0 = 0 := by
          intro m
          exact zero_smul k (f m)
        have h₂ : ∀ (m) (t₁ t₂ : k), g m (t₁ + t₂) = g m t₁ + g m t₂ := by
          intros
          rw [← add_smul]
        -- Porting note: `reducible` cannot be `local` so proof gets long.
        simp_rw [Finsupp.mul_sum, Finsupp.sum_mul, smul_mul_smul_comm, ← f.map_mul, mul_def,
          sum_comm a₂ a₁]
        rw [sum_sum_index h₁ h₂]; congr; ext
        rw [sum_sum_index h₁ h₂]; congr; ext
        rw [sum_single_index (h₁ _)] }
  invFun F := F.toMulHom.comp (ofMagma k G)
  left_inv f := by
    ext m
    simp only [NonUnitalAlgHom.coe_mk, ofMagma_apply, NonUnitalAlgHom.toMulHom_eq_coe,
      sum_single_index, Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp,
      NonUnitalAlgHom.coe_to_mulHom]
  right_inv F := by
    ext m
    simp only [NonUnitalAlgHom.coe_mk, ofMagma_apply, NonUnitalAlgHom.toMulHom_eq_coe,
      sum_single_index, Function.comp_apply, one_smul, zero_smul, MulHom.coe_comp,
      NonUnitalAlgHom.coe_to_mulHom]
Adjunction between magma homomorphisms and monoid algebra homomorphisms
Informal description
Given a semiring $k$, a magma $G$, and a $k$-module $A$ where the scalar multiplication operations of $k$ and $A$ on $A$ form a tower and commute with each other, there is a natural bijection between: 1. Non-unital multiplicative homomorphisms from $G$ to $A$ (i.e., maps preserving multiplication but not necessarily the identity), and 2. Non-unital $k$-algebra homomorphisms from the monoid algebra $k[G]$ to $A$. The bijection is constructed as follows: - **Forward direction**: Given a non-unital multiplicative homomorphism $f : G \to A$, the corresponding algebra homomorphism $\phi : k[G] \to A$ is defined by $\phi(\sum_{g \in G} c_g g) = \sum_{g \in G} c_g \cdot f(g)$, where $c_g \in k$ are coefficients with finite support. - **Backward direction**: Given a non-unital $k$-algebra homomorphism $F : k[G] \to A$, the corresponding multiplicative homomorphism is obtained by restricting $F$ to the canonical embedding of $G$ in $k[G]$. This establishes an adjunction between the functor $G \mapsto k[G]$ (from magmas to non-unital $k$-algebras) and the forgetful functor in the opposite direction.
MonoidAlgebra.algebra instance
{A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : Algebra k (MonoidAlgebra A G)
Full source 
/-- The instance `Algebra k (MonoidAlgebra A G)` whenever we have `Algebra k A`.

In particular this provides the instance `Algebra k (MonoidAlgebra k G)`.
-/
instance algebra {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    Algebra k (MonoidAlgebra A G) where
  algebraMap := singleOneRingHom.comp (algebraMap k A)
  smul_def' := fun r a => by
    ext
    rw [Finsupp.coe_smul]
    simp [single_one_mul_apply, Algebra.smul_def, Pi.smul_apply]
  commutes' := fun r f => by
    refine Finsupp.ext fun _ => ?_
    simp [single_one_mul_apply, mul_single_one_apply, Algebra.commutes]
Algebra Structure on Monoid Algebras via Coefficient Extension
Informal description
For any commutative semiring $k$, semiring $A$ with an algebra structure over $k$, and monoid $G$, the monoid algebra $A[G]$ inherits an algebra structure over $k$. This structure is defined such that the algebra map $k \to A[G]$ is given by composing the algebra map $k \to A$ with the embedding of $A$ into $A[G]$ that sends $a \in A$ to $\text{single}(1_G, a)$, where $1_G$ is the identity element of $G$.
MonoidAlgebra.singleOneAlgHom definition
{A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : A →ₐ[k] MonoidAlgebra A G
Full source 
/-- `Finsupp.single 1` as an `AlgHom` -/
@[simps! apply]
def singleOneAlgHom {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    A →ₐ[k] MonoidAlgebra A G :=
  { singleOneRingHom with
    commutes' := fun r => by
      ext
      simp
      rfl }
Algebra homomorphism embedding coefficients into monoid algebra via identity element
Informal description
The algebra homomorphism $\text{singleOneAlgHom} \colon A \to A[G]$ from a semiring $A$ (which is an algebra over a commutative semiring $k$) to the monoid algebra $A[G]$ maps each element $a \in A$ to the monoid algebra element $\text{single}(1_G, a)$, where $1_G$ is the multiplicative identity of $G$. This homomorphism preserves the algebra structure, meaning it commutes with the scalar multiplication by elements of $k$.
MonoidAlgebra.coe_algebraMap theorem
{A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : ⇑(algebraMap k (MonoidAlgebra A G)) = single 1 ∘ algebraMap k A
Full source 
@[simp]
theorem coe_algebraMap {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    ⇑(algebraMap k (MonoidAlgebra A G)) = singlesingle 1 ∘ algebraMap k A :=
  rfl
Algebra Map Characterization for Monoid Algebras
Informal description
For a commutative semiring $k$, a semiring $A$ with an algebra structure over $k$, and a monoid $G$, the algebra map $\text{algebraMap}_k : k \to \text{MonoidAlgebra}(A, G)$ is given by the composition of the algebra map $k \to A$ with the function $\text{single}(1_G, -)$, where $1_G$ is the identity element of $G$. In other words, for any $b \in k$, we have $\text{algebraMap}_k(b) = \text{single}(1_G, \text{algebraMap}_k(b))$.
MonoidAlgebra.single_eq_algebraMap_mul_of theorem
[CommSemiring k] [Monoid G] (a : G) (b : k) : single a b = algebraMap k (MonoidAlgebra k G) b * of k G a
Full source 
theorem single_eq_algebraMap_mul_of [CommSemiring k] [Monoid G] (a : G) (b : k) :
    single a b = algebraMap k (MonoidAlgebra k G) b * of k G a := by simp
Decomposition of Single Generator in Monoid Algebra: $\text{single}(a, b) = \text{algebraMap}_k(b) \cdot \text{of}_k(a)$
Informal description
Let $k$ be a commutative semiring and $G$ a monoid. For any element $a \in G$ and any scalar $b \in k$, the element $\text{single}(a, b)$ in the monoid algebra $k[G]$ can be expressed as the product of the algebra map $\text{algebraMap}_k(b)$ and the image of $a$ under the canonical embedding $\text{of}_k(a)$. That is, $$\text{single}(a, b) = \text{algebraMap}_k(b) \cdot \text{of}_k(a).$$
MonoidAlgebra.single_algebraMap_eq_algebraMap_mul_of theorem
{A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] (a : G) (b : k) : single a (algebraMap k A b) = algebraMap k (MonoidAlgebra A G) b * of A G a
Full source 
theorem single_algebraMap_eq_algebraMap_mul_of {A : Type*} [CommSemiring k] [Semiring A]
    [Algebra k A] [Monoid G] (a : G) (b : k) :
    single a (algebraMap k A b) = algebraMap k (MonoidAlgebra A G) b * of A G a := by simp
Decomposition of Single Generator via Algebra Map in Monoid Algebra
Informal description
Let $k$ be a commutative semiring, $A$ a semiring with an algebra structure over $k$, and $G$ a monoid. For any element $a \in G$ and $b \in k$, the element $\text{single}(a, \text{algebraMap}_k(b))$ in the monoid algebra $A[G]$ equals the product of $\text{algebraMap}_k(b)$ (viewed as an element of $A[G]$) and the image of $a$ under the canonical embedding $\text{of} : G \to A[G]$. In other words, we have: $$\text{single}(a, \text{algebraMap}_k(b)) = \text{algebraMap}_k(b) \cdot \text{of}(a).$$
MonoidAlgebra.isLocalHom_singleOneAlgHom instance
{A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] : IsLocalHom (singleOneAlgHom : A →ₐ[k] MonoidAlgebra A G)
Full source 
instance isLocalHom_singleOneAlgHom
    {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] :
    IsLocalHom (singleOneAlgHom : A →ₐ[k] MonoidAlgebra A G) where
  map_nonunit := isLocalHom_singleOneRingHom.map_nonunit
Local Homomorphism Property of the Coefficient Embedding in Monoid Algebras
Informal description
For any commutative semiring $k$, semiring $A$ with an algebra structure over $k$, and monoid $G$, the algebra homomorphism $\text{singleOneAlgHom} \colon A \to A[G]$ that maps $a \in A$ to $\text{single}(1_G, a) \in A[G]$ is a local homomorphism. That is, for any $a \in A$, if $\text{single}(1_G, a)$ is a unit in $A[G]$, then $a$ is a unit in $A$.
MonoidAlgebra.isLocalHom_algebraMap instance
{A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G] [IsLocalHom (algebraMap k A)] : IsLocalHom (algebraMap k (MonoidAlgebra A G))
Full source 
instance isLocalHom_algebraMap
    {A : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G]
    [IsLocalHom (algebraMap k A)] :
    IsLocalHom (algebraMap k (MonoidAlgebra A G)) where
  map_nonunit _ hx := .of_map _ _ <| isLocalHom_singleOneAlgHom (k := k).map_nonunit _ hx
Local Homomorphism Property of the Induced Algebra Map on Monoid Algebras
Informal description
For any commutative semiring $k$, semiring $A$ with an algebra structure over $k$, and monoid $G$, if the algebra map $\text{algebraMap}_k \colon k \to A$ is a local homomorphism, then the induced algebra map $\text{algebraMap}_k \colon k \to A[G]$ to the monoid algebra is also a local homomorphism. That is, for any $b \in k$, if $\text{algebraMap}_k(b)$ is a unit in $A[G]$, then $b$ is a unit in $k$.
MonoidAlgebra.liftNCAlgHom definition
(f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) : MonoidAlgebra A G →ₐ[k] B
Full source 
/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom` -/
def liftNCAlgHom (f : A →ₐ[k] B) (g : G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) :
    MonoidAlgebraMonoidAlgebra A G →ₐ[k] B :=
  { liftNCRingHom (f : A →+* B) g h_comm with
    commutes' := by simp [liftNCRingHom] }
Algebra homomorphism from monoid algebra induced by commuting homomorphisms
Informal description
Given a commutative semiring $k$, semirings $A$ and $B$ with $B$ being a $k$-algebra, and a monoid $G$, for any $k$-algebra homomorphism $f \colon A \to B$ and monoid homomorphism $g \colon G \to B$ such that $f(x)$ and $g(y)$ commute for all $x \in A$ and $y \in G$, the function $\text{liftNCAlgHom}(f, g) \colon A[G] \to B$ is the $k$-algebra homomorphism from the monoid algebra $A[G]$ to $B$ defined by linearly extending the map $\text{single}(a, b) \mapsto f(b) \cdot g(a)$ for all $a \in G$ and $b \in A$. More explicitly, for any finitely supported function $\varphi \in A[G]$, we have: \[ \text{liftNCAlgHom}(f, g)(\varphi) = \sum_{a \in \text{supp}(\varphi)} f(\varphi(a)) \cdot g(a). \] This homomorphism preserves both the $k$-algebra structure and the convolution product structure of the monoid algebra.
MonoidAlgebra.algHom_ext theorem
⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄ (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂
Full source 
/-- A `k`-algebra homomorphism from `MonoidAlgebra k G` is uniquely defined by its
values on the functions `single a 1`. -/
theorem algHom_ext ⦃φ₁ φ₂ : MonoidAlgebraMonoidAlgebra k G →ₐ[k] A⦄
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  AlgHom.toLinearMap_injective <| Finsupp.lhom_ext' fun a => LinearMap.ext_ring (h a)
Uniqueness of Algebra Homomorphisms on Monoid Algebras via Single Generators
Informal description
Let $k$ be a commutative semiring, $G$ a monoid, and $A$ a $k$-algebra. For any two $k$-algebra homomorphisms $\varphi_1, \varphi_2 \colon k[G] \to A$, if $\varphi_1(\text{single}(x, 1)) = \varphi_2(\text{single}(x, 1))$ for all $x \in G$, then $\varphi_1 = \varphi_2$.
MonoidAlgebra.algHom_ext' theorem
⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄ (h : (φ₁ : MonoidAlgebra k G →* A).comp (of k G) = (φ₂ : MonoidAlgebra k G →* A).comp (of k G)) : φ₁ = φ₂
Full source 
/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem algHom_ext' ⦃φ₁ φ₂ : MonoidAlgebraMonoidAlgebra k G →ₐ[k] A⦄
    (h :
      (φ₁ : MonoidAlgebraMonoidAlgebra k G →* A).comp (of k G) = (φ₂ : MonoidAlgebraMonoidAlgebra k G →* A).comp (of k G)) :
    φ₁ = φ₂ :=
  algHom_ext <| DFunLike.congr_fun h
Uniqueness of Algebra Homomorphisms on Monoid Algebras via Composition with Embedding
Informal description
Let $k$ be a commutative semiring, $G$ a monoid, and $A$ a $k$-algebra. For any two $k$-algebra homomorphisms $\varphi_1, \varphi_2 \colon k[G] \to A$, if the compositions of $\varphi_1$ and $\varphi_2$ with the embedding $\text{of} \colon G \to k[G]$ are equal as monoid homomorphisms, then $\varphi_1 = \varphi_2$.
MonoidAlgebra.lift definition
: (G →* A) ≃ (MonoidAlgebra k G →ₐ[k] A)
Full source 
/-- Any monoid homomorphism `G →* A` can be lifted to an algebra homomorphism
`MonoidAlgebra k G →ₐ[k] A`. -/
def lift : (G →* A) ≃ (MonoidAlgebra k G →ₐ[k] A) where
  invFun f := (f : MonoidAlgebraMonoidAlgebra k G →* A).comp (of k G)
  toFun F := liftNCAlgHom (Algebra.ofId k A) F fun _ _ => Algebra.commutes _ _
  left_inv f := by
    ext
    simp [liftNCAlgHom, liftNCRingHom]
  right_inv F := by
    ext
    simp [liftNCAlgHom, liftNCRingHom]
Lifting monoid homomorphisms to algebra homomorphisms on monoid algebras
Informal description
Given a commutative semiring $k$, a monoid $G$, and a $k$-algebra $A$, there is a natural equivalence between monoid homomorphisms $G \to^* A$ and $k$-algebra homomorphisms $\text{MonoidAlgebra}\ k\ G \toₐ[k] A$. More precisely, the equivalence is constructed as follows: - The forward direction lifts a monoid homomorphism $F \colon G \to^* A$ to an algebra homomorphism by linearly extending the map $\text{single}(a, b) \mapsto b \cdot F(a)$. - The backward direction restricts an algebra homomorphism $\varphi \colon \text{MonoidAlgebra}\ k\ G \toₐ[k] A$ to the monoid $G$ via the embedding $\text{of}\ k\ G \colon G \to^* \text{MonoidAlgebra}\ k\ G$. This equivalence satisfies the property that for any monoid homomorphism $F \colon G \to^* A$ and any element $f \in \text{MonoidAlgebra}\ k\ G$, the lifted homomorphism evaluates as: \[ \text{lift}\ k\ G\ A\ F\ f = \sum_{a \in \text{supp}(f)} f(a) \cdot F(a). \]
MonoidAlgebra.lift_apply' theorem
(F : G →* A) (f : MonoidAlgebra k G) : lift k G A F f = f.sum fun a b => algebraMap k A b * F a
Full source 
theorem lift_apply' (F : G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => algebraMap k A b * F a :=
  rfl
Evaluation of Lifted Algebra Homomorphism on Monoid Algebra Elements
Informal description
Let $k$ be a commutative semiring, $G$ a monoid, and $A$ a $k$-algebra. For any monoid homomorphism $F \colon G \to A$ and any element $f \in k[G]$, the evaluation of the lifted algebra homomorphism $\text{lift}_{k,G,A}(F)$ at $f$ is given by: \[ \text{lift}_{k,G,A}(F)(f) = \sum_{(a,b) \in \text{supp}(f)} \text{algebraMap}_k^A(b) \cdot F(a), \] where $\text{algebraMap}_k^A \colon k \to A$ is the canonical algebra map and $\text{supp}(f)$ denotes the support of $f$.
MonoidAlgebra.lift_apply theorem
(F : G →* A) (f : MonoidAlgebra k G) : lift k G A F f = f.sum fun a b => b • F a
Full source 
theorem lift_apply (F : G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => b • F a := by simp only [lift_apply', Algebra.smul_def]
Evaluation of Lifted Algebra Homomorphism on Monoid Algebra Elements
Informal description
Given a commutative semiring $k$, a monoid $G$, a $k$-algebra $A$, and a monoid homomorphism $F \colon G \to A$, the evaluation of the lifted algebra homomorphism $\text{lift}_{k,G,A}(F)$ at an element $f \in k[G]$ is equal to the sum over the support of $f$ of the scalar multiples $b \cdot F(a)$, where $f(a) = b$ for each $a \in G$. In symbols: \[ \text{lift}_{k,G,A}(F)(f) = \sum_{a \in \text{supp}(f)} b \cdot F(a) \quad \text{where} \quad f(a) = b. \]
MonoidAlgebra.lift_def theorem
(F : G →* A) : ⇑(lift k G A F) = liftNC ((algebraMap k A : k →+* A) : k →+ A) F
Full source 
theorem lift_def (F : G →* A) : ⇑(lift k G A F) = liftNC ((algebraMap k A : k →+* A) : k →+ A) F :=
  rfl
Definition of the lift homomorphism for monoid algebras via non-commutative lift
Informal description
Given a commutative semiring $k$, a monoid $G$, and a $k$-algebra $A$, for any monoid homomorphism $F \colon G \to A$, the algebra homomorphism $\text{lift}_{k,G,A}(F) \colon k[G] \to A$ is equal to the non-commutative lift $\text{liftNC}$ applied to the additive homomorphism $\text{algebraMap}_{k,A} \colon k \to A$ and $F$. More precisely, for any $f \in k[G]$, we have: \[ \text{lift}_{k,G,A}(F)(f) = \sum_{a \in \text{supp}(f)} f(a) \cdot F(a) \] where $\text{algebraMap}_{k,A}$ is the canonical $k$-algebra structure map on $A$.
MonoidAlgebra.lift_symm_apply theorem
(F : MonoidAlgebra k G →ₐ[k] A) (x : G) : (lift k G A).symm F x = F (single x 1)
Full source 
@[simp]
theorem lift_symm_apply (F : MonoidAlgebraMonoidAlgebra k G →ₐ[k] A) (x : G) :
    (lift k G A).symm F x = F (single x 1) :=
  rfl
Inverse Lifting Formula for Monoid Algebra Homomorphisms
Informal description
Given a commutative semiring $k$, a monoid $G$, and a $k$-algebra $A$, for any $k$-algebra homomorphism $F \colon k[G] \to A$ and any element $x \in G$, the inverse of the lifting equivalence applied to $F$ evaluated at $x$ equals $F$ applied to the monoid algebra element $\text{single}(x, 1)$, i.e., \[ \text{lift}_{k,G,A}^{-1}(F)(x) = F(\text{single}(x, 1)). \]
MonoidAlgebra.lift_single theorem
(F : G →* A) (a b) : lift k G A F (single a b) = b • F a
Full source 
@[simp]
theorem lift_single (F : G →* A) (a b) : lift k G A F (single a b) = b • F a := by
  rw [lift_def, liftNC_single, Algebra.smul_def, AddMonoidHom.coe_coe]
Evaluation of Lifted Homomorphism on Single Generator: $\text{lift}(F)(\text{single}(a, b)) = b \cdot F(a)$
Informal description
Let $k$ be a commutative semiring, $G$ a monoid, and $A$ a $k$-algebra. For any monoid homomorphism $F \colon G \to A$ and elements $a \in G$, $b \in k$, the lifted algebra homomorphism $\text{lift}_{k,G,A}(F)$ applied to the monoid algebra element $\text{single}(a, b)$ satisfies: \[ \text{lift}_{k,G,A}(F)(\text{single}(a, b)) = b \cdot F(a). \]
MonoidAlgebra.lift_of theorem
(F : G →* A) (x) : lift k G A F (of k G x) = F x
Full source 
theorem lift_of (F : G →* A) (x) : lift k G A F (of k G x) = F x := by simp
Lifted Homomorphism Preserves Canonical Embedding: $\text{lift}(F)(\text{of}(x)) = F(x)$
Informal description
Let $k$ be a commutative semiring, $G$ a monoid, and $A$ a $k$-algebra. For any monoid homomorphism $F \colon G \to A$ and any element $x \in G$, the lifted algebra homomorphism $\text{lift}_{k,G,A}(F)$ applied to the canonical embedding $\text{of}_{k,G}(x)$ equals $F(x)$, i.e., \[ \text{lift}_{k,G,A}(F)(\text{of}_{k,G}(x)) = F(x). \]
MonoidAlgebra.lift_unique' theorem
(F : MonoidAlgebra k G →ₐ[k] A) : F = lift k G A ((F : MonoidAlgebra k G →* A).comp (of k G))
Full source 
theorem lift_unique' (F : MonoidAlgebraMonoidAlgebra k G →ₐ[k] A) :
    F = lift k G A ((F : MonoidAlgebraMonoidAlgebra k G →* A).comp (of k G)) :=
  ((lift k G A).apply_symm_apply F).symm
Uniqueness of Algebra Homomorphisms from Monoid Algebras via Lifting
Informal description
Let $k$ be a commutative semiring, $G$ a monoid, and $A$ a $k$-algebra. For any $k$-algebra homomorphism $F \colon k[G] \to A$, the homomorphism $F$ is uniquely determined by its composition with the canonical embedding $\text{of} \colon G \to k[G]$. Specifically, $F$ equals the lift of the monoid homomorphism $(F \circ \text{of}) \colon G \to A$.
MonoidAlgebra.lift_unique theorem
(F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) : F f = f.sum fun a b => b • F (single a 1)
Full source 
/-- Decomposition of a `k`-algebra homomorphism from `MonoidAlgebra k G` by
its values on `F (single a 1)`. -/
theorem lift_unique (F : MonoidAlgebraMonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G) :
    F f = f.sum fun a b => b • F (single a 1) := by
  conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
Uniqueness of Algebra Homomorphisms on Monoid Algebras via Single Generators
Informal description
Let $k$ be a commutative semiring, $G$ a monoid, and $A$ a $k$-algebra. For any $k$-algebra homomorphism $F \colon k[G] \to A$ and any element $f \in k[G]$, the value of $F$ at $f$ is given by the sum over the support of $f$ of the scalar multiples $b \cdot F(\text{single}(a, 1))$, where $f(a) = b$ for each $a \in G$. In symbols: \[ F(f) = \sum_{a \in \text{supp}(f)} b \cdot F(\text{single}(a, 1)) \quad \text{where} \quad f(a) = b. \]
MonoidAlgebra.mapDomainNonUnitalAlgHom definition
(k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] {G H F : Type*} [Mul G] [Mul H] [FunLike F G H] [MulHomClass F G H] (f : F) : MonoidAlgebra A G →ₙₐ[k] MonoidAlgebra A H
Full source 
/-- If `f : G → H` is a homomorphism between two magmas, then
`Finsupp.mapDomain f` is a non-unital algebra homomorphism between their magma algebras. -/
@[simps apply]
def mapDomainNonUnitalAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A]
    {G H F : Type*} [Mul G] [Mul H] [FunLike F G H] [MulHomClass F G H] (f : F) :
    MonoidAlgebraMonoidAlgebra A G →ₙₐ[k] MonoidAlgebra A H :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebraMonoidAlgebra A G →+ MonoidAlgebra A H) with
    map_mul' := fun x y => mapDomain_mul f x y
    map_smul' := fun r x => mapDomain_smul r x }
Non-unital algebra homomorphism induced by domain mapping of monoid algebras
Informal description
Given a commutative semiring \( k \), a semiring \( A \) with an algebra structure over \( k \), and multiplicative magmas \( G \) and \( H \), for any multiplicative homomorphism \( f \colon G \to H \), the function `MonoidAlgebra.mapDomainNonUnitalAlgHom` is the non-unital algebra homomorphism from the monoid algebra \( A[G] \) to \( A[H] \) induced by mapping the domain via \( f \). Explicitly, it maps a finitely supported function \( v \in A[G] \) to its image under domain mapping by \( f \), i.e., \( \text{mapDomain}\, f\, v \), and satisfies: - **Multiplicativity**: \( \text{mapDomain}\, f\, (x * y) = (\text{mapDomain}\, f\, x) * (\text{mapDomain}\, f\, y) \) for all \( x, y \in A[G] \). - **Linearity over \( k \)**: \( \text{mapDomain}\, f\, (r \cdot x) = r \cdot (\text{mapDomain}\, f\, x) \) for all \( r \in k \) and \( x \in A[G] \).
MonoidAlgebra.mapDomain_algebraMap theorem
{F : Type*} [FunLike F G H] [MonoidHomClass F G H] (f : F) (r : k) : mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r
Full source 
theorem mapDomain_algebraMap {F : Type*} [FunLike F G H] [MonoidHomClass F G H] (f : F) (r : k) :
    mapDomain f (algebraMap k (MonoidAlgebra A G) r) = algebraMap k (MonoidAlgebra A H) r := by
  simp only [coe_algebraMap, mapDomain_single, map_one, (· ∘ ·)]
Compatibility of Domain Mapping with Algebra Maps in Monoid Algebras
Informal description
Let $k$ be a commutative semiring, $A$ a semiring with an algebra structure over $k$, and $G$, $H$ monoids. For any monoid homomorphism $f \colon G \to H$ and any element $r \in k$, the image under the domain mapping map $\text{mapDomain}\, f$ of the algebra map $\text{algebraMap}\, k\, (A[G])\, r$ equals the algebra map $\text{algebraMap}\, k\, (A[H])\, r$. In other words, the following diagram commutes: $$\text{algebraMap}\, k\, (A[G])\, r \xrightarrow{\text{mapDomain}\, f} \text{algebraMap}\, k\, (A[H])\, r$$
MonoidAlgebra.mapDomainAlgHom definition
(k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] {H F : Type*} [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) : MonoidAlgebra A G →ₐ[k] MonoidAlgebra A H
Full source 
/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`Finsupp.mapDomain f` is an algebra homomorphism between their monoid algebras. -/
@[simps!]
def mapDomainAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] {H F : Type*}
    [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
    MonoidAlgebraMonoidAlgebra A G →ₐ[k] MonoidAlgebra A H :=
  { mapDomainRingHom A f with commutes' := mapDomain_algebraMap A f }
Algebra homomorphism between monoid algebras induced by a monoid homomorphism
Informal description
Given a commutative semiring $k$, a semiring $A$ with an algebra structure over $k$, and monoids $G$ and $H$, for any monoid homomorphism $f \colon G \to H$, the function `MonoidAlgebra.mapDomainAlgHom` is the algebra homomorphism from the monoid algebra $A[G]$ to $A[H]$ induced by mapping the domain via $f$. Explicitly, it maps a finitely supported function $v \in A[G]$ to its image under domain mapping by $f$, i.e., $\text{mapDomain}\, f\, v$, and satisfies: - **Multiplicativity**: $\text{mapDomain}\, f\, (x * y) = (\text{mapDomain}\, f\, x) * (\text{mapDomain}\, f\, y)$ for all $x, y \in A[G]$. - **Additivity**: $\text{mapDomain}\, f\, (x + y) = \text{mapDomain}\, f\, x + \text{mapDomain}\, f\, y$ for all $x, y \in A[G]$. - **Preservation of scalar multiplication**: $\text{mapDomain}\, f\, (r \cdot x) = r \cdot (\text{mapDomain}\, f\, x)$ for all $r \in k$ and $x \in A[G]$. - **Preservation of multiplicative identity**: $\text{mapDomain}\, f\, 1 = 1$.
MonoidAlgebra.mapDomainAlgHom_id theorem
(k A) [CommSemiring k] [Semiring A] [Algebra k A] : mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G)
Full source 
@[simp]
lemma mapDomainAlgHom_id (k A) [CommSemiring k] [Semiring A] [Algebra k A] :
    mapDomainAlgHom k A (MonoidHom.id G) = AlgHom.id k (MonoidAlgebra A G) := by
  ext; simp [MonoidHom.id, ← Function.id_def]
Identity Monoid Homomorphism Induces Identity Algebra Homomorphism on Monoid Algebras
Informal description
Let $k$ be a commutative semiring and $A$ a semiring with an algebra structure over $k$. For any monoid $G$, the algebra homomorphism induced by the identity monoid homomorphism $\text{id}_G \colon G \to G$ is equal to the identity algebra homomorphism on the monoid algebra $A[G]$. That is, $\text{mapDomainAlgHom}\, k\, A\, \text{id}_G = \text{AlgHom.id}\, k\, (A[G])$.
MonoidAlgebra.mapDomainAlgHom_comp theorem
(k A) {G₁ G₂ G₃} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G₁] [Monoid G₂] [Monoid G₃] (f : G₁ →* G₂) (g : G₂ →* G₃) : mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)
Full source 
@[simp]
lemma mapDomainAlgHom_comp (k A) {G₁ G₂ G₃} [CommSemiring k] [Semiring A] [Algebra k A]
    [Monoid G₁] [Monoid G₂] [Monoid G₃] (f : G₁ →* G₂) (g : G₂ →* G₃) :
    mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f) := by
  ext; simp [mapDomain_comp]
Composition of Algebra Homomorphisms on Monoid Algebras via Monoid Homomorphism Composition
Informal description
Let $k$ be a commutative semiring, $A$ a semiring with an algebra structure over $k$, and $G_1$, $G_2$, $G_3$ monoids. For any monoid homomorphisms $f \colon G_1 \to G_2$ and $g \colon G_2 \to G_3$, the algebra homomorphism between monoid algebras induced by the composition $g \circ f$ equals the composition of the algebra homomorphisms induced by $g$ and $f$ respectively. That is: \[ \text{mapDomainAlgHom}\, k\, A\, (g \circ f) = (\text{mapDomainAlgHom}\, k\, A\, g) \circ (\text{mapDomainAlgHom}\, k\, A\, f). \]
MonoidAlgebra.domCongr definition
(e : G ≃* H) : MonoidAlgebra A G ≃ₐ[k] MonoidAlgebra A H
Full source 
/-- If `e : G ≃* H` is a multiplicative equivalence between two monoids, then
`MonoidAlgebra.domCongr e` is an algebra equivalence between their monoid algebras. -/
def domCongr (e : G ≃* H) : MonoidAlgebraMonoidAlgebra A G ≃ₐ[k] MonoidAlgebra A H :=
  AlgEquiv.ofLinearEquiv
    (Finsupp.domLCongr e : (G →₀ A) ≃ₗ[k] (H →₀ A))
    ((equivMapDomain_eq_mapDomain _ _).trans <| mapDomain_one e)
    (fun f g => (equivMapDomain_eq_mapDomain _ _).trans <| (mapDomain_mul e f g).trans <|
        congr_arg₂ _ (equivMapDomain_eq_mapDomain _ _).symm (equivMapDomain_eq_mapDomain _ _).symm)
Algebra equivalence of monoid algebras induced by a multiplicative equivalence
Informal description
Given a commutative semiring $k$, a semiring $A$ with an algebra structure over $k$, and a multiplicative equivalence $e : G \simeq^* H$ between monoids $G$ and $H$, the function `MonoidAlgebra.domCongr e` defines an algebra equivalence between the monoid algebras $A[G]$ and $A[H]$. This equivalence maps a finitely supported function $f : G \to_0 A$ to the function $H \to_0 A$ given by $h \mapsto f(e^{-1}(h))$, and preserves both the algebra and multiplicative structures.
MonoidAlgebra.domCongr_toAlgHom theorem
(e : G ≃* H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e
Full source 
theorem domCongr_toAlgHom (e : G ≃* H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e :=
  AlgHom.ext fun _ => equivMapDomain_eq_mapDomain _ _
Algebra homomorphism component of monoid algebra equivalence equals domain mapping homomorphism
Informal description
Given a commutative semiring $k$, a semiring $A$ with an algebra structure over $k$, and a multiplicative equivalence $e : G \simeq^* H$ between monoids $G$ and $H$, the algebra homomorphism component of the algebra equivalence $\text{domCongr}_k^A e$ between the monoid algebras $A[G]$ and $A[H]$ is equal to the algebra homomorphism $\text{mapDomainAlgHom}_k^A e$ induced by $e$.
MonoidAlgebra.domCongr_apply theorem
(e : G ≃* H) (f : MonoidAlgebra A G) (h : H) : domCongr k A e f h = f (e.symm h)
Full source 
@[simp] theorem domCongr_apply (e : G ≃* H) (f : MonoidAlgebra A G) (h : H) :
    domCongr k A e f h = f (e.symm h) :=
  rfl
Evaluation of Monoid Algebra Equivalence Induced by Group Isomorphism
Informal description
Given a commutative semiring $k$, a semiring $A$ with an algebra structure over $k$, and a multiplicative equivalence $e : G \simeq^* H$ between monoids $G$ and $H$, the algebra equivalence $\text{domCongr}_k^A e$ between the monoid algebras $A[G]$ and $A[H]$ satisfies \[ (\text{domCongr}_k^A e)(f)(h) = f(e^{-1}(h)) \] for any finitely supported function $f \in A[G]$ and any element $h \in H$.
MonoidAlgebra.domCongr_support theorem
(e : G ≃* H) (f : MonoidAlgebra A G) : (domCongr k A e f).support = f.support.map e
Full source 
@[simp] theorem domCongr_support (e : G ≃* H) (f : MonoidAlgebra A G) :
    (domCongr k A e f).support = f.support.map e :=
  rfl
Support Preservation under Monoid Algebra Equivalence Induced by Multiplicative Equivalence
Informal description
Let $k$ be a commutative semiring, $A$ a semiring with an algebra structure over $k$, and $G$, $H$ monoids. Given a multiplicative equivalence $e : G \simeq^* H$ and an element $f \in A[G]$, the support of the image of $f$ under the algebra equivalence $\text{domCongr}\,k\,A\,e : A[G] \simeq A[H]$ is equal to the image of the support of $f$ under the injective map induced by $e$. That is: $$\text{supp}(\text{domCongr}\,k\,A\,e\,f) = e(\text{supp}(f))$$ where $\text{supp}(f)$ denotes the finite support of $f$ (the set of elements where $f$ is non-zero).
MonoidAlgebra.domCongr_single theorem
(e : G ≃* H) (g : G) (a : A) : domCongr k A e (single g a) = single (e g) a
Full source 
@[simp] theorem domCongr_single (e : G ≃* H) (g : G) (a : A) :
    domCongr k A e (single g a) = single (e g) a :=
  Finsupp.equivMapDomain_single _ _ _
Preservation of Single Generators under Monoid Algebra Equivalence
Informal description
Given a multiplicative equivalence $e \colon G \simeq^* H$ between monoids $G$ and $H$, and elements $g \in G$ and $a \in A$, the algebra equivalence $\text{domCongr}_{k,A}(e)$ maps the single generator $\text{single}(g, a) \in A[G]$ to $\text{single}(e(g), a) \in A[H]$. In other words, the equivalence preserves single generators by applying $e$ to their monoid elements.
MonoidAlgebra.domCongr_refl theorem
: domCongr k A (MulEquiv.refl G) = AlgEquiv.refl
Full source 
@[simp] theorem domCongr_refl : domCongr k A (MulEquiv.refl G) = AlgEquiv.refl :=
  AlgEquiv.ext fun _ => Finsupp.ext fun _ => rfl
Identity Equivalence Induces Identity Algebra Equivalence on Monoid Algebra
Informal description
For any commutative semiring $k$, semiring $A$ with an algebra structure over $k$, and monoid $G$, the algebra equivalence $\text{domCongr}$ induced by the multiplicative identity isomorphism $\text{MulEquiv.refl}$ on $G$ is equal to the identity algebra equivalence $\text{AlgEquiv.refl}$ on the monoid algebra $A[G]$.
MonoidAlgebra.domCongr_symm theorem
(e : G ≃* H) : (domCongr k A e).symm = domCongr k A e.symm
Full source 
@[simp] theorem domCongr_symm (e : G ≃* H) : (domCongr k A e).symm = domCongr k A e.symm := rfl
Inverse of Monoid Algebra Equivalence Induced by Group Isomorphism
Informal description
Given a commutative semiring $k$, a semiring $A$ with an algebra structure over $k$, and a multiplicative equivalence $e : G \simeq^* H$ between monoids $G$ and $H$, the inverse of the algebra equivalence $\text{domCongr}\,k\,A\,e$ between the monoid algebras $A[G]$ and $A[H]$ is equal to the algebra equivalence $\text{domCongr}\,k\,A\,e^{-1}$ induced by the inverse multiplicative equivalence $e^{-1} : H \simeq^* G$.
MonoidAlgebra.GroupSMul.linearMap definition
[Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) : V →ₗ[k] V
Full source 
/-- When `V` is a `k[G]`-module, multiplication by a group element `g` is a `k`-linear map. -/
def GroupSMul.linearMap [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V]
    [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) : V →ₗ[k] V where
  toFun v := single g (1 : k) • v
  map_add' x y := smul_add (single g (1 : k)) x y
  map_smul' _c _x := smul_algebra_smul_comm _ _ _
Linear action of group elements on a module over a monoid algebra
Informal description
For a monoid $G$, a commutative semiring $k$, and a $k$-module $V$ that is also a $k[G]$-module with compatible scalar multiplications, the function $\text{GroupSMul.linearMap}$ maps each group element $g \in G$ to a $k$-linear endomorphism of $V$. Specifically, for any $v \in V$, this linear map acts by $\text{GroupSMul.linearMap}(g)(v) = \text{single}(g, 1_k) \cdot v$, where $\text{single}(g, 1_k)$ is the element of the monoid algebra $k[G]$ with value $1_k$ at $g$ and zero elsewhere.
MonoidAlgebra.GroupSMul.linearMap_apply theorem
[Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V] [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G) (v : V) : (GroupSMul.linearMap k V g) v = single g (1 : k) • v
Full source 
@[simp]
theorem GroupSMul.linearMap_apply [Monoid G] [CommSemiring k] (V : Type u₃) [AddCommMonoid V]
    [Module k V] [Module (MonoidAlgebra k G) V] [IsScalarTower k (MonoidAlgebra k G) V] (g : G)
    (v : V) : (GroupSMul.linearMap k V g) v = single g (1 : k) • v :=
  rfl
Action of Group Elements via Monoid Algebra Linear Maps
Informal description
Let $G$ be a monoid, $k$ a commutative semiring, and $V$ a $k$-module that is also a module over the monoid algebra $k[G]$ with compatible scalar multiplications. For any group element $g \in G$ and vector $v \in V$, the linear map $\text{GroupSMul.linearMap}(g)$ acts on $v$ as: $$(\text{GroupSMul.linearMap}(g))(v) = \text{single}(g, 1_k) \cdot v$$ where $\text{single}(g, 1_k)$ denotes the element of $k[G]$ with value $1_k$ at $g$ and zero elsewhere.
MonoidAlgebra.equivariantOfLinearOfComm definition
(h : ∀ (g : G) (v : V), f (single g (1 : k) • v) = single g (1 : k) • f v) : V →ₗ[MonoidAlgebra k G] W
Full source 
/-- Build a `k[G]`-linear map from a `k`-linear map and evidence that it is `G`-equivariant. -/
def equivariantOfLinearOfComm
    (h : ∀ (g : G) (v : V), f (single g (1 : k) • v) = single g (1 : k) • f v) :
    V →ₗ[MonoidAlgebra k G] W where
  toFun := f
  map_add' v v' := by simp
  map_smul' c v := by
    refine Finsupp.induction c ?_ ?_
    · simp
    · intro g r c' _nm _nz w
      dsimp at *
      simp only [add_smul, f.map_add, w, add_left_inj, single_eq_algebraMap_mul_of, ← smul_smul]
      rw [algebraMap_smul (MonoidAlgebra k G) r, algebraMap_smul (MonoidAlgebra k G) r, f.map_smul,
        of_apply, h g v]
$G$-equivariant linear map extension from $k$-linear maps
Informal description
Given a $k$-linear map $f \colon V \to W$ between modules over a commutative semiring $k$, where $V$ and $W$ are also modules over the monoid algebra $k[G]$, if $f$ satisfies the $G$-equivariance condition $f(g \cdot v) = g \cdot f(v)$ for all $g \in G$ and $v \in V$ (where $g \cdot v$ denotes the action of $\text{single}(g, 1)$ on $v$), then $f$ extends to a $k[G]$-linear map from $V$ to $W$.
MonoidAlgebra.equivariantOfLinearOfComm_apply theorem
(v : V) : (equivariantOfLinearOfComm f h) v = f v
Full source 
@[simp]
theorem equivariantOfLinearOfComm_apply (v : V) : (equivariantOfLinearOfComm f h) v = f v :=
  rfl
Evaluation of $G$-equivariant linear extension: $\text{equivariantOfLinearOfComm}(f, h)(v) = f(v)$
Informal description
For any vector $v \in V$, the $G$-equivariant linear map $\text{equivariantOfLinearOfComm}(f, h)$ evaluated at $v$ equals $f(v)$.
AddMonoidAlgebra.nonUnitalAlgHom_ext theorem
[DistribMulAction k A] {φ₁ φ₂ : k[G] →ₙₐ[k] A} (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂
Full source 
/-- A non_unital `k`-algebra homomorphism from `k[G]` is uniquely defined by its
values on the functions `single a 1`. -/
theorem nonUnitalAlgHom_ext [DistribMulAction k A] {φ₁ φ₂ : k[G]k[G] →ₙₐ[k] A}
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  @MonoidAlgebra.nonUnitalAlgHom_ext k (Multiplicative G) _ _ _ _ _ φ₁ φ₂ h
Uniqueness of Non-unital Algebra Homomorphisms on Additive Monoid Algebras via Single Generators
Informal description
Let $k$ be a semiring and $G$ an additive monoid. For any two non-unital $k$-algebra homomorphisms $\phi_1, \phi_2 \colon k[G] \to A$ (where $A$ is a non-unital $k$-algebra equipped with a distributive multiplicative action of $k$), if $\phi_1$ and $\phi_2$ agree on all elements of the form $\text{single}(x, 1)$ for $x \in G$, then $\phi_1 = \phi_2$. Here, $\text{single}(x, 1)$ denotes the element of the additive monoid algebra $k[G]$ that is $1$ at $x$ and $0$ elsewhere.
AddMonoidAlgebra.nonUnitalAlgHom_ext' theorem
[DistribMulAction k A] {φ₁ φ₂ : k[G] →ₙₐ[k] A} (h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G)) : φ₁ = φ₂
Full source 
/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem nonUnitalAlgHom_ext' [DistribMulAction k A] {φ₁ φ₂ : k[G]k[G] →ₙₐ[k] A}
    (h : φ₁.toMulHom.comp (ofMagma k G) = φ₂.toMulHom.comp (ofMagma k G)) : φ₁ = φ₂ :=
  @MonoidAlgebra.nonUnitalAlgHom_ext' k (Multiplicative G) _ _ _ _ _ φ₁ φ₂ h
Uniqueness of Non-unital Algebra Homomorphisms via Composition with Canonical Embedding in Additive Monoid Algebra
Informal description
Let $k$ be a semiring and $G$ an additive monoid. For any two non-unital $k$-algebra homomorphisms $\phi_1, \phi_2 \colon k[G] \to A$ (where $A$ is a non-unital $k$-algebra with a distributive multiplicative action of $k$), if the compositions of $\phi_1$ and $\phi_2$ with the canonical embedding $\text{ofMagma}_k \colon \text{Multiplicative}\,G \to k[G]$ are equal, then $\phi_1 = \phi_2$. Here, $\text{ofMagma}_k$ maps an element $a$ of $G$ (viewed multiplicatively via $\text{Multiplicative}\,G$) to the element $\text{single}(a, 1)$ in $k[G]$, where $\text{single}(a, 1)$ is the function that is $1$ at $a$ and $0$ elsewhere.
AddMonoidAlgebra.liftMagma definition
[Module k A] [IsScalarTower k A A] [SMulCommClass k A A] : (Multiplicative G →ₙ* A) ≃ (k[G] →ₙₐ[k] A)
Full source 
/-- The functor `G ↦ k[G]`, from the category of magmas to the category of
non-unital, non-associative algebras over `k` is adjoint to the forgetful functor in the other
direction. -/
@[simps apply_apply symm_apply]
def liftMagma [Module k A] [IsScalarTower k A A] [SMulCommClass k A A] :
    (Multiplicative G →ₙ* A) ≃ (k[G] →ₙₐ[k] A) :=
  { (MonoidAlgebra.liftMagma k : (Multiplicative G →ₙ* A) ≃ (_ →ₙₐ[k] A)) with
    toFun := fun f =>
      { (MonoidAlgebra.liftMagma k f :) with
        toFun := fun a => sum a fun m t => t • f (Multiplicative.ofAdd m) }
    invFun := fun F => F.toMulHom.comp (ofMagma k G) }
Adjunction between additive magma homomorphisms and additive magma algebra homomorphisms
Informal description
Given a semiring $k$, an additive magma $G$, and a $k$-module $A$ where the scalar multiplication operations of $k$ and $A$ on $A$ form a tower and commute with each other, there is a natural bijection between: 1. Non-unital multiplicative homomorphisms from the multiplicative version of $G$ to $A$ (i.e., maps preserving multiplication but not necessarily the identity), and 2. Non-unital $k$-algebra homomorphisms from the additive magma algebra $k[G]$ to $A$. The bijection is constructed as follows: - **Forward direction**: Given a non-unital multiplicative homomorphism $f : \text{Multiplicative}\,G \to A$, the corresponding algebra homomorphism $\phi : k[G] \to A$ is defined by $\phi(\sum_{g \in G} c_g g) = \sum_{g \in G} c_g \cdot f(\text{Multiplicative.ofAdd}\,g)$, where $c_g \in k$ are coefficients with finite support. - **Backward direction**: Given a non-unital $k$-algebra homomorphism $F : k[G] \to A$, the corresponding multiplicative homomorphism is obtained by composing $F$ with the canonical embedding of $\text{Multiplicative}\,G$ in $k[G]$. This establishes an adjunction between the functor $G \mapsto k[G]$ (from additive magmas to non-unital $k$-algebras) and the forgetful functor in the opposite direction.
AddMonoidAlgebra.algebra instance
[CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : Algebra R k[G]
Full source 
/-- The instance `Algebra R k[G]` whenever we have `Algebra R k`.

In particular this provides the instance `Algebra k k[G]`.
-/
instance algebra [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
    Algebra R k[G] where
  algebraMap := singleZeroRingHom.comp (algebraMap R k)
  smul_def' := fun r a => by
    ext
    rw [Finsupp.coe_smul]
    simp [single_zero_mul_apply, Algebra.smul_def, Pi.smul_apply]
  commutes' := fun r f => by
    refine Finsupp.ext fun _ => ?_
    simp [single_zero_mul_apply, mul_single_zero_apply, Algebra.commutes]
Algebra Structure on Additive Monoid Algebras
Informal description
For any commutative semiring $R$, semiring $k$ with an $R$-algebra structure, and additive monoid $G$, the additive monoid algebra $k[G]$ inherits an $R$-algebra structure. This means $k[G]$ is equipped with: 1. A ring homomorphism $\text{algebraMap} \colon R \to k[G]$ given by $r \mapsto \text{single}(0, \text{algebraMap}(r))$, where $\text{single}(0, \cdot)$ embeds $k$ into $k[G]$ via the zero element of $G$ 2. A scalar multiplication operation $R \times k[G] \to k[G]$ compatible with the algebra structure In particular, when $R = k$, this provides the canonical algebra structure $k \to k[G]$.
AddMonoidAlgebra.singleZeroAlgHom definition
[CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : k →ₐ[R] k[G]
Full source 
/-- `Finsupp.single 0` as an `AlgHom` -/
@[simps! apply]
def singleZeroAlgHom [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : k →ₐ[R] k[G] :=
  { singleZeroRingHom with
    commutes' := fun r => by
      ext
      simp
      rfl }
Algebra homomorphism embedding $k$ into $k[G]$ via zero support
Informal description
The algebra 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) 4. Commutes with the $R$-algebra structure: for any $r \in R$, $\text{single}(0, \text{algebraMap}(r)) = \text{algebraMap}(r) \cdot \text{single}(0, 1)$
AddMonoidAlgebra.coe_algebraMap theorem
[CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : (algebraMap R k[G] : R → k[G]) = single 0 ∘ algebraMap R k
Full source 
@[simp]
theorem coe_algebraMap [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
    (algebraMap R k[G] : R → k[G]) = singlesingle 0 ∘ algebraMap R k :=
  rfl
Algebra Map Decomposition for Additive Monoid Algebras
Informal description
Let $R$ be a commutative semiring, $k$ a semiring with an $R$-algebra structure, and $G$ an additive monoid. The algebra map from $R$ to the additive monoid algebra $k[G]$ is given by composing the algebra map from $R$ to $k$ with the function $\text{single}(0, \cdot)$, which embeds $k$ into $k[G]$ via the zero element of $G$. In other words, for any $r \in R$, we have: \[ \text{algebraMap}_{R \to k[G]}(r) = \text{single}(0, \text{algebraMap}_{R \to k}(r)). \]
AddMonoidAlgebra.isLocalHom_singleZeroAlgHom instance
[CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] : IsLocalHom (singleZeroAlgHom : k →ₐ[R] k[G])
Full source 
instance isLocalHom_singleZeroAlgHom [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] :
    IsLocalHom (singleZeroAlgHom : k →ₐ[R] k[G]) where
  map_nonunit := isLocalHom_singleZeroRingHom.map_nonunit
Localness of the Zero-Support Algebra Homomorphism in Additive Monoid Algebras
Informal description
For any commutative semiring $R$, semiring $k$ with an $R$-algebra structure, and additive monoid $G$, the algebra homomorphism $\text{singleZeroAlgHom} \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$.
AddMonoidAlgebra.isLocalHom_algebraMap instance
[CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G] [IsLocalHom (algebraMap R k)] : IsLocalHom (algebraMap R k[G])
Full source 
instance isLocalHom_algebraMap [CommSemiring R] [Semiring k] [Algebra R k] [AddMonoid G]
    [IsLocalHom (algebraMap R k)] :
    IsLocalHom (algebraMap R k[G]) where
  map_nonunit _ hx := .of_map _ _ <| isLocalHom_singleZeroAlgHom (R := R).map_nonunit _ hx
Localness of the Induced Algebra Map in Additive Monoid Algebras
Informal description
For any commutative semiring $R$, semiring $k$ with an $R$-algebra structure, and additive monoid $G$, if the algebra map $\text{algebraMap} \colon R \to k$ is a local homomorphism, then the induced algebra map $\text{algebraMap} \colon R \to k[G]$ is also a local homomorphism. This means that for any $r \in R$, if $\text{algebraMap}(r)$ is a unit in $k[G]$, then $r$ is a unit in $R$.
AddMonoidAlgebra.liftNCAlgHom definition
(f : A →ₐ[k] B) (g : Multiplicative G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) : A[G] →ₐ[k] B
Full source 
/-- `liftNCRingHom` as an `AlgHom`, for when `f` is an `AlgHom` -/
def liftNCAlgHom (f : A →ₐ[k] B) (g : MultiplicativeMultiplicative G →* B) (h_comm : ∀ x y, Commute (f x) (g y)) :
    A[G]A[G] →ₐ[k] B :=
  { liftNCRingHom (f : A →+* B) g h_comm with
    commutes' := by simp [liftNCRingHom] }
Algebra homomorphism lift for additive monoid algebra with commuting images
Informal description
Given an algebra homomorphism \( f \colon A \to B \) over a commutative semiring \( k \), a monoid homomorphism \( g \colon \text{Multiplicative}\,G \to B \), and the condition that \( f(x) \) and \( g(y) \) commute for all \( x \in A \) and \( y \in G \), the function \( \text{liftNCAlgHom}\,f\,g \) is the algebra homomorphism from the additive monoid algebra \( A[G] \) to \( B \) defined by: \[ \text{liftNCAlgHom}\,f\,g\,(\text{single}\,a\,b) = f(b) \cdot g(\text{ofAdd}\,a) \] for all \( a \in G \) and \( b \in A \). This extends the non-commutative lift \( \text{liftNCRingHom} \) to an algebra homomorphism when the images of \( f \) and \( g \) commute pairwise.
AddMonoidAlgebra.algHom_ext theorem
⦃φ₁ φ₂ : k[G] →ₐ[k] A⦄ (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂
Full source 
/-- A `k`-algebra homomorphism from `k[G]` is uniquely defined by its
values on the functions `single a 1`. -/
theorem algHom_ext ⦃φ₁ φ₂ : k[G]k[G] →ₐ[k] A⦄
    (h : ∀ x, φ₁ (single x 1) = φ₂ (single x 1)) : φ₁ = φ₂ :=
  @MonoidAlgebra.algHom_ext k (Multiplicative G) _ _ _ _ _ _ _ h
Uniqueness of Algebra Homomorphisms on Additive Monoid Algebras via Single Generators
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any two $k$-algebra homomorphisms $\varphi_1, \varphi_2 \colon k[G] \to A$, if $\varphi_1(\text{single}(x, 1)) = \varphi_2(\text{single}(x, 1))$ for all $x \in G$, then $\varphi_1 = \varphi_2$. Here, $k[G]$ denotes the additive monoid algebra of $G$ over $k$, and $\text{single}(x, 1)$ is the element of $k[G]$ that is $1$ at $x$ and $0$ elsewhere.
AddMonoidAlgebra.algHom_ext' theorem
⦃φ₁ φ₂ : k[G] →ₐ[k] A⦄ (h : (φ₁ : k[G] →* A).comp (of k G) = (φ₂ : k[G] →* A).comp (of k G)) : φ₁ = φ₂
Full source 
/-- See note [partially-applied ext lemmas]. -/
@[ext high]
theorem algHom_ext' ⦃φ₁ φ₂ : k[G]k[G] →ₐ[k] A⦄
    (h : (φ₁ : k[G]k[G] →* A).comp (of k G) = (φ₂ : k[G]k[G] →* A).comp (of k G)) :
    φ₁ = φ₂ :=
  algHom_ext <| DFunLike.congr_fun h
Uniqueness of Algebra Homomorphisms on Additive Monoid Algebras via Composition with Embedding
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any two $k$-algebra homomorphisms $\varphi_1, \varphi_2 \colon k[G] \to A$, if the compositions of $\varphi_1$ and $\varphi_2$ with the embedding $\text{of}\,k\,G \colon \text{Multiplicative}\,G \to k[G]$ are equal, then $\varphi_1 = \varphi_2$. Here, $k[G]$ denotes the additive monoid algebra of $G$ over $k$, and $\text{of}\,k\,G$ is the canonical embedding of $G$ into $k[G]$ as a multiplicative monoid.
AddMonoidAlgebra.lift definition
: (Multiplicative G →* A) ≃ (k[G] →ₐ[k] A)
Full source 
/-- Any monoid homomorphism `G →* A` can be lifted to an algebra homomorphism
`k[G] →ₐ[k] A`. -/
def lift : (Multiplicative G →* A) ≃ (k[G] →ₐ[k] A) :=
  { @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ with
    invFun := fun f => (f : k[G]k[G] →* A).comp (of k G)
    toFun := fun F =>
      { @MonoidAlgebra.lift k (Multiplicative G) _ _ A _ _ F with
        toFun := liftNCAlgHom (Algebra.ofId k A) F fun _ _ => Algebra.commutes _ _ } }
Lifting monoid homomorphisms to algebra homomorphisms on additive monoid algebras
Informal description
Given a commutative semiring $k$, an additive monoid $G$, and a $k$-algebra $A$, there is a natural equivalence between monoid homomorphisms from the multiplicative version of $G$ to $A$ and $k$-algebra homomorphisms from the additive monoid algebra $k[G]$ to $A$. More precisely: - The forward direction lifts a monoid homomorphism $F \colon \text{Multiplicative}\,G \to^* A$ to an algebra homomorphism by linearly extending the map $\text{single}(a, b) \mapsto b \cdot F(\text{ofAdd}\,a)$. - The backward direction restricts an algebra homomorphism $\varphi \colon k[G] \toₐ[k] A$ to $\text{Multiplicative}\,G$ via composition with the embedding $\text{of}\,k\,G \colon \text{Multiplicative}\,G \to^* k[G]$. This equivalence satisfies that for any monoid homomorphism $F$ and $f \in k[G]$, the lifted homomorphism evaluates as: \[ \text{lift}\,k\,G\,A\,F\,f = \sum_{(a,b) \in \text{supp}(f)} b \cdot F(\text{ofAdd}\,a) \] where $\text{supp}(f)$ is the support of $f$ (the finite set where $f$ is nonzero).
AddMonoidAlgebra.lift_apply' theorem
(F : Multiplicative G →* A) (f : MonoidAlgebra k G) : lift k G A F f = f.sum fun a b => algebraMap k A b * F (Multiplicative.ofAdd a)
Full source 
theorem lift_apply' (F : MultiplicativeMultiplicative G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => algebraMap k A b * F (Multiplicative.ofAdd a) :=
  rfl
Evaluation of Lifted Algebra Homomorphism on Additive Monoid Algebra Elements
Informal description
Given a commutative semiring $k$, an additive monoid $G$, a $k$-algebra $A$, and a monoid homomorphism $F \colon \text{Multiplicative}\,G \to A$, the lifted algebra homomorphism $\text{lift}\,k\,G\,A\,F \colon k[G] \to A$ evaluated at an element $f \in k[G]$ satisfies: \[ \text{lift}\,k\,G\,A\,F\,f = \sum_{(a, b) \in \text{supp}(f)} \text{algebraMap}\,k\,A\,b \cdot F(\text{Multiplicative.ofAdd}\,a), \] where $\text{supp}(f)$ is the support of $f$ (the finite set where $f$ is nonzero), $\text{algebraMap}\,k\,A$ is the canonical ring homomorphism from $k$ to $A$, and $\text{Multiplicative.ofAdd}$ is the embedding of $G$ into its multiplicative version.
AddMonoidAlgebra.lift_apply theorem
(F : Multiplicative G →* A) (f : MonoidAlgebra k G) : lift k G A F f = f.sum fun a b => b • F (Multiplicative.ofAdd a)
Full source 
theorem lift_apply (F : MultiplicativeMultiplicative G →* A) (f : MonoidAlgebra k G) :
    lift k G A F f = f.sum fun a b => b • F (Multiplicative.ofAdd a) := by
  simp only [lift_apply', Algebra.smul_def]
Evaluation of Lifted Algebra Homomorphism on Additive Monoid Algebra Elements
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. Given a monoid homomorphism $F \colon \text{Multiplicative}\,G \to A$ and an element $f \in k[G]$, the lift of $F$ to an algebra homomorphism $\text{lift}\,k\,G\,A\,F \colon k[G] \to A$ satisfies: \[ \text{lift}\,k\,G\,A\,F\,f = \sum_{(a,b) \in \text{supp}(f)} b \cdot F(\text{ofAdd}\,a) \] where $\text{supp}(f)$ is the support of $f$ (the finite set where $f$ is nonzero), and $\text{ofAdd}$ is the canonical embedding of $G$ into $\text{Multiplicative}\,G$.
AddMonoidAlgebra.lift_def theorem
(F : Multiplicative G →* A) : ⇑(lift k G A F) = liftNC ((algebraMap k A : k →+* A) : k →+ A) F
Full source 
theorem lift_def (F : MultiplicativeMultiplicative G →* A) :
    ⇑(lift k G A F) = liftNC ((algebraMap k A : k →+* A) : k →+ A) F :=
  rfl
Definition of the Lifted Algebra Homomorphism via Non-Commutative Lift
Informal description
For any commutative semiring $k$, additive monoid $G$, $k$-algebra $A$, and monoid homomorphism $F \colon \text{Multiplicative}\,G \to^* A$, the lifted algebra homomorphism $\text{lift}\,k\,G\,A\,F \colon k[G] \to A$ is equal to the non-commutative lift $\text{liftNC}$ applied to the additive homomorphism $\text{algebraMap}\,k\,A \colon k \to A$ and $F$. More precisely, for any $f \in k[G]$, we have: \[ \text{lift}\,k\,G\,A\,F\,f = \sum_{(a,b) \in \text{supp}(f)} \text{algebraMap}\,k\,A(b) \cdot F(\text{ofAdd}\,a) \] where $\text{supp}(f)$ is the support of $f$ (the finite set where $f$ is nonzero).
AddMonoidAlgebra.lift_symm_apply theorem
(F : k[G] →ₐ[k] A) (x : Multiplicative G) : (lift k G A).symm F x = F (single x.toAdd 1)
Full source 
@[simp]
theorem lift_symm_apply (F : k[G]k[G] →ₐ[k] A) (x : Multiplicative G) :
    (lift k G A).symm F x = F (single x.toAdd 1) :=
  rfl
Inverse of Lifting Equivalence for Additive Monoid Algebras
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any $k$-algebra homomorphism $F \colon k[G] \to A$ and any element $x$ in the multiplicative version of $G$, the inverse of the lifting equivalence $\text{lift}$ satisfies: \[ \text{lift}^{-1}(F)(x) = F(\text{single}(x, 1)) \] where $\text{single}(x, 1)$ is the element of $k[G]$ that is $1$ at $x$ and $0$ elsewhere.
AddMonoidAlgebra.lift_of theorem
(F : Multiplicative G →* A) (x : Multiplicative G) : lift k G A F (of k G x) = F x
Full source 
theorem lift_of (F : MultiplicativeMultiplicative G →* A) (x : Multiplicative G) :
    lift k G A F (of k G x) = F x := MonoidAlgebra.lift_of F x
Lifted homomorphism preserves canonical embedding: $\text{lift}(F)(\text{of}(x)) = F(x)$
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any monoid homomorphism $F \colon \text{Multiplicative}\,G \to A$ and any element $x \in \text{Multiplicative}\,G$, the lifted algebra homomorphism $\text{lift}_{k,G,A}(F)$ satisfies \[ \text{lift}_{k,G,A}(F)(\text{of}_{k,G}(x)) = F(x), \] where $\text{of}_{k,G} \colon \text{Multiplicative}\,G \to k[G]$ is the canonical embedding of $G$ into its monoid algebra.
AddMonoidAlgebra.lift_single theorem
(F : Multiplicative G →* A) (a b) : lift k G A F (single a b) = b • F (Multiplicative.ofAdd a)
Full source 
@[simp]
theorem lift_single (F : MultiplicativeMultiplicative G →* A) (a b) :
    lift k G A F (single a b) = b • F (Multiplicative.ofAdd a) :=
  MonoidAlgebra.lift_single F (.ofAdd a) b
Evaluation of Lifted Homomorphism on Single Generator: $\text{lift}(F)(\text{single}(a, b)) = b \cdot F(a)$
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any monoid homomorphism $F \colon \text{Multiplicative}\,G \to^* A$ and elements $a \in G$, $b \in k$, the lifted algebra homomorphism $\text{lift}_{k,G,A}(F)$ applied to the monoid algebra element $\text{single}(a, b)$ satisfies: \[ \text{lift}_{k,G,A}(F)(\text{single}(a, b)) = b \cdot F(\text{ofAdd}\,a), \] where $\text{ofAdd}\,a$ is the embedding of $a$ into $\text{Multiplicative}\,G$.
AddMonoidAlgebra.lift_of' theorem
(F : Multiplicative G →* A) (x : G) : lift k G A F (of' k G x) = F (Multiplicative.ofAdd x)
Full source 
lemma lift_of' (F : MultiplicativeMultiplicative G →* A) (x : G) :
    lift k G A F (of' k G x) = F (Multiplicative.ofAdd x) :=
  lift_of F x
Lifted homomorphism preserves canonical embedding: $\text{lift}(F)(\text{of}'(x)) = F(\text{ofAdd}\,x)$
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any monoid homomorphism $F \colon \text{Multiplicative}\,G \to A$ and any element $x \in G$, the lifted algebra homomorphism $\text{lift}_{k,G,A}(F)$ satisfies \[ \text{lift}_{k,G,A}(F)(\text{of}'_{k,G}(x)) = F(\text{Multiplicative.ofAdd}\,x), \] where $\text{of}'_{k,G} \colon G \to k[G]$ is the canonical embedding of $G$ into its monoid algebra, and $\text{Multiplicative.ofAdd}$ is the embedding of $G$ into $\text{Multiplicative}\,G$.
AddMonoidAlgebra.lift_unique' theorem
(F : k[G] →ₐ[k] A) : F = lift k G A ((F : k[G] →* A).comp (of k G))
Full source 
theorem lift_unique' (F : k[G]k[G] →ₐ[k] A) :
    F = lift k G A ((F : k[G]k[G] →* A).comp (of k G)) :=
  ((lift k G A).apply_symm_apply F).symm
Uniqueness of Algebra Homomorphism Factorization via Lift in Additive Monoid Algebras
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any $k$-algebra homomorphism $F \colon k[G] \to A$, $F$ is equal to the lift of the composition of $F$ (viewed as a monoid homomorphism) with the canonical embedding $\text{of} \colon \text{Multiplicative}\,G \to^* k[G]$. More precisely, $F$ factors uniquely through the lift construction applied to $F \circ \text{of}$.
AddMonoidAlgebra.lift_unique theorem
(F : k[G] →ₐ[k] A) (f : MonoidAlgebra k G) : F f = f.sum fun a b => b • F (single a 1)
Full source 
/-- Decomposition of a `k`-algebra homomorphism from `MonoidAlgebra k G` by
its values on `F (single a 1)`. -/
theorem lift_unique (F : k[G]k[G] →ₐ[k] A) (f : MonoidAlgebra k G) :
    F f = f.sum fun a b => b • F (single a 1) := by
  conv_lhs =>
    rw [lift_unique' F]
    simp [lift_apply]
Factorization of Algebra Homomorphisms on Additive Monoid Algebras via Single Generators
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any $k$-algebra homomorphism $F \colon k[G] \to A$ and any element $f \in k[G]$, the homomorphism $F$ evaluated at $f$ can be expressed as: \[ F(f) = \sum_{(a,b) \in \text{supp}(f)} b \cdot F(\text{single}(a, 1)) \] where $\text{supp}(f)$ is the support of $f$ (the finite set where $f$ is nonzero), and $\text{single}(a, 1)$ denotes the element of $k[G]$ that is $1$ at $a$ and $0$ elsewhere.
AddMonoidAlgebra.algHom_ext_iff theorem
{φ₁ φ₂ : k[G] →ₐ[k] A} : (∀ x, φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) ↔ φ₁ = φ₂
Full source 
theorem algHom_ext_iff {φ₁ φ₂ : k[G]k[G] →ₐ[k] A} :
    (∀ x, φ₁ (Finsupp.single x 1) = φ₂ (Finsupp.single x 1)) ↔ φ₁ = φ₂ :=
  ⟨fun h => algHom_ext h, by rintro rfl _; rfl⟩
Equivalence of Algebra Homomorphism Equality and Agreement on Single Generators in Additive Monoid Algebras
Informal description
Let $k$ be a commutative semiring, $G$ an additive monoid, and $A$ a $k$-algebra. For any two $k$-algebra homomorphisms $\varphi_1, \varphi_2 \colon k[G] \to A$, the following are equivalent: 1. $\varphi_1$ and $\varphi_2$ agree on all elements of the form $\text{single}(x, 1)$ for $x \in G$, where $\text{single}(x, 1)$ denotes the function that is $1$ at $x$ and $0$ elsewhere. 2. $\varphi_1 = \varphi_2$.
AddMonoidAlgebra.mapDomain_algebraMap theorem
(A : Type*) {H F : Type*} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) (r : k) : mapDomain f (algebraMap k A[G] r) = algebraMap k A[H] r
Full source 
theorem mapDomain_algebraMap (A : Type*) {H F : Type*} [CommSemiring k] [Semiring A] [Algebra k A]
    [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H]
    (f : F) (r : k) :
    mapDomain f (algebraMap k A[G] r) = algebraMap k A[H] r := by
  simp only [Function.comp_apply, mapDomain_single, AddMonoidAlgebra.coe_algebraMap, map_zero]
Commutativity of Algebra Map with Domain Mapping in Additive Monoid Algebras
Informal description
Let $k$ be a commutative semiring, $A$ a semiring with a $k$-algebra structure, and $G$, $H$ additive monoids. For any additive monoid homomorphism $f \colon G \to H$ and any element $r \in k$, the map domain operation applied to the algebra map of $r$ in $A[G]$ equals the algebra map of $r$ in $A[H]$. In other words, the following diagram commutes: $$ \begin{CD} k @>{\text{algebraMap}}>> A[G] \\ @V{\text{algebraMap}}VV @VV{\text{mapDomain}\, f}V \\ A[H] @= A[H] \end{CD} $$
AddMonoidAlgebra.mapDomainNonUnitalAlgHom definition
(k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] {G H F : Type*} [Add G] [Add H] [FunLike F G H] [AddHomClass F G H] (f : F) : A[G] →ₙₐ[k] A[H]
Full source 
/-- If `f : G → H` is a homomorphism between two additive magmas, then `Finsupp.mapDomain f` is a
non-unital algebra homomorphism between their additive magma algebras. -/
@[simps apply]
def mapDomainNonUnitalAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A]
    {G H F : Type*} [Add G] [Add H] [FunLike F G H] [AddHomClass F G H] (f : F) :
    A[G]A[G] →ₙₐ[k] A[H] :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebraMonoidAlgebra A G →+ MonoidAlgebra A H) with
    map_mul' := fun x y => mapDomain_mul f x y
    map_smul' := fun r x => mapDomain_smul r x }
Non-unital algebra homomorphism induced by domain mapping of additive magma algebras
Informal description
Given a commutative semiring $k$, a semiring $A$ with a $k$-algebra structure, and additive magmas $G$ and $H$, for any additive homomorphism $f \colon G \to H$, the function `mapDomainNonUnitalAlgHom` constructs a non-unital algebra homomorphism between the additive magma algebras $A[G]$ and $A[H]$. This homomorphism is defined by extending $f$ linearly to formal $A$-linear combinations of elements of $G$, preserving the convolution product structure. Specifically, it maps a finitely supported function $v \in A[G]$ to its image under domain mapping by $f$, i.e., $\text{mapDomain}\, f\, v \in A[H]$.
AddMonoidAlgebra.mapDomainAlgHom definition
(k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] {H F : Type*} [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) : A[G] →ₐ[k] A[H]
Full source 
/-- If `f : G → H` is an additive homomorphism between two additive monoids, then
`Finsupp.mapDomain f` is an algebra homomorphism between their add monoid algebras. -/
@[simps!]
def mapDomainAlgHom (k A : Type*) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G]
    {H F : Type*} [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :
    A[G]A[G] →ₐ[k] A[H] :=
  { mapDomainRingHom A f with commutes' := mapDomain_algebraMap A f }
Algebra homomorphism induced by domain mapping of additive monoid algebras
Informal description
Given a commutative semiring $k$, a semiring $A$ with a $k$-algebra structure, and additive monoids $G$ and $H$, for any additive monoid homomorphism $f \colon G \to H$, the function `mapDomainAlgHom` constructs an algebra homomorphism between the additive monoid algebras $A[G]$ and $A[H]$. This homomorphism is defined by extending $f$ linearly to formal $A$-linear combinations of elements of $G$, preserving both the additive and multiplicative structures. Specifically, it maps a finitely supported function $v \in A[G]$ to its image under domain mapping by $f$, i.e., $\text{mapDomain}\, f\, v \in A[H]$, and it commutes with the algebra maps from $k$.
AddMonoidAlgebra.mapDomainAlgHom_id theorem
(k A) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] : mapDomainAlgHom k A (AddMonoidHom.id G) = AlgHom.id k (AddMonoidAlgebra A G)
Full source 
@[simp]
lemma mapDomainAlgHom_id (k A) [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G] :
    mapDomainAlgHom k A (AddMonoidHom.id G) = AlgHom.id k (AddMonoidAlgebra A G) := by
  ext; simp [AddMonoidHom.id, ← Function.id_def]
Identity Mapping Induces Identity Algebra Homomorphism on Additive Monoid Algebras
Informal description
For any commutative semiring $k$, semiring $A$ with a $k$-algebra structure, and additive monoid $G$, the algebra homomorphism induced by the identity additive monoid homomorphism on $G$ is equal to the identity algebra homomorphism on the additive monoid algebra $A[G]$. That is, the following diagram commutes: \[ \text{mapDomainAlgHom}\, k\, A\, (\text{id}_G) = \text{id}_{A[G]} \]
AddMonoidAlgebra.mapDomainAlgHom_comp theorem
(k A) {G₁ G₂ G₃} [CommSemiring k] [Semiring A] [Algebra k A] [AddMonoid G₁] [AddMonoid G₂] [AddMonoid G₃] (f : G₁ →+ G₂) (g : G₂ →+ G₃) : mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f)
Full source 
@[simp]
lemma mapDomainAlgHom_comp (k A) {G₁ G₂ G₃} [CommSemiring k] [Semiring A] [Algebra k A]
    [AddMonoid G₁] [AddMonoid G₂] [AddMonoid G₃] (f : G₁ →+ G₂) (g : G₂ →+ G₃) :
    mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f) := by
  ext; simp [mapDomain_comp]
Composition of Algebra Homomorphisms Induced by Additive Monoid Homomorphisms
Informal description
Let $k$ be a commutative semiring, $A$ a semiring with a $k$-algebra structure, and $G_1$, $G_2$, $G_3$ additive monoids. For any additive monoid homomorphisms $f \colon G_1 \to G_2$ and $g \colon G_2 \to G_3$, the algebra homomorphism induced by the composition $g \circ f$ on the additive monoid algebras is equal to the composition of the algebra homomorphisms induced by $g$ and $f$ respectively. That is, \[ \text{mapDomainAlgHom}\, k\, A\, (g \circ f) = (\text{mapDomainAlgHom}\, k\, A\, g) \circ (\text{mapDomainAlgHom}\, k\, A\, f). \]
AddMonoidAlgebra.domCongr definition
(e : G ≃+ H) : A[G] ≃ₐ[k] A[H]
Full source 
/-- If `e : G ≃* H` is a multiplicative equivalence between two monoids, then
`AddMonoidAlgebra.domCongr e` is an algebra equivalence between their monoid algebras. -/
def domCongr (e : G ≃+ H) : A[G]A[G] ≃ₐ[k] A[H] :=
  AlgEquiv.ofLinearEquiv
    (Finsupp.domLCongr e : (G →₀ A) ≃ₗ[k] (H →₀ A))
    ((equivMapDomain_eq_mapDomain _ _).trans <| mapDomain_one e)
    (fun f g => (equivMapDomain_eq_mapDomain _ _).trans <| (mapDomain_mul e f g).trans <|
        congr_arg₂ _ (equivMapDomain_eq_mapDomain _ _).symm (equivMapDomain_eq_mapDomain _ _).symm)
Algebra equivalence of monoid algebras induced by an additive monoid equivalence
Informal description
Given a commutative semiring $k$, a semiring $A$ with a $k$-algebra structure, and an additive equivalence $e : G \simeq H$ between two additive monoids $G$ and $H$, the function $\text{AddMonoidAlgebra.domCongr}\, e$ is an algebra equivalence between the monoid algebras $A[G]$ and $A[H]$. This equivalence maps a finitely supported function $f : G \to A$ to the function $H \to A$ defined by $h \mapsto f(e^{-1}(h))$, and preserves both the additive and multiplicative structures of the monoid algebras. Specifically: 1. It maps the multiplicative identity of $A[G]$ to that of $A[H]$. 2. It preserves the convolution product: for any $f, g \in A[G]$, the image of $f * g$ under the equivalence is the convolution product of the images of $f$ and $g$.
AddMonoidAlgebra.domCongr_toAlgHom theorem
(e : G ≃+ H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e
Full source 
theorem domCongr_toAlgHom (e : G ≃+ H) : (domCongr k A e).toAlgHom = mapDomainAlgHom k A e :=
  AlgHom.ext fun _ => equivMapDomain_eq_mapDomain _ _
Equality of Algebra Homomorphisms in Monoid Algebra Equivalence
Informal description
Given a commutative semiring $k$, a semiring $A$ with a $k$-algebra structure, and an additive equivalence $e : G \simeq H$ between two additive monoids $G$ and $H$, the underlying algebra homomorphism of the algebra equivalence $\text{domCongr}\, e$ is equal to the algebra homomorphism $\text{mapDomainAlgHom}\, e$ induced by $e$. In other words, the following diagram commutes: $$ \begin{CD} A[G] @>{\text{domCongr}\, e}>> A[H] \\ @V{\text{mapDomainAlgHom}\, e}VV @| \\ A[H] @= A[H] \end{CD} $$
AddMonoidAlgebra.domCongr_apply theorem
(e : G ≃+ H) (f : MonoidAlgebra A G) (h : H) : domCongr k A e f h = f (e.symm h)
Full source 
@[simp] theorem domCongr_apply (e : G ≃+ H) (f : MonoidAlgebra A G) (h : H) :
    domCongr k A e f h = f (e.symm h) :=
  rfl
Evaluation of Monoid Algebra Equivalence Induced by Additive Monoid Equivalence
Informal description
Let $k$ be a commutative semiring, $A$ a semiring with a $k$-algebra structure, and $e : G \simeq H$ an additive equivalence between two additive monoids $G$ and $H$. For any element $f$ in the monoid algebra $A[G]$ and any $h \in H$, the evaluation of the algebra equivalence $\text{domCongr}\, e$ applied to $f$ at $h$ is equal to $f$ evaluated at $e^{-1}(h)$, i.e., $$(\text{domCongr}\, e\, f)(h) = f(e^{-1}(h)).$$
AddMonoidAlgebra.domCongr_support theorem
(e : G ≃+ H) (f : MonoidAlgebra A G) : (domCongr k A e f).support = f.support.map e
Full source 
@[simp] theorem domCongr_support (e : G ≃+ H) (f : MonoidAlgebra A G) :
    (domCongr k A e f).support = f.support.map e :=
  rfl
Support Preservation under Monoid Algebra Equivalence
Informal description
Given a commutative semiring $k$, a semiring $A$ with a $k$-algebra structure, and an additive equivalence $e : G \simeq H$ between two additive monoids $G$ and $H$, the support of the image of any element $f \in A[G]$ under the algebra equivalence $\text{domCongr}\, e$ is equal to the image of the support of $f$ under the map induced by $e$. In other words, for any $f \in A[G]$, we have: $$\text{supp}(\text{domCongr}\, e\, f) = e(\text{supp}(f))$$ where $\text{supp}(f)$ denotes the support of $f$ (the finite set of elements where $f$ is non-zero).
AddMonoidAlgebra.domCongr_single theorem
(e : G ≃+ H) (g : G) (a : A) : domCongr k A e (single g a) = single (e g) a
Full source 
@[simp] theorem domCongr_single (e : G ≃+ H) (g : G) (a : A) :
    domCongr k A e (single g a) = single (e g) a :=
  Finsupp.equivMapDomain_single _ _ _
Preservation of Single Generators under Monoid Algebra Equivalence: $\text{domCongr}\, e \, (\text{single}(g, a)) = \text{single}(e(g), a)$
Informal description
Let $G$ and $H$ be additive monoids, $A$ a semiring, and $k$ a commutative semiring such that $A$ is a $k$-algebra. Given an additive equivalence $e \colon G \simeq H$, an element $g \in G$, and an element $a \in A$, the algebra equivalence $\text{domCongr}\, e$ maps the single generator $\text{single}(g, a) \in A[G]$ to $\text{single}(e(g), a) \in A[H]$. In other words, the equivalence preserves single generators via: $$\text{domCongr}\, e \, (\text{single}(g, a)) = \text{single}(e(g), a).$$
AddMonoidAlgebra.domCongr_refl theorem
: domCongr k A (AddEquiv.refl G) = AlgEquiv.refl
Full source 
@[simp] theorem domCongr_refl : domCongr k A (AddEquiv.refl G) = AlgEquiv.refl :=
  AlgEquiv.ext fun _ => Finsupp.ext fun _ => rfl
Identity Additive Monoid Equivalence Induces Identity Algebra Equivalence on Monoid Algebras
Informal description
For any commutative semiring $k$, semiring $A$ with a $k$-algebra structure, and additive monoid $G$, the algebra equivalence $\text{domCongr}$ induced by the additive monoid equivalence $\text{AddEquiv.refl}\, G$ is equal to the identity algebra equivalence $\text{AlgEquiv.refl}$ on the monoid algebra $A[G]$.
AddMonoidAlgebra.domCongr_symm theorem
(e : G ≃+ H) : (domCongr k A e).symm = domCongr k A e.symm
Full source 
@[simp] theorem domCongr_symm (e : G ≃+ H) : (domCongr k A e).symm = domCongr k A e.symm := rfl
Inverse of Monoid Algebra Equivalence Induced by Additive Monoid Equivalence
Informal description
Given a commutative semiring $k$, a semiring $A$ with a $k$-algebra structure, and an additive equivalence $e : G \simeq H$ between two additive monoids $G$ and $H$, the inverse of the algebra equivalence $\text{domCongr}\, e : A[G] \simeq A[H]$ is equal to the algebra equivalence $\text{domCongr}\, e^{-1} : A[H] \simeq A[G]$.
AddMonoidAlgebra.toMultiplicativeAlgEquiv definition
[Semiring k] [Algebra R k] [AddMonoid G] : AddMonoidAlgebra k G ≃ₐ[R] MonoidAlgebra k (Multiplicative G)
Full source 
/-- The algebra equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative`. -/
def AddMonoidAlgebra.toMultiplicativeAlgEquiv [Semiring k] [Algebra R k] [AddMonoid G] :
    AddMonoidAlgebraAddMonoidAlgebra k G ≃ₐ[R] MonoidAlgebra k (Multiplicative G) :=
  { AddMonoidAlgebra.toMultiplicative k G with
    commutes' := fun r => by simp [AddMonoidAlgebra.toMultiplicative] }
Algebra equivalence between additive and multiplicative monoid algebras
Informal description
The algebra equivalence between the additive monoid algebra $k[G]$ and the monoid algebra $k[\text{Multiplicative}\,G]$, where $\text{Multiplicative}\,G$ is the multiplicative type tag of the additive monoid $G$. This equivalence preserves the algebra structure over the commutative semiring $R$. More precisely, it is an algebra isomorphism that commutes with the algebra maps from $R$ and respects the convolution product structure on both sides.
MonoidAlgebra.toAdditiveAlgEquiv definition
[Semiring k] [Algebra R k] [Monoid G] : MonoidAlgebra k G ≃ₐ[R] AddMonoidAlgebra k (Additive G)
Full source 
/-- The algebra equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of
`Additive`. -/
def MonoidAlgebra.toAdditiveAlgEquiv [Semiring k] [Algebra R k] [Monoid G] :
    MonoidAlgebraMonoidAlgebra k G ≃ₐ[R] AddMonoidAlgebra k (Additive G) :=
  { MonoidAlgebra.toAdditive k G with commutes' := fun r => by simp [MonoidAlgebra.toAdditive] }
Algebra equivalence between monoid algebra and additive monoid algebra
Informal description
Given a semiring $k$ with an algebra structure over a commutative semiring $R$ and a monoid $G$, there is an algebra equivalence between the monoid algebra $k[G]$ and the additive monoid algebra $k[\text{Additive}(G)]$, where $\text{Additive}(G)$ is the additive monoid obtained by converting the multiplicative structure of $G$ to an additive structure. This equivalence preserves the algebra structure, meaning it commutes with the algebra maps from $R$ and respects the addition and multiplication operations in both algebras.