Scalar multiplication on Finsupp

This file defines the pointwise scalar multiplication on Finsupp, assuming it preserves zero.

Main declarations

• Finsupp.smulZeroClass: if the action of R on M preserves 0, then it acts on α →₀ M

Implementation notes

This file is intermediate between Finsupp.Defs and Finsupp.Module in that it covers scalar multiplication but does not rely on the definition of Module. Scalar multiplication is needed to supply the nsmul (and zsmul) fields of (semi)ring structures which are fundamental for e.g. Polynomial, so we want to keep the imports required for the Finsupp.smulZeroClass instance reasonably light.

This file is a noncomputable theory and uses classical logic throughout.

instance Finsupp.smulZeroClass {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] : SMulZeroClass R (α →₀ M)

Equations

• Finsupp.smulZeroClass = { smul := fun (a : R) (v : α →₀ M) => Finsupp.mapRange (fun (x : M) => a • x) ⋯ v, smul_zero := ⋯ }

Throughout this section, some Monoid and Semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

@[simp]

theorem Finsupp.coe_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) : ⇑(b • v) = b • ⇑v

theorem Finsupp.smul_apply {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] (b : R) (v : α →₀ M) (a : α) : (b • v) a = b • v a

instance Finsupp.instSMulWithZero {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero R] [Zero M] [SMulWithZero R M] : SMulWithZero R (α →₀ M)

Equations

• Finsupp.instSMulWithZero = { toSMulZeroClass := Finsupp.smulZeroClass, zero_smul := ⋯ }

instance Finsupp.distribSMul (α : Type u_1) (M : Type u_5) {R : Type u_11} [AddZeroClass M] [DistribSMul R M] : DistribSMul R (α →₀ M)

Equations

• Finsupp.distribSMul α M = { smul := fun (x1 : R) (x2 : α →₀ M) => x1 • x2, smul_zero := ⋯, smul_add := ⋯ }

instance Finsupp.isScalarTower (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMul R S] [IsScalarTower R S M] : IsScalarTower R S (α →₀ M)

instance Finsupp.smulCommClass (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [Zero M] [SMulZeroClass R M] [SMulZeroClass S M] [SMulCommClass R S M] : SMulCommClass R S (α →₀ M)

instance Finsupp.isCentralScalar (α : Type u_1) (M : Type u_5) {R : Type u_11} [Zero M] [SMulZeroClass R M] [SMulZeroClass Rᵐᵒᵖ M] [IsCentralScalar R M] : IsCentralScalar R (α →₀ M)

theorem Finsupp.support_smul {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] {b : R} {g : α →₀ M} : (b • g).support ⊆ g.support

@[simp]

theorem Finsupp.smul_single {α : Type u_1} {M : Type u_5} {R : Type u_11} [Zero M] [SMulZeroClass R M] (c : R) (a : α) (b : M) : c • single a b = single a (c • b)

theorem Finsupp.mapRange_smul' {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} {S : Type u_12} [Zero M] [SMulZeroClass R M] [Zero N] [SMulZeroClass S N] {f : M → N} {hf : f 0 = 0} (c : R) (d : S) (v : α →₀ M) (hsmul : ∀ (x : M), f (c • x) = d • f x) : mapRange f hf (c • v) = d • mapRange f hf v

theorem Finsupp.mapRange_smul {α : Type u_1} {M : Type u_5} {N : Type u_7} {R : Type u_11} [Zero M] [SMulZeroClass R M] [Zero N] [SMulZeroClass R N] {f : M → N} {hf : f 0 = 0} (c : R) (v : α →₀ M) (hsmul : ∀ (x : M), f (c • x) = c • f x) : mapRange f hf (c • v) = c • mapRange f hf v