Mathlib.Algebra.MonoidAlgebra.MapDomain

MonoidAlgebra.mapDomain abbrev

(f : M → N) (v : MonoidAlgebra R M) : MonoidAlgebra R N

Full source

abbrev mapDomain (f : M → N) (v : MonoidAlgebra R M) : MonoidAlgebra R N := Finsupp.mapDomain f v

Induced algebra homomorphism between monoid algebras via monoid homomorphism

Informal description

Given a semiring $R$ and monoids $M$ and $N$, the function `MonoidAlgebra.mapDomain` maps a monoid homomorphism $f : M \to N$ to a $R$-algebra homomorphism from the monoid algebra $R[M]$ to $R[N]$. Specifically, for any element $v \in R[M]$, `mapDomain f v` is the element of $R[N]$ obtained by applying $f$ to the support of $v$ and preserving the coefficients.

MonoidAlgebra.mapDomain_sum theorem

 (f : M → N) (s : MonoidAlgebra S M) (v : M → S → MonoidAlgebra R M) :
  mapDomain f (s.sum v) = s.sum fun a b ↦ mapDomain f (v a b)

Full source

lemma mapDomain_sum (f : M → N) (s : MonoidAlgebra S M) (v : M → S → MonoidAlgebra R M) :
    mapDomain f (s.sum v) = s.sum fun a b ↦ mapDomain f (v a b) := Finsupp.mapDomain_sum

Summation Commutes with Monoid Algebra Homomorphism

Informal description

Let $R$, $S$ be semirings and $M$, $N$ be monoids. Given a monoid homomorphism $f \colon M \to N$, a finitely supported function $s \in S[M]$, and a family of finitely supported functions $v \colon M \to S \to R[M]$, the image under the induced algebra homomorphism $\operatorname{mapDomain} f$ of the sum $\sum_{a \in M} s(a) \cdot v(a)$ equals the sum $\sum_{a \in M} s(a) \cdot \operatorname{mapDomain} f (v(a))$. In other words, the following equality holds: \[ \operatorname{mapDomain}_f \left( \sum_{a \in M} s(a) \cdot v(a) \right) = \sum_{a \in M} s(a) \cdot \operatorname{mapDomain}_f (v(a)). \]

MonoidAlgebra.mapDomain_single theorem

: mapDomain f (single a r) = single (f a) r

Full source

lemma mapDomain_single : mapDomain f (single a r) = single (f a) r := Finsupp.mapDomain_single

Image of a Single Generator under Monoid Algebra Homomorphism

Informal description

For any monoid homomorphism $f \colon M \to N$ and any elements $a \in M$ and $r \in R$, the image of the monoid algebra element $\text{single}(a, r) \in R[M]$ under the induced algebra homomorphism $\text{mapDomain}\, f$ is equal to $\text{single}(f(a), r) \in R[N]$. That is, \[ \text{mapDomain}\, f\, (\text{single}\, a\, r) = \text{single}\, (f\, a)\, r. \]

MonoidAlgebra.mapDomain_injective theorem

(hf : Injective f) : Injective (mapDomain (R := R) f)

Full source

lemma mapDomain_injective (hf : Injective f) : Injective (mapDomain (R := R) f) :=
  Finsupp.mapDomain_injective hf

Injectivity of Induced Algebra Homomorphism via Injective Monoid Homomorphism

Informal description

Let $R$ be a semiring and $M$, $N$ be monoids. Given an injective monoid homomorphism $f \colon M \to N$, the induced $R$-algebra homomorphism $\text{mapDomain}\, f \colon R[M] \to R[N]$ is also injective.

MonoidAlgebra.mapDomain_one theorem

 {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [One α] [One α₂] {F : Type*} [FunLike F α α₂] [OneHomClass F α α₂]
  (f : F) : (mapDomain f (1 : MonoidAlgebra β α) : MonoidAlgebra β α₂) = (1 : MonoidAlgebra β α₂)

Full source

/-- Like `Finsupp.mapDomain_zero`, but for the `1` we define in this file -/
@[simp]
theorem mapDomain_one {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [One α] [One α₂]
    {F : Type*} [FunLike F α α₂] [OneHomClass F α α₂] (f : F) :
    (mapDomain f (1 : MonoidAlgebra β α) : MonoidAlgebra β α₂) = (1 : MonoidAlgebra β α₂) := by
  simp_rw [one_def, mapDomain_single, map_one]

Preservation of Multiplicative Identity under Monoid Algebra Homomorphism

Informal description

Let $R$ be a semiring, and let $M$ and $N$ be monoids each equipped with a multiplicative identity element. Given a homomorphism $f \colon M \to N$ that preserves the identity (i.e., $f(1_M) = 1_N$), the induced algebra homomorphism $\text{mapDomain}\, f$ from the monoid algebra $R[M]$ to $R[N]$ maps the multiplicative identity of $R[M]$ to the multiplicative identity of $R[N]$. That is, \[ \text{mapDomain}\, f\, (1_{R[M]}) = 1_{R[N]}. \]

MonoidAlgebra.mapDomain_mul theorem

 {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Mul α] [Mul α₂] {F : Type*} [FunLike F α α₂] [MulHomClass F α α₂]
  (f : F) (x y : MonoidAlgebra β α) : mapDomain f (x * y) = mapDomain f x * mapDomain f y

Full source

/-- Like `Finsupp.mapDomain_add`, but for the convolutive multiplication we define in this file -/
theorem mapDomain_mul {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Mul α] [Mul α₂]
    {F : Type*} [FunLike F α α₂] [MulHomClass F α α₂] (f : F) (x y : MonoidAlgebra β α) :
    mapDomain f (x * y) = mapDomain f x * mapDomain f y := by
  simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_mul]
  rw [Finsupp.sum_mapDomain_index]
  · congr
    ext a b
    rw [Finsupp.sum_mapDomain_index]
    · simp
    · simp [mul_add]
  · simp
  · simp [add_mul]

Preservation of Convolution Product under Monoid Algebra Homomorphism

Informal description

Let $R$ be a semiring, and let $M$ and $N$ be multiplicative monoids. Given a multiplicative homomorphism $f \colon M \to N$ (i.e., $f(x \cdot y) = f(x) \cdot f(y)$ for all $x, y \in M$), the induced algebra homomorphism $\operatorname{mapDomain} f$ from the monoid algebra $R[M]$ to $R[N]$ preserves the convolution product. That is, for any $x, y \in R[M]$, we have: \[ \operatorname{mapDomain} f (x * y) = (\operatorname{mapDomain} f x) * (\operatorname{mapDomain} f y). \]

MonoidAlgebra.mapDomainRingHom definition

 (k : Type*) {H F : Type*} [Semiring k] [Monoid G] [Monoid H] [FunLike F G H] [MonoidHomClass F G H] (f : F) :
  MonoidAlgebra k G →+* MonoidAlgebra k H

Full source

/-- If `f : G → H` is a multiplicative homomorphism between two monoids, then
`Finsupp.mapDomain f` is a ring homomorphism between their monoid algebras. -/
@[simps]
def mapDomainRingHom (k : Type*) {H F : Type*} [Semiring k] [Monoid G] [Monoid H]
    [FunLike F G H] [MonoidHomClass F G H] (f : F) : MonoidAlgebraMonoidAlgebra k G →+* MonoidAlgebra k H :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebraMonoidAlgebra k G →+ MonoidAlgebra k H) with
    map_one' := mapDomain_one f
    map_mul' := fun x y => mapDomain_mul f x y }

Ring homomorphism induced by monoid homomorphism on monoid algebras

Informal description

Given a semiring $k$ and monoids $G$ and $H$, for any monoid homomorphism $f \colon G \to H$, the function $\text{mapDomainRingHom}\, f$ is a ring homomorphism from the monoid algebra $k[G]$ to $k[H]$ that maps a finitely supported function $v \colon G \to k$ to its image under domain mapping by $f$, i.e., $\text{mapDomain}\, f\, v$.

AddMonoidAlgebra.mapDomain abbrev

(f : M → N) (v : R[M]) : R[N]

Full source

abbrev mapDomain (f : M → N) (v : R[M]) : R[N] := Finsupp.mapDomain f v

Domain Mapping for Additive Monoid Algebra

Informal description

Given a semiring $R$, additive monoids $M$ and $N$, and a function $f : M \to N$, the function `mapDomain f` maps a finitely supported function $v : M \to_{\text{f}} R$ to a finitely supported function $N \to_{\text{f}} R$ by summing the values of $v$ over the preimages of $f$. More precisely, for any $n \in N$, the value of `mapDomain f v` at $n$ is given by: $$(\text{mapDomain } f \ v)(n) = \sum_{\substack{m \in M \\ f(m) = n}} v(m)$$

AddMonoidAlgebra.mapDomain_sum theorem

(f : M → N) (s : S[M]) (v : M → S → R[M]) :
    mapDomain f (s.sum v) = s.sum fun a b ↦ mapDomain f (v a b)

Full source

lemma mapDomain_sum (f : M → N) (s : S[M]) (v : M → S → R[M]) :
    mapDomain f (s.sum v) = s.sum fun a b ↦ mapDomain f (v a b) := Finsupp.mapDomain_sum

Summation Commutes with Domain Mapping in Additive Monoid Algebra

Informal description

Let $R$ be a semiring, $M$ and $N$ be additive monoids, $S$ be another additive monoid, and $f : M \to N$ be a function. For any finitely supported function $s : M \to_{\text{f}} S$ and any family of finitely supported functions $v : M \to S \to R[M]$, the domain mapping of the sum of $v$ over $s$ equals the sum over $s$ of the domain mappings of $v$. That is, \[ \operatorname{mapDomain}_f \left( \sum_{a \in M} s(a) \cdot v(a) \right) = \sum_{a \in M} s(a) \cdot \operatorname{mapDomain}_f (v(a)). \]

AddMonoidAlgebra.mapDomain_single theorem

: mapDomain f (single a r) = single (f a) r

Full source

lemma mapDomain_single : mapDomain f (single a r) = single (f a) r := Finsupp.mapDomain_single

Domain Mapping Preserves Single Generator in Additive Monoid Algebra

Informal description

Let $R$ be a semiring, $M$ and $N$ be additive monoids, and $f : M \to N$ be a function. For any element $a \in M$ and any scalar $r \in R$, the image of the single generator $\text{single}(a, r)$ under the domain mapping $f$ is equal to the single generator $\text{single}(f(a), r)$. That is, \[ \text{mapDomain}\, f\, (\text{single}\, a\, r) = \text{single}\, (f\, a)\, r. \]

AddMonoidAlgebra.mapDomain_injective theorem

(hf : Injective f) : Injective (mapDomain (R := R) f)

Full source

lemma mapDomain_injective (hf : Injective f) : Injective (mapDomain (R := R) f) :=
  Finsupp.mapDomain_injective hf

Injectivity of Domain Mapping in Additive Monoid Algebra

Informal description

Let $R$ be a semiring, $M$ and $N$ be additive monoids, and $f : M \to N$ be an injective function. Then the induced mapping $\text{mapDomain}\,f : R[M] \to R[N]$ on the additive monoid algebra is also injective.

AddMonoidAlgebra.mapDomain_one theorem

 {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Zero α] [Zero α₂] {F : Type*} [FunLike F α α₂] [ZeroHomClass F α α₂]
  (f : F) : (mapDomain f (1 : AddMonoidAlgebra β α) : AddMonoidAlgebra β α₂) = (1 : AddMonoidAlgebra β α₂)

Full source

/-- Like `Finsupp.mapDomain_zero`, but for the `1` we define in this file -/
@[simp]
theorem mapDomain_one {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Zero α] [Zero α₂]
    {F : Type*} [FunLike F α α₂] [ZeroHomClass F α α₂] (f : F) :
    (mapDomain f (1 : AddMonoidAlgebra β α) : AddMonoidAlgebra β α₂) =
      (1 : AddMonoidAlgebra β α₂) := by
  simp_rw [one_def, mapDomain_single, map_zero]

Preservation of Multiplicative Identity under Domain Mapping in Additive Monoid Algebra

Informal description

Let $R$ be a semiring, and let $G$ and $H$ be additive monoids with zero elements. Given a zero-preserving homomorphism $f : G \to H$, the image of the multiplicative identity $1 \in R[G]$ under the domain mapping $\text{mapDomain}\, f$ is equal to the multiplicative identity $1 \in R[H]$. In other words, for the additive monoid algebras $R[G]$ and $R[H]$, we have: \[ \text{mapDomain}\, f\, (1_{R[G]}) = 1_{R[H]}. \]

AddMonoidAlgebra.mapDomain_mul theorem

 {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Add α] [Add α₂] {F : Type*} [FunLike F α α₂] [AddHomClass F α α₂]
  (f : F) (x y : AddMonoidAlgebra β α) : mapDomain f (x * y) = mapDomain f x * mapDomain f y

Full source

/-- Like `Finsupp.mapDomain_add`, but for the convolutive multiplication we define in this file -/
theorem mapDomain_mul {α : Type*} {β : Type*} {α₂ : Type*} [Semiring β] [Add α] [Add α₂]
    {F : Type*} [FunLike F α α₂] [AddHomClass F α α₂] (f : F) (x y : AddMonoidAlgebra β α) :
    mapDomain f (x * y) = mapDomain f x * mapDomain f y := by
  simp_rw [mul_def, mapDomain_sum, mapDomain_single, map_add]
  rw [Finsupp.sum_mapDomain_index]
  · congr
    ext a b
    rw [Finsupp.sum_mapDomain_index]
    · simp
    · simp [mul_add]
  · simp
  · simp [add_mul]

Preservation of Convolution Product under Domain Mapping in Additive Monoid Algebra

Informal description

Let $k$ be a semiring, and let $G$ and $H$ be additive monoids. Given an additive homomorphism $f \colon G \to H$, the domain mapping $\operatorname{mapDomain}_f$ preserves the convolution product in the additive monoid algebra. That is, for any $x, y \in k[G]$, we have: \[ \operatorname{mapDomain}_f (x * y) = \operatorname{mapDomain}_f x * \operatorname{mapDomain}_f y. \]

AddMonoidAlgebra.mapDomainRingHom definition

 (k : Type*) [Semiring k] {H F : Type*} [AddMonoid G] [AddMonoid H] [FunLike F G H] [AddMonoidHomClass F G H] (f : F) :
  k[G] →+* k[H]

Full source

/-- If `f : G → H` is an additive homomorphism between two additive monoids, then
`Finsupp.mapDomain f` is a ring homomorphism between their add monoid algebras. -/
@[simps]
def mapDomainRingHom (k : Type*) [Semiring k] {H F : Type*} [AddMonoid G] [AddMonoid H]
    [FunLike F G H] [AddMonoidHomClass F G H] (f : F) : k[G]k[G] →+* k[H] :=
  { (Finsupp.mapDomain.addMonoidHom f : MonoidAlgebraMonoidAlgebra k G →+ MonoidAlgebra k H) with
    map_one' := mapDomain_one f
    map_mul' := fun x y => mapDomain_mul f x y }

Ring homomorphism induced by domain mapping of additive monoid algebra

Informal description

Given a semiring $k$ and additive monoids $G$ and $H$, for any additive monoid homomorphism $f \colon G \to H$, the function $\text{mapDomainRingHom}\, f$ is a ring homomorphism from the additive monoid algebra $k[G]$ to $k[H]$ that maps a finitely supported function $v \in k[G]$ to its image under domain mapping by $f$. More precisely, it satisfies: 1. $\text{mapDomainRingHom}\, f\, (1_{k[G]}) = 1_{k[H]}$ (preservation of multiplicative identity) 2. $\text{mapDomainRingHom}\, f\, (x * y) = (\text{mapDomainRingHom}\, f\, x) * (\text{mapDomainRingHom}\, f\, y)$ (preservation of multiplication) 3. $\text{mapDomainRingHom}\, f\, (x + y) = (\text{mapDomainRingHom}\, f\, x) + (\text{mapDomainRingHom}\, f\, y)$ (preservation of addition) 4. $\text{mapDomainRingHom}\, f\, 0 = 0$ (preservation of zero)

AddMonoidAlgebra.toMultiplicative definition

[Semiring k] [Add G] : AddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G)

Full source

/-- The equivalence between `AddMonoidAlgebra` and `MonoidAlgebra` in terms of
`Multiplicative` -/
protected def AddMonoidAlgebra.toMultiplicative [Semiring k] [Add G] :
    AddMonoidAlgebraAddMonoidAlgebra k G ≃+* MonoidAlgebra k (Multiplicative G) :=
  { Finsupp.domCongr
      Multiplicative.ofAdd with
    toFun := equivMapDomain Multiplicative.ofAdd
    map_mul' := fun x y => by
      repeat' rw [equivMapDomain_eq_mapDomain (M := k)]
      dsimp [Multiplicative.ofAdd]
      exact MonoidAlgebra.mapDomain_mul (α := Multiplicative G) (β := k)
        (MulHom.id (Multiplicative G)) x y }

Ring equivalence between additive and multiplicative monoid algebras

Informal description

The function provides a ring equivalence between the additive monoid algebra $k[G]$ and the monoid algebra $k[\text{Multiplicative}\,G]$, where $\text{Multiplicative}\,G$ is the multiplicative monoid obtained from the additive monoid $G$ via the type tag $\text{Multiplicative}$. Specifically, it maps a finitely supported function $f \colon G \to₀ k$ to the finitely supported function $\text{Multiplicative}\,G \to₀ k$ defined by $(\text{Multiplicative.ofAdd}\,g) \mapsto f(g)$, where $\text{Multiplicative.ofAdd}$ is the canonical bijection between $G$ and $\text{Multiplicative}\,G$. This equivalence preserves both the additive and multiplicative structures of the algebras.

MonoidAlgebra.toAdditive definition

[Semiring k] [Mul G] : MonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G)

Full source

/-- The equivalence between `MonoidAlgebra` and `AddMonoidAlgebra` in terms of `Additive` -/
protected def MonoidAlgebra.toAdditive [Semiring k] [Mul G] :
    MonoidAlgebraMonoidAlgebra k G ≃+* AddMonoidAlgebra k (Additive G) :=
  { Finsupp.domCongr Additive.ofMul with
    toFun := equivMapDomain Additive.ofMul
    map_mul' := fun x y => by
      repeat' rw [equivMapDomain_eq_mapDomain (M := k)]
      dsimp [Additive.ofMul]
      convert MonoidAlgebra.mapDomain_mul (β := k) (MulHom.id G) x y }

Ring equivalence between monoid algebra and additive monoid algebra via Additive type tag

Informal description

The ring equivalence between the monoid algebra $k[G]$ over a semiring $k$ generated by a multiplicative monoid $G$ and the additive monoid algebra $k[\text{Additive } G]$ over the same semiring $k$ generated by the additive monoid $\text{Additive } G$. This equivalence is constructed by reinterpreting the multiplicative structure of $G$ as an additive structure via the type tag $\text{Additive } G$, while preserving the underlying $k$-linear combinations. The equivalence maps a finitely supported function $f \colon G \to k$ to the corresponding finitely supported function $\text{Additive } G \to k$ via the bijection $\text{Additive.ofMul} \colon G \simeq \text{Additive } G$.