Scalar multiplication by finitely supported functions.

Given sets G and P, with a left-cancellative vector-addition of G on P, we define an antidiagonal function that assigns, for any element a in P, finite subset s of G, and subset t in P, the Set of all pairs of an element in s and an element in t that vector-add to a. When R is a ring and V is an R-module, we obtain a convolution-type action of the ring of finitely supported R-valued functions on G on the space of V-valued functions on P.

Definitions

• Finsupp.vaddAntidiagonal : The finset of pairs that vector-add to a given element.

theorem Finsupp.finite_vaddAntidiagonal {G : Type u_1} {P : Type u_2} {R : Type u_4} {V : Type u_7} [VAdd G P] [IsLeftCancelVAdd G P] [Zero R] [Zero V] (f : G →₀ R) (x : P → V) (p : P) : ((↑f.support).vaddAntidiagonal (Function.support x) p).Finite

noncomputable def Finsupp.vaddAntidiagonal {G : Type u_1} {P : Type u_2} {R : Type u_4} {V : Type u_7} [VAdd G P] [IsLeftCancelVAdd G P] [Zero R] [Zero V] (f : G →₀ R) (x : P → V) (p : P) : Finset (G × P)

The finset of pairs that vector-add to a given element.

Equations

• f.vaddAntidiagonal x p = ⋯.toFinset

theorem Finsupp.mem_vaddAntidiagonal_iff {G : Type u_1} {P : Type u_2} {R : Type u_4} {V : Type u_7} [VAdd G P] [IsLeftCancelVAdd G P] [Zero R] [Zero V] (f : G →₀ R) (x : P → V) (p : P) (gh : G × P) : gh ∈ f.vaddAntidiagonal x p ↔ f gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.1 +ᵥ gh.2 = p

theorem Finsupp.mem_vaddAntidiagonal_of_addGroup {G : Type u_1} {P : Type u_2} {R : Type u_4} {V : Type u_7} [AddGroup G] [AddAction G P] [Zero R] [Zero V] (f : G →₀ R) (x : P → V) (p : P) (gh : G × P) : gh ∈ f.vaddAntidiagonal x p ↔ f gh.1 ≠ 0 ∧ x gh.2 ≠ 0 ∧ gh.2 = -gh.1 +ᵥ p

@[implicit_reducible]

noncomputable def Finsupp.instSMulForallOfIsLeftCancelVAddOfSMulWithZero {G : Type u_1} {P : Type u_2} {R : Type u_4} {V : Type u_7} [VAdd G P] [IsLeftCancelVAdd G P] [Zero R] [AddCommMonoid V] [SMulWithZero R V] : SMul (G →₀ R) (P → V)

A convolution-type scalar multiplication of finitely supported functions on formal functions.

Equations

• Finsupp.instSMulForallOfIsLeftCancelVAddOfSMulWithZero = { smul := fun (f : G →₀ R) (x : P → V) (p : P) => ∑ G_1 ∈ f.vaddAntidiagonal x p, f G_1.1 • x G_1.2 }

theorem Finsupp.smul_eq {G : Type u_1} {P : Type u_2} {R : Type u_4} {V : Type u_7} [VAdd G P] [IsLeftCancelVAdd G P] [Zero R] [AddCommMonoid V] [SMulWithZero R V] (f : G →₀ R) (x : P → V) (p : P) : (f • x) p = ∑ G_1 ∈ f.vaddAntidiagonal x p, f G_1.1 • x G_1.2

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