MonoidAlgebra.nonUnitalAlgHom_ext'
theorem MonoidAlgebra.nonUnitalAlgHom_ext' :
∀ (k : Type u₁) {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] {A : Type u₃}
[inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction k A]
{φ₁ φ₂ : MonoidAlgebra k G →ₛₙₐ[MonoidHom.id k] A},
φ₁.toMulHom.comp (MonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (MonoidAlgebra.ofMagma k G) → φ₁ = φ₂
The theorem `MonoidAlgebra.nonUnitalAlgHom_ext'` asserts that for any given semiring `k`, type `G` with multiplication operation, and another type `A` which is a non-unital, non-associative semiring with a distribution of multiplication over addition, if we have two non-unital algebra homomorphisms `φ₁` and `φ₂` from the monoid algebra over `k` generated by `G` to `A`, then `φ₁` and `φ₂` are equal if and only if their corresponding multiplication homomorphisms, after being composed with the embedding of `G` into its monoid algebra, are also equal.
More concisely: Given semirings `k`, type `G` with multiplication `*` and distribution over addition, and non-unital algebra homomorphisms `φ₁` and `φ₂` from the monoid algebra over `k` generated by `G` to a non-unital, non-associative semiring `A`, `φ₁ = φ₂` if and only if the multiplication homomorphisms `μ₁` and `μ₂` induced by `φ₁` and `φ₂`, respectively, satisfy `μ₁(x * y) = μ₂(x * y)` for all `x, y ∈ G`.
|
AddMonoidAlgebra.mapDomain_mul
theorem AddMonoidAlgebra.mapDomain_mul :
∀ {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [inst : Semiring β] [inst_1 : Add α] [inst_2 : Add α₂]
{F : Type u_6} [inst_3 : FunLike F α α₂] [inst_4 : AddHomClass F α α₂] (f : F) (x y : AddMonoidAlgebra β α),
AddMonoidAlgebra.mapDomain (⇑f) (x * y) = AddMonoidAlgebra.mapDomain (⇑f) x * AddMonoidAlgebra.mapDomain (⇑f) y
The theorem `AddMonoidAlgebra.mapDomain_mul` states that for any two elements `x` and `y` of an additively-structured monoid algebra over a semiring `β` and generated by `α`, and for any function `f` that is both a homomorphism between additive structures and injective when coerced to a function from `α` to some type `α₂`, the process of mapping the domain of the product of `x` and `y` under the function `f` is the same as individually mapping the domains of `x` and `y` under `f` and then taking their product. In other words, domain-mapping under `f` preserves multiplication in the additively-structured monoid algebra.
More concisely: For any additively-structured monoid algebra over a semiring, any homomorphism and injective function between its generating set preserves multiplication when applied to the domains of elements.
|
AddMonoidAlgebra.mul_single_apply_aux
theorem AddMonoidAlgebra.mul_single_apply_aux :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] (f : AddMonoidAlgebra k G) (r : k) (x y z : G),
(∀ (a : G), a + x = z ↔ a = y) → (f * AddMonoidAlgebra.single x r) z = f y * r
This theorem states that for any semiring `k`, any type `G` that has addition, any `f` which is an additive monoid algebra of `k` and `G`, any `r` of type `k`, and any `x`, `y`, and `z` of type `G`, such that for all `a` of type `G`, `a` plus `x` equals `z` if and only if `a` equals `y`, then the result of multiplying `f` with the additive monoid algebra single `x` and `r` at `z` is equal to the multiplication of `f` at `y` and `r`. In other words, it describes a property of multiplication in the context of additive monoid algebras, particularly in relation to the `single` function.
More concisely: For any semiring `k`, additive monoid algebra `f` of `k` and type `G`, if for all `x, y, z, a` in `G`, `a + x = z` if and only if `a = y` implies `f(y) * r = f(x) * r * z`, then `f(y) * r = f(single x) * r * z`.
|
AddMonoidAlgebra.algHom_ext'
theorem AddMonoidAlgebra.algHom_ext' :
∀ {k : Type u₁} {G : Type u₂} [inst : CommSemiring k] [inst_1 : AddMonoid G] {A : Type u₃} [inst_2 : Semiring A]
[inst_3 : Algebra k A] ⦃φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A⦄,
(↑φ₁).comp (AddMonoidAlgebra.of k G) = (↑φ₂).comp (AddMonoidAlgebra.of k G) → φ₁ = φ₂
The theorem `AddMonoidAlgebra.algHom_ext'` states that for any commutative semiring `k`, an additive monoid `G`, another semiring `A` that is also a `k`-algebra, and two algebra homomorphisms `φ₁` and `φ₂` from the monoid algebra over `k` generated by `G` to `A`, if the composition of `φ₁` and the embedding of `G` into its monoid algebra is equivalent to the composition of `φ₂` and the same embedding, then `φ₁` is identical to `φ₂`. In other words, two algebra homomorphisms from the monoid algebra to `A` are the same if they give the same result when applied to elements of `G` embedded into the monoid algebra.
More concisely: If two algebra homomorphisms from the monoid algebra generated by a commutative semigroup to a semiring have identical compositions with the embedding of the semigroup into the algebra, then they are equal.
|
MonoidAlgebra.nonUnitalAlgHom_ext
theorem MonoidAlgebra.nonUnitalAlgHom_ext :
∀ (k : Type u₁) {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] {A : Type u₃}
[inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction k A]
{φ₁ φ₂ : MonoidAlgebra k G →ₛₙₐ[MonoidHom.id k] A},
(∀ (x : G), φ₁ (MonoidAlgebra.single x 1) = φ₂ (MonoidAlgebra.single x 1)) → φ₁ = φ₂
The theorem `MonoidAlgebra.nonUnitalAlgHom_ext` states that, given a semiring `k`, a mulitiplicative set `G`, and a non-unital, non-associative semiring `A` with a distributive mulitiplicative action by `k`, any two non-unital `k`-algebra homomorphisms from the monoid algebra over `k` generated by `G` to `A` that agree on the values of the function `single a 1` for all `a` in `G` (where `single a 1` is the function that assigns `1` to the element `a` and `0` to all other elements), are equal. This theorem therefore provides a uniqueness criterion for non-unital `k`-algebra homomorphisms based on their values on a specific set of generator functions.
More concisely: Given a semiring `k`, a multiplicative set `G`, and non-unital, non-associative semirings `A` with a distributive multiplicative action by `k`, any two non-unital `k`-algebra homomorphisms from the monoid algebra over `k` generated by `G` that agree on the values of `single a 1` for all `a` in `G`, are equal.
|
MonoidAlgebra.sum_single_index
theorem MonoidAlgebra.sum_single_index :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] {N : Type u_3} [inst_1 : AddCommMonoid N] {a : G} {b : k}
{h : G → k → N}, h a 0 = 0 → Finsupp.sum (MonoidAlgebra.single a b) h = h a b
The theorem `MonoidAlgebra.sum_single_index` states that for any types `k` and `G` with an instance of semiring `k`, and for any type `N` with an instance of additive commutative monoid, given a function `h` from `G` and `k` to `N` such that `h a 0 = 0` for any `a` in `G`, and any `a` of type `G` and `b` of type `k`, the sum of `h a (f a)` over the support of `f` (where `f` is the monoid algebra of a single element `a` with coefficient `b`) is equal to `h a b`. This means that when you apply the sum operation on the single element monoid algebra, the result is the same as directly applying `h` to `a` and `b`.
More concisely: For any semiring `k`, additive commutative monoid `N`, type `G` with semiring instance, function `h` from `G x k` to `N` with `h a 0 = 0`, and element `a` of type `G`, the sum of `h` applied to `a` and the monoid algebra of `a` with coefficient `b` equals `h a b`.
|
MonoidAlgebra.sum_single
theorem MonoidAlgebra.sum_single :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] (f : MonoidAlgebra k G), Finsupp.sum f MonoidAlgebra.single = f
The theorem `MonoidAlgebra.sum_single` states that for any semiring `k` and any type `G`, and for any monoid algebra `f` over `k` generated by `G`, the sum of the application of the function `MonoidAlgebra.single` to each element in the support of `f` (which is computed via `Finsupp.sum`) is equal to `f` itself. In simpler terms, this result describes an important property of the algebraic structure called a monoid algebra, specifically how summing over its elements using a certain operation gives back the original monoid algebra.
More concisely: For any semiring `k` and type `G`, the sum of the monoid algebra `f` over `k` generated by `G`, as the application of `MonoidAlgebra.single` to each element in its support, equals `f` itself.
|
MonoidAlgebra.single_zero
theorem MonoidAlgebra.single_zero :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] (a : G), MonoidAlgebra.single a 0 = 0
The theorem `MonoidAlgebra.single_zero` states that for any type `k` under the semiring structure, and any type `G`, if we apply the `MonoidAlgebra.single` function to any element 'a' of `G` and the zero of `k`, it yields the zero of the `MonoidAlgebra`. In other words, in the context of monoid algebras, "singling out" an element with a zero coefficient results in the zero element of the corresponding monoid algebra.
More concisely: For any semiring `k` and monoid `G`, applying `MonoidAlgebra.single` to an element `a` in `G` and the zero of `k` results in the zero of the monoid algebra `MonoidAlgebra k G`.
|
AddMonoidAlgebra.nonUnitalAlgHom_ext'
theorem AddMonoidAlgebra.nonUnitalAlgHom_ext' :
∀ (k : Type u₁) {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] {A : Type u₃}
[inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction k A]
{φ₁ φ₂ : AddMonoidAlgebra k G →ₛₙₐ[MonoidHom.id k] A},
φ₁.toMulHom.comp (AddMonoidAlgebra.ofMagma k G) = φ₂.toMulHom.comp (AddMonoidAlgebra.ofMagma k G) → φ₁ = φ₂
This theorem states that for any semiring `k`, additive group `G`, and non-unital non-associative semiring `A` (with `A` also being a `k`-module), given two non-unital `k`-algebra homomorphisms `φ₁` and `φ₂` from the monoid algebra of `G` over `k` to `A`, if the compositions of `φ₁` and `φ₂` with the embedding of `G` into its monoid algebra coincide, then `φ₁` and `φ₂` must be the same. In more mathematical terms, if `φ₁ ∘ ι = φ₂ ∘ ι` for the embedding map `ι` of `G` into its monoid algebra, then `φ₁ = φ₂`.
More concisely: Two non-unital `k`-algebra homomorphisms from the monoid algebra of a group `G` over a semiring `k` to a non-unital `k`-module semiring `A` are equal if and only if their compositions with the embedding of `G` into its monoid algebra are equal.
|
AddMonoidAlgebra.of'_apply
theorem AddMonoidAlgebra.of'_apply :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] (a : G),
AddMonoidAlgebra.of' k G a = AddMonoidAlgebra.single a 1
This theorem states that for any types `k` and `G`, given that `k` has a `Semiring` structure and for any element `a` of type `G`, the application of the `AddMonoidAlgebra.of'` function with the types `k` and `G`, and the variable `a`, is equivalent to the application of the `AddMonoidAlgebra.single` function with the variables `a` and `1`. In other words, the embedding of a magma with zero `G`, into its magma algebra, having `G` as the source, maps an element `a` to the single value of the algebra associated with `a` and `1`.
More concisely: For any semiring `k` and type `G` with an element `a`, the `AddMonoidAlgebra.of' k G a` is equal to `AddMonoidAlgebra.single a 1` in `AddMonoidAlgebra k G`.
|
AddMonoidAlgebra.nonUnitalAlgHom_ext
theorem AddMonoidAlgebra.nonUnitalAlgHom_ext :
∀ (k : Type u₁) {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] {A : Type u₃}
[inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction k A]
{φ₁ φ₂ : AddMonoidAlgebra k G →ₛₙₐ[MonoidHom.id k] A},
(∀ (x : G), φ₁ (AddMonoidAlgebra.single x 1) = φ₂ (AddMonoidAlgebra.single x 1)) → φ₁ = φ₂
The theorem `AddMonoidAlgebra.nonUnitalAlgHom_ext` states that for any semiring `k`, additive group `G`, and any non-unital, non-associative semiring `A` with an action of `k`, if two non-unital `k`-algebra homomorphisms from the monoid algebra `k[G]` to `A` coincide on the images of the functions `single a 1` for all `a` in `G`, then the two homomorphisms are equal. In short, a non-unital `k`-algebra homomorphism from `k[G]` to `A` is uniquely determined by its values on the `single a 1` functions.
More concisely: If `k` is a semiring, `G` is an additive group, `A` is a non-unital, non-associative semiring with a `k`-action, and two homomorphisms from `k[G]` to `A` agree on the images of `single a 1` for all `a` in `G`, then these homomorphisms are equal.
|
MonoidAlgebra.mapDomain_mul
theorem MonoidAlgebra.mapDomain_mul :
∀ {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [inst : Semiring β] [inst_1 : Mul α] [inst_2 : Mul α₂]
{F : Type u_6} [inst_3 : FunLike F α α₂] [inst_4 : MulHomClass F α α₂] (f : F) (x y : MonoidAlgebra β α),
MonoidAlgebra.mapDomain (⇑f) (x * y) = MonoidAlgebra.mapDomain (⇑f) x * MonoidAlgebra.mapDomain (⇑f) y
The theorem `MonoidAlgebra.mapDomain_mul` states that for any semiring `β`, multiplicative structures `α` and `α₂`, a function `f` from `α` to `α₂` that preserves multiplication, and two elements `x` and `y` from the monoid algebra over `β` generated by `α`, the operation of mapping the domain of the product of `x` and `y` using `f` is equivalent to the product of the domain mappings of `x` and `y` individually by `f`. In other words, it asserts that the `mapDomain` operation commutes with the convolution multiplication in the monoid algebra.
More concisely: For any semiring β, multiplicative structures α and α₂, and a multiplicative function f from α to α₂, the mapDomain operation of the product of elements x and y in the monoid algebra over β, with respect to f, is equal to the product of the mapDomain mappings of x and y by f.
|
MonoidAlgebra.mul_single_apply_aux
theorem MonoidAlgebra.mul_single_apply_aux :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G},
(∀ (a : G), a * x = z ↔ a = y) → (f * MonoidAlgebra.single x r) z = f y * r
The theorem `MonoidAlgebra.mul_single_apply_aux` states that for any semiring `k`, any multiplicative group `G`, a monoid algebra `f` over `k` and `G`, and any elements `r` in `k`, `x`, `y`, and `z` in `G` such that for any element `a` in `G`, the equality `a * x = z` holds if and only if `a = y`, then the product of `f` and the monoid algebra generated by `x` and `r` evaluated at `z` equals the product of `f` evaluated at `y` and `r`.
More concisely: Given a semiring `k`, a multiplicative group `G`, a monoid algebra `f` over `k` and `G`, and `x`, `y` in `G` such that `x * a = z` if and only if `a = y`, then `f * (algBase x r) = f y * r`.
|
MonoidAlgebra.algHom_ext'
theorem MonoidAlgebra.algHom_ext' :
∀ {k : Type u₁} {G : Type u₂} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u₃} [inst_2 : Semiring A]
[inst_3 : Algebra k A] ⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄,
(↑φ₁).comp (MonoidAlgebra.of k G) = (↑φ₂).comp (MonoidAlgebra.of k G) → φ₁ = φ₂
This theorem states that for any commutative semiring `k`, any monoid `G`, and any semiring `A` that is also an algebra over `k`, if we have two algebra homomorphisms `φ₁` and `φ₂` from the monoid algebra of `G` over `k` to `A`, then if the composition of `φ₁` with the embedding of `G` into its monoid algebra is equal to the composition of `φ₂` with the same embedding, the two algebra homomorphisms `φ₁` and `φ₂` must be equal.
More concisely: If `φ₁` and `φ₂` are algebra homomorphisms from the monoid algebra of a commutative monoid `G` over a commutative semiring `k` to a semiring `A` that is an `k`-algebra, and `φ₁ ∘ i = φ₂ ∘ i`, where `i` is the embedding of `G` into its monoid algebra, then `φ₁ = φ₂`.
|
MonoidAlgebra.single_mul_apply_aux
theorem MonoidAlgebra.single_mul_apply_aux :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] (f : MonoidAlgebra k G) {r : k} {x y z : G},
(∀ (a : G), x * a = y ↔ a = z) → (MonoidAlgebra.single x r * f) y = r * f z
This theorem, `MonoidAlgebra.single_mul_apply_aux`, is about the monoid algebra generated over a semiring `k` by a monoid `G`. It states that for all instances `k` of a semiring, all instances `G` of a multiplicative monoid, any `f` in the monoid algebra of `k` and `G`, any element `r` of `k`, and any elements `x`, `y`, and `z` of `G`, such that for every element `a` in `G`, `x * a` equals `y` if and only if `a` equals `z`. Under these conditions, the theorem asserts that the convolution of the single-element monoid algebra generated by `x` and `r`, and `f`, evaluated at `y`, is equal to `r` multiplied by `f` evaluated at `z`.
More concisely: For any semiring `k`, multiplicative monoid `G`, `f` in the monoid algebra of `k` and `G`, `r` in `k`, and `x`, `y`, `z` in `G` such that `x * a = y` if and only if `a = z`, the convolution of the single-element monoid algebra generated by `x` and `r`, and `f`, equals `r * f(z)`.
|
MonoidAlgebra.mapDomain_one
theorem MonoidAlgebra.mapDomain_one :
∀ {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [inst : Semiring β] [inst_1 : One α] [inst_2 : One α₂]
{F : Type u_6} [inst_3 : FunLike F α α₂] [inst_4 : OneHomClass F α α₂] (f : F),
MonoidAlgebra.mapDomain (⇑f) 1 = 1
The theorem `MonoidAlgebra.mapDomain_one` states that for any types `α`, `β`, `α₂`, and `F`; given a semiring structure on `β`, a `One` structure (i.e., a type with a distinguished "one" element) on `α` and `α₂`, a `FunLike` structure from `α` to `α₂` on `F`, and a `OneHomClass` structure (i.e., a class of functions preserving the "one" element) on `F` from `α` to `α₂`; for any function `f` of type `F`, if we map the domain of the one element of the monoid algebra of `α` using the function `f`, we will get the one element of the monoid algebra of `α₂`. In simpler terms, it says that the one element of a monoid algebra remains unchanged when we apply an operation that preserves the "one" element.
More concisely: For any semiring `β`, type `α` with a One structure, FunLike `F` from `α` to `α₂`, OneHomClass `F` from `α` to `α₂`, and function `f` of type `F` preserving the one element, the one element of the monoid algebra of `α` maps to the one element of the monoid algebra of `α₂` under `f`.
|
AddMonoidAlgebra.lift_unique
theorem AddMonoidAlgebra.lift_unique :
∀ {k : Type u₁} {G : Type u₂} [inst : CommSemiring k] [inst_1 : AddMonoid G] {A : Type u₃} [inst_2 : Semiring A]
[inst_3 : Algebra k A] (F : AddMonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G),
F f = Finsupp.sum f fun a b => b • F (AddMonoidAlgebra.single a 1)
The theorem `AddMonoidAlgebra.lift_unique` states that given a `k`-algebra homomorphism `F` from the `MonoidAlgebra k G` to a semiring `A`, and a `MonoidAlgebra k G` element `f`, the value of `F` at `f` can be uniquely decomposed as the sum, over the support of `f`, of the product of `b` and the value of `F` at the singleton `a` with coefficient `1`.
In other words, for a commutative semiring `k`, an additive monoid `G`, a semiring `A` with a `k`-algebra structure, a `k`-algebra homomorphism `F` from `AddMonoidAlgebra k G` to `A`, and a `MonoidAlgebra` element `f`, the `k`-algebra homomorphism `F` maps `f` to the sum of `b • F (AddMonoidAlgebra.single a 1)` for each `(a, b)` in the support of `f`. This sum is essentially a weighted sum of the images under `F` of the `k`-linear combinations of terms of `G` with coefficient `1`.
More concisely: Given a commutative semiring $k$, an additive monoid $G$, a semiring $A$ with a $k$-algebra structure, a $k$-algebra homomorphism $F$ from $AddMonoidAlgebra\ k\ G$ to $A$, and an element $f$ in $AddMonoidAlgebra\ k\ G$, the image of $f$ under $F$ is uniquely the sum, over the support of $f$, of the products of the image of the singleton under $F$ with coefficient $1$.
|
AddMonoidAlgebra.algHom_ext
theorem AddMonoidAlgebra.algHom_ext :
∀ {k : Type u₁} {G : Type u₂} [inst : CommSemiring k] [inst_1 : AddMonoid G] {A : Type u₃} [inst_2 : Semiring A]
[inst_3 : Algebra k A] ⦃φ₁ φ₂ : AddMonoidAlgebra k G →ₐ[k] A⦄,
(∀ (x : G), φ₁ (AddMonoidAlgebra.single x 1) = φ₂ (AddMonoidAlgebra.single x 1)) → φ₁ = φ₂
The theorem `AddMonoidAlgebra.algHom_ext` states that for any commutative semiring `k`, any additive monoid `G`, any semiring `A`, and any `k`-algebra structure on `A`, if two `k`-algebra homomorphisms from the monoid algebra `k[G]` to `A` are such that they map the function `single a 1` to the same value for all `a` in `G`, then the two homomorphisms are identical. In simpler terms, a `k`-algebra homomorphism from `k[G]` is completely determined by its values on elements of the form `single a 1`.
More concisely: Given a commutative semiring `k`, an additive monoid `G`, a semiring `A`, and two `k`-algebra homomorphisms from `k[G]` to `A` that agree on the element `single a 1` for all `a` in `G`, these homomorphisms are equal.
|
AddMonoidAlgebra.mapDomain_one
theorem AddMonoidAlgebra.mapDomain_one :
∀ {α : Type u_3} {β : Type u_4} {α₂ : Type u_5} [inst : Semiring β] [inst_1 : Zero α] [inst_2 : Zero α₂]
{F : Type u_6} [inst_3 : FunLike F α α₂] [inst_4 : ZeroHomClass F α α₂] (f : F),
AddMonoidAlgebra.mapDomain (⇑f) 1 = 1
The theorem `AddMonoidAlgebra.mapDomain_one` states that for any types `α`, `β`, `α₂`, and `F`, given a semiring structure on `β`, zero elements in `α` and `α₂`, a function `F` that behaves like a function from `α` to `α₂` (in the sense of the `FunLike` class), and a zero-preserving homomorphism from `α` to `α₂` (in the sense of the `ZeroHomClass`), then mapping the domain of the '1' element in the `AddMonoidAlgebra` using the function `F` yields the '1' element. In other words, this theorem states that the operation of mapping the domain in this way preserves the '1' element of the algebra.
More concisely: Given a semiring `β` with zero elements, a function `F` behaving like a map from type `α` to `α₂`, and a zero-preserving homomorphism from `α` to `α₂`, the map of the '1' element in the `AddMonoidAlgebra` of `α` under `F` equals the '1' element in the `AddMonoidAlgebra` of `α₂`.
|
AddMonoidAlgebra.single_mul_apply_aux
theorem AddMonoidAlgebra.single_mul_apply_aux :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] (f : AddMonoidAlgebra k G) (r : k) (x y z : G),
(∀ (a : G), x + a = y ↔ a = z) → (AddMonoidAlgebra.single x r * f) y = r * f z
The theorem `AddMonoidAlgebra.single_mul_apply_aux` states that for any type `k`, any additive monoid `G`, any element `f` of the monoid algebra of `k` generated by `G`, any element `r` of type `k`, and any elements `x`, `y`, and `z` of `G` such that for every `a` in `G`, `x + a = y` if and only if `a = z`, then the result of multiplying `AddMonoidAlgebra.single x r` and `f` at the point `y` is equal to the result of multiplying `r` and `f` at the point `z`. In other words, this theorem is about the interaction of multiplication in the monoid algebra with addition in the underlying additive monoid.
More concisely: For any additive monoid `G`, any element `f` of its monoid algebra, and any elements `r`, `x`, `y`, and `z` in `G` such that `x + a = y` if and only if `a = z`, the multiplication of `AddMonoidAlgebra.single x r` and `f` at `y` equals the multiplication of `r` and `f` at `z`.
|
MonoidAlgebra.single_mul_apply
theorem MonoidAlgebra.single_mul_apply :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Group G] (r : k) (x : G) (f : MonoidAlgebra k G)
(y : G), (MonoidAlgebra.single x r * f) y = r * f (x⁻¹ * y)
This theorem states that for any semiring `k`, group `G`, scalar `r` from `k`, group element `x` from `G`, and a formal linear combination `f` in the monoid algebra of `G` with coefficients in `k`, the convolution of the singleton formal linear combination of `x` and `r` with `f`, evaluated at a group element `y`, equals `r` times the evaluation of `f` at the element `x⁻¹ * y`. In simpler terms, this is a distributive property showing how multiplication distributes over the convolution in the monoid algebra.
More concisely: For any semiring `k`, group `G`, scalar `r` from `k`, group elements `x, y` from `G`, and formal linear combination `f` in the monoid algebra of `G` with coefficients in `k`, we have `(rx : k) * (f ! x) ^-1 * f = r * f ! (x ^-1 * y)`.
|
MonoidAlgebra.lift_unique
theorem MonoidAlgebra.lift_unique :
∀ {k : Type u₁} {G : Type u₂} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u₃} [inst_2 : Semiring A]
[inst_3 : Algebra k A] (F : MonoidAlgebra k G →ₐ[k] A) (f : MonoidAlgebra k G),
F f = Finsupp.sum f fun a b => b • F (MonoidAlgebra.single a 1)
This theorem, `MonoidAlgebra.lift_unique`, states that for any commutative semiring `k`, any monoid `G`, any semiring `A`, and any `k`-algebra `A`, any `k`-algebra homomorphism `F` from the monoid algebra generated by `G` over `k` to `A` can be uniquely decomposed by its values on `F` applied to `single a 1` (i.e., the monoid algebra element determined by a single element `a` of `G` with a coefficient of `1`). More specifically, the value of `F` at any point `f` in the monoid algebra is equal to the sum, over all elements `a` in the support of `f`, of the product of the coefficient `b` at `a` of `f` and `F` applied to `single a 1`, scaled by `b` (denoted `b • F (MonoidAlgebra.single a 1)`).
More concisely: Given a commutative semiring `k`, a monoid `G` over `k`, a semiring `A`, and a `k`-algebra homomorphism `F` from the monoid algebra of `G` over `k` to `A`, the decomposition of `F` in terms of its values on `single a 1` for each `a` in the monoid is unique, where `F(f)` equals the sum, over all `a` in the support of `f`, of the product of the coefficient `b` of `a` in `f` and `F(single a 1)` scaled by `b`.
|
AddMonoidAlgebra.ringHom_ext
theorem AddMonoidAlgebra.ringHom_ext :
∀ {k : Type u₁} {G : Type u₂} {R : Type u_3} [inst : Semiring k] [inst_1 : AddMonoid G] [inst_2 : Semiring R]
{f g : AddMonoidAlgebra k G →+* R},
(∀ (b : k), f (AddMonoidAlgebra.single 0 b) = g (AddMonoidAlgebra.single 0 b)) →
(∀ (a : G), f (AddMonoidAlgebra.single a 1) = g (AddMonoidAlgebra.single a 1)) → f = g
This theorem states that if we have two ring homomorphisms from the monoid algebra `k[G]` to some semiring `R`, denoted as `f` and `g`, then if they are equal on all elements of the form `single a 1` for all `a` in `G` and `single 0 b` for all `b` in `k`, then the two ring homomorphisms `f` and `g` are actually equal. Here, `single a b` represents a finite formal `k`-linear combination of terms of `G`, where only the term `a` has a coefficient not equal to 0 (namely `b`).
More concisely: If two ring homomorphisms from the monoid algebra `k[G]` to a semiring agree on all elements of the form `single a 1` for all `a` in `G` and `single 0 b` for all `b` in `k`, then they are equal.
|
AddMonoidAlgebra.ringHom_ext'
theorem AddMonoidAlgebra.ringHom_ext' :
∀ {k : Type u₁} {G : Type u₂} {R : Type u_3} [inst : Semiring k] [inst_1 : AddMonoid G] [inst_2 : Semiring R]
{f g : AddMonoidAlgebra k G →+* R},
f.comp AddMonoidAlgebra.singleZeroRingHom = g.comp AddMonoidAlgebra.singleZeroRingHom →
(↑f).comp (AddMonoidAlgebra.of k G) = (↑g).comp (AddMonoidAlgebra.of k G) → f = g
The theorem `AddMonoidAlgebra.ringHom_ext'` states that for a given semiring `k`, an additive monoid `G`, and another semiring `R`, if there are two ring homomorphisms `f` and `g` from the additive monoid algebra `k[G]` to `R`, and they agree on all the elements of the form `single a 1` and `single 0 b`, then these two homomorphisms are identical.
In more detail, if the composition of `f` and `AddMonoidAlgebra.singleZeroRingHom` is equal to the composition of `g` and `AddMonoidAlgebra.singleZeroRingHom`, and further, the composition of `f` and `AddMonoidAlgebra.of` is equal to the composition of `g` and `AddMonoidAlgebra.of`, then `f` must be equal to `g`.
More concisely: If two ring homomorphisms from the additive monoid algebra of an additive semigroup over a semiring to another semiring agree on the constants and the generators, then they are equal.
|
MonoidAlgebra.lift_single
theorem MonoidAlgebra.lift_single :
∀ {k : Type u₁} {G : Type u₂} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u₃} [inst_2 : Semiring A]
[inst_3 : Algebra k A] (F : G →* A) (a : G) (b : k),
((MonoidAlgebra.lift k G A) F) (MonoidAlgebra.single a b) = b • F a
This theorem states that for any commutative semiring `k`, any monoid `G`, any semiring `A` with a `k`-algebra structure, any monoid homomorphism `F` from `G` to `A`, and any elements `a` from `G` and `b` from `k`, the result of lifting `F` to an algebra homomorphism and then applying this to the monoid algebra element corresponding to `a` and `b`, is equal to `b` times `F(a)` in the `A` algebra. In other words, the lifting operation respects the operation of the monoid algebra.
More concisely: For any commutative semiring `k`, monoid `G`, `k`-algebra `A` over `G`, monoid homomorphism `F` from `G` to `A`, and elements `a` from `G` and `b` from `k`, the lifting of `F` to an algebra homomorphism and application to the monoid algebra elements `a * x` and `b` results in `b * F(a)` in `A`. (Here, `*` denotes the monoid and algebra multiplication.)
|
MonoidAlgebra.algHom_ext
theorem MonoidAlgebra.algHom_ext :
∀ {k : Type u₁} {G : Type u₂} [inst : CommSemiring k] [inst_1 : Monoid G] {A : Type u₃} [inst_2 : Semiring A]
[inst_3 : Algebra k A] ⦃φ₁ φ₂ : MonoidAlgebra k G →ₐ[k] A⦄,
(∀ (x : G), φ₁ (MonoidAlgebra.single x 1) = φ₂ (MonoidAlgebra.single x 1)) → φ₁ = φ₂
This theorem states that for any given commutative semiring `k`, monoid `G`, semiring `A`, and `k`-algebra `A`, an algebra homomorphism from the monoid algebra `MonoidAlgebra k G` to `A` is uniquely determined by its values on the functions `MonoidAlgebra.single a 1` for all `a` in `G`. In other words, if two such homomorphisms `φ₁` and `φ₂` agree on the values of `MonoidAlgebra.single a 1` for every `a` in `G`, then they must be the same homomorphism.
More concisely: Given a commutative semiring `k`, a monoid `G`, a semiring `A`, and a `k`-algebra `A`, any two algebra homomorphisms from `MonoidAlgebra k G` to `A` that agree on the values of `MonoidAlgebra.single a 1` for all `a` in `G` are equal.
|
MonoidAlgebra.ringHom_ext
theorem MonoidAlgebra.ringHom_ext :
∀ {k : Type u₁} {G : Type u₂} {R : Type u_3} [inst : Semiring k] [inst_1 : MulOneClass G] [inst_2 : Semiring R]
{f g : MonoidAlgebra k G →+* R},
(∀ (b : k), f (MonoidAlgebra.single 1 b) = g (MonoidAlgebra.single 1 b)) →
(∀ (a : G), f (MonoidAlgebra.single a 1) = g (MonoidAlgebra.single a 1)) → f = g
The theorem `MonoidAlgebra.ringHom_ext` states that for any two ring homomorphisms `f` and `g` from the monoid algebra of a monoid `G` over a semiring `k` to another semiring `R`, if they are equal when applied to all elements of the form `single 1 b` for any `b` in `k`, and also equal when applied to all elements of the form `single a 1` for any `a` in `G`, then the two ring homomorphisms are indeed equal. Essentially, this means that the equality of two such ring homomorphisms can be determined solely by their behavior on the basis elements formed by `single 1 b` and `single a 1`.
More concisely: If two ring homomorphisms from the monoid algebra of a monoid over a semiring to another semiring agree on elements of the form `single 1 b` for all `b` in the semiring and elements of the form `single a 1` for all `a` in the monoid, then they are equal.
|
MonoidAlgebra.ringHom_ext'
theorem MonoidAlgebra.ringHom_ext' :
∀ {k : Type u₁} {G : Type u₂} {R : Type u_3} [inst : Semiring k] [inst_1 : MulOneClass G] [inst_2 : Semiring R]
{f g : MonoidAlgebra k G →+* R},
f.comp MonoidAlgebra.singleOneRingHom = g.comp MonoidAlgebra.singleOneRingHom →
(↑f).comp (MonoidAlgebra.of k G) = (↑g).comp (MonoidAlgebra.of k G) → f = g
This theorem states that, given two ring homomorphisms `f` and `g` from the monoid algebra `MonoidAlgebra k G` to some semiring `R`, if these homomorphisms agree on the images of all elements `a` and `b` under the mappings `single a 1` and `single 1 b` respectively, then the homomorphisms `f` and `g` are equal. This establishes a criterion for equality of ring homomorphisms based on their behavior with respect to these specific mappings.
More concisely: If two ring homomorphisms from the monoid algebra of a group into some semiring agree on the images of `single a 1` and `single 1 b` for all group elements `a` and `b`, then they are equal.
|
AddMonoidAlgebra.single_zero_mul_apply
theorem AddMonoidAlgebra.single_zero_mul_apply :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : AddZeroClass G] (f : AddMonoidAlgebra k G) (r : k)
(x : G), (AddMonoidAlgebra.single 0 r * f) x = r * f x
The theorem `AddMonoidAlgebra.single_zero_mul_apply` states that for any semiring `k`, any `AddZeroClass` `G` (i.e., a type endowed with an addition operation and a zero element), any `AddMonoidAlgebra` `f` over `k` and `G`, and any element `r` of `k` and `x` of `G`, the convolution product of the `AddMonoidAlgebra` generated by the zero element of `G` and the element `r` of `k`, with `f`, evaluated at `x`, is equal to `r` times the value of `f` at `x`. Essentially, this theorem is capturing the distributive property of multiplication over addition in the context of monoid algebras.
More concisely: For any semiring `k`, AddMonoidAlgebra over `k` and AddZeroClass `G`, element `r` of `k`, and `x` of `G`, the convolution product of the AddMonoidAlgebra generated by the zero element of `G` and `r` with `f` equals `r` times `f(x)`.
|
AddMonoidAlgebra.single_mul_single
theorem AddMonoidAlgebra.single_mul_single :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] {a₁ a₂ : G} {b₁ b₂ : k},
AddMonoidAlgebra.single a₁ b₁ * AddMonoidAlgebra.single a₂ b₂ = AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)
The theorem `AddMonoidAlgebra.single_mul_single` states that for any types `k` and `G`, where `k` is a semiring and `G` is an additive monoid, and for any elements `a₁, a₂` in `G` and `b₁, b₂` in `k`, the product of two `AddMonoidAlgebra.single` functions, `AddMonoidAlgebra.single a₁ b₁` and `AddMonoidAlgebra.single a₂ b₂`, is equal to `AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)`. In other words, it asserts a distributive property of the `single` function in the context of the `AddMonoidAlgebra`: the multiplication of `single` functions distributes over the addition in the underlying `G` monoid and the multiplication in the semiring `k`.
More concisely: For any semiring `k` and additive monoid `G`, the product of two `AddMonoidAlgebra.single` functions, `AddMonoidAlgebra.single a₁ b₁` and `AddMonoidAlgebra.single a₂ b₂`, equals `AddMonoidAlgebra.single (a₁ + a₂) (b₁ * b₂)`.
|
MonoidAlgebra.liftNC_single
theorem MonoidAlgebra.liftNC_single :
∀ {k : Type u₁} {G : Type u₂} {R : Type u_2} [inst : Semiring k] [inst_1 : NonUnitalNonAssocSemiring R] (f : k →+ R)
(g : G → R) (a : G) (b : k), (MonoidAlgebra.liftNC f g) (MonoidAlgebra.single a b) = f b * g a
The theorem `MonoidAlgebra.liftNC_single` states that for any semiring `k`, any type `G`, and any non-unital, non-associative semiring `R`, given a semiring homomorphism `f` from `k` to `R`, a function `g` from `G` to `R`, an element `a` of `G` and an element `b` of `k`, applying the `liftNC` function of the monoid algebra on the `single` function of the monoid algebra for `a` and `b` equals the multiplication of the result of applying `f` on `b` and applying `g` on `a`. In mathematical terms, this can be written as $(\text{liftNC } f \; g)(\text{single } a \; b) = f(b) \cdot g(a)$.
More concisely: For any semiring homomorphism $f$ from $k$ to a non-unital, non-associative semiring $R$, any function $g$ from a type $G$ to $R$, and any elements $a$ in $G$ and $b$ in $k$, we have $(\text{liftNC } f \; g)(\text{single } a \; b) = f(b) \cdot g(a)$.
|
MonoidAlgebra.mul_apply
theorem MonoidAlgebra.mul_apply :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : DecidableEq G] [inst_2 : Mul G]
(f g : MonoidAlgebra k G) (x : G),
(f * g) x = Finsupp.sum f fun a₁ b₁ => Finsupp.sum g fun a₂ b₂ => if a₁ * a₂ = x then b₁ * b₂ else 0
The `MonoidAlgebra.mul_apply` theorem establishes the behavior of the multiplication operation in the monoid algebra over a semiring `k` generated by the monoid `G`. Given two elements `f` and `g` of the monoid algebra, and an element `x` from the monoid `G`, the result of multiplying `f` and `g` and then applying `x` is equal to the double summation over the supports of `f` and `g`, where for each pair `(a₁, b₁)` from `f` and `(a₂, b₂)` from `g`, if the multiplication of `a₁` and `a₂` in the monoid equals `x`, then we take the product of `b₁` and `b₂` in the semiring, otherwise we take zero. This gives a formal description of the convolution product in the monoid algebra. The theorem also assumes that equality in the monoid `G` is decidable, and that `G` has a multiplication operation.
More concisely: Given two elements in the monoid algebra over a semiring with decidable equality and multiplication, the product of the elements followed by application of an element from the monoid equals the double summation over their supports, where the product in the semiring is taken for matching monoid multiplications and zero otherwise.
|
MonoidAlgebra.single_mul_single
theorem MonoidAlgebra.single_mul_single :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Mul G] {a₁ a₂ : G} {b₁ b₂ : k},
MonoidAlgebra.single a₁ b₁ * MonoidAlgebra.single a₂ b₂ = MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)
The theorem `MonoidAlgebra.single_mul_single` states that for any semiring `k` and any set `G` with a multiplication operation, and for any elements `a₁, a₂` from `G` and `b₁, b₂` from `k`, the product of two `MonoidAlgebra.single` elements, first formed by `a₁` and `b₁` and second by `a₂` and `b₂`, is equal to another `MonoidAlgebra.single` element which is formed by the multiplication of `a₁` and `a₂` and the multiplication of `b₁` and `b₂`. In the context of abstract algebra, this is a property of multiplication in the monoid algebra of a semiring over a set with multiplication.
More concisely: For any semiring `k` and set `G` with multiplication, and for all `a₁, a₂ in G` and `b₁, b₂ in k`, the product of `MonoidAlgebra.single a₁ b₁` and `MonoidAlgebra.single a₂ b₂` equals `MonoidAlgebra.single (a₁ * a₂) (b₁ * b₂)`.
|
AddMonoidAlgebra.sum_single_index
theorem AddMonoidAlgebra.sum_single_index :
∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] {N : Type u_3} [inst_1 : AddCommMonoid N] {a : G} {b : k}
{h : G → k → N}, h a 0 = 0 → Finsupp.sum (AddMonoidAlgebra.single a b) h = h a b
The theorem `AddMonoidAlgebra.sum_single_index` states that for any types `k`, `G`, and `N`, where `k` is a semiring and `N` is an additive commutative monoid, and for any elements `a` of type `G`, `b` of type `k`, and a function `h` from `G` and `k` to `N` such that `h a 0` equals to zero, the sum of `h a (f a)` over the support of `f` where `f` is the AddMonoidAlgebra.single of `a` and `b`, is equal to `h a b`. In other words, the sum over the function `h` applied to the single element created by the AddMonoidAlgebra is equal to the function `h` applied directly to the elements `a` and `b`.
More concisely: For any semiring `k`, additive commutative monoid `N`, type `G`, element `a` of `G`, element `b` of `k`, and function `h` from `G` x `k` to `N` such that `h a 0 = 0`, the sum of `h (a, b)` over the support of `AddMonoidAlgebra.single a b` equals `h (a, b)`.
|