Scalar multiplication by (additive) monoid rings on formal functions.

Given sets G and P, with a left-cancellative scalar-multiplication (or vector-addition) of G on P, together with a module V over a semiring R, we define a convolution action of the monoid algebra R[G] on the set of functions P → V.

theorem MonoidAlgebra.mem_smulAntidiagonal_of_group {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [Group G] [MulAction G P] [Semiring R] [Zero V] (f : MonoidAlgebra R G) (x : P → V) (p : P) (gh : G × P) : gh ∈ Finset.SMulAntidiagonal p ⋯ ↔ f gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = gh.1⁻¹ • p

theorem AddMonoidAlgebra.mem_vaddAntidiagonal_of_addGroup {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [AddGroup G] [AddAction G P] [Semiring R] [Zero V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) (gh : G × P) : gh ∈ Finset.VAddAntidiagonal p ⋯ ↔ f gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = -gh.1 +ᵥ p

@[implicit_reducible]

noncomputable def MonoidAlgebra.instSMulForallOfIsLeftCancelSMulOfSMulWithZero {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [SMul G P] [IsLeftCancelSMul G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] : SMul (MonoidAlgebra R G) (P → V)

A convolution-type scalar multiplication of the monoid algebra on the set of formal functions.

Equations

• MonoidAlgebra.instSMulForallOfIsLeftCancelSMulOfSMulWithZero = { smul := fun (f : MonoidAlgebra R G) (x : P → V) (p : P) => ∑ gh ∈ Finset.SMulAntidiagonal p ⋯, f gh.1 • x gh.2 }

@[implicit_reducible]

noncomputable def AddMonoidAlgebra.instVAddForallOfIsLeftCancelVAddOfVAddWithZero {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [VAdd G P] [IsLeftCancelVAdd G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] : SMul (AddMonoidAlgebra R G) (P → V)

A convolution-type scalar multiplication of the additive monoid algebra on the set of formal functions.

Equations

• AddMonoidAlgebra.instVAddForallOfIsLeftCancelVAddOfVAddWithZero = { smul := fun (f : AddMonoidAlgebra R G) (x : P → V) (p : P) => ∑ gh ∈ Finset.VAddAntidiagonal p ⋯, f gh.1 • x gh.2 }

theorem MonoidAlgebra.smul_eq {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [SMul G P] [IsLeftCancelSMul G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] (f : MonoidAlgebra R G) (x : P → V) (p : P) (hp : ((↑f.support).smulAntidiagonal (Function.support x) p).Finite := ⋯) : (f • x) p = ∑ gh ∈ Finset.SMulAntidiagonal p hp, f gh.1 • x gh.2

theorem AddMonoidAlgebra.smul_eq {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [VAdd G P] [IsLeftCancelVAdd G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) (hp : ((↑f.support).vaddAntidiagonal (Function.support x) p).Finite := ⋯) : (f • x) p = ∑ gh ∈ Finset.VAddAntidiagonal p hp, f gh.1 • x gh.2

theorem MonoidAlgebra.smul_apply_mulAction {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [Group G] [MulAction G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] (f : MonoidAlgebra R G) (x : P → V) (p : P) : (f • x) p = ∑ i ∈ f.support, f i • x (i⁻¹ • p)

theorem AddMonoidAlgebra.smul_apply_addAction {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [AddGroup G] [AddAction G P] [Semiring R] [AddCommMonoid V] [SMulWithZero R V] (f : AddMonoidAlgebra R G) (x : P → V) (p : P) : (f • x) p = ∑ i ∈ f.support, f i • x (-i +ᵥ p)