Declarations about scalar multiplication on Finsupp

Implementation notes

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

@[simp]

theorem Finsupp.single_smul {α : Type u_1} {M : Type u_3} {R : Type u_6} [Zero M] [MonoidWithZero R] [MulActionWithZero R M] (a b : α) (f : α → M) (r : R) : (single a r) b • f a = (single a (r • f b)) b

def Finsupp.comapSMul {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] : SMul G (α →₀ M)

Scalar multiplication acting on the domain.

This is not an instance as it would conflict with the action on the range. See the instance_diamonds test for examples of such conflicts.

Equations

• Finsupp.comapSMul = { smul := fun (g : G) => Finsupp.mapDomain fun (x : α) => g • x }

theorem Finsupp.comapSMul_def {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] (g : G) (f : α →₀ M) : g • f = mapDomain (fun (x : α) => g • x) f

@[simp]

theorem Finsupp.comapSMul_single {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] (g : G) (a : α) (b : M) : g • single a b = single (g • a) b

def Finsupp.comapMulAction {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] : MulAction G (α →₀ M)

Finsupp.comapSMul is multiplicative

Equations

• Finsupp.comapMulAction = { toSMul := Finsupp.comapSMul, one_smul := ⋯, mul_smul := ⋯ }

def Finsupp.comapDistribMulAction {α : Type u_1} {M : Type u_3} {G : Type u_5} [Monoid G] [MulAction G α] [AddCommMonoid M] : DistribMulAction G (α →₀ M)

Finsupp.comapSMul is distributive

Equations

• Finsupp.comapDistribMulAction = { toMulAction := Finsupp.comapMulAction, smul_zero := ⋯, smul_add := ⋯ }

@[simp]

theorem Finsupp.comapSMul_apply {α : Type u_1} {M : Type u_3} {G : Type u_5} [Group G] [MulAction G α] [AddCommMonoid M] (g : G) (f : α →₀ M) (a : α) : (g • f) a = f (g⁻¹ • a)

When G is a group, Finsupp.comapSMul acts by precomposition with the action of g⁻¹.

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

theorem IsSMulRegular.finsupp {α : Type u_1} {M : Type u_3} {R : Type u_6} [Zero M] [SMulZeroClass R M] {k : R} (hk : IsSMulRegular M k) : IsSMulRegular (α →₀ M) k

instance Finsupp.faithfulSMul {α : Type u_1} {M : Type u_3} {R : Type u_6} [Nonempty α] [Zero M] [SMulZeroClass R M] [FaithfulSMul R M] : FaithfulSMul R (α →₀ M)

instance Finsupp.distribMulAction (α : Type u_1) (M : Type u_3) {R : Type u_6} [Monoid R] [AddMonoid M] [DistribMulAction R M] : DistribMulAction R (α →₀ M)

Equations

• Finsupp.distribMulAction α M = { toSMul := (Finsupp.distribSMul α M).toSMul, one_smul := ⋯, mul_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance Finsupp.module (α : Type u_1) (M : Type u_3) {R : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] : Module R (α →₀ M)

Equations

• Finsupp.module α M = { toDistribMulAction := Finsupp.distribMulAction α M, add_smul := ⋯, zero_smul := ⋯ }

@[simp]

theorem Finsupp.support_smul_eq {α : Type u_1} {M : Type u_3} {R : Type u_6} [Zero R] [Zero M] [SMulWithZero R M] [NoZeroSMulDivisors R M] {b : R} (hb : b ≠ 0) {g : α →₀ M} : (b • g).support = g.support

@[simp]

theorem Finsupp.filter_smul {α : Type u_1} {M : Type u_3} {R : Type u_6} {p : α → Prop} [DecidablePred p] [Zero M] [SMulZeroClass R M] {b : R} {v : α →₀ M} : filter p (b • v) = b • filter p v

theorem Finsupp.mapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [AddCommMonoid M] [DistribSMul R M] {f : α → β} (b : R) (v : α →₀ M) : mapDomain f (b • v) = b • mapDomain f v

theorem Finsupp.smul_single' {α : Type u_1} {R : Type u_6} {x✝ : Semiring R} (c : R) (a : α) (b : R) : c • single a b = single a (c * b)

theorem Finsupp.smul_single_one {α : Type u_1} {R : Type u_6} [MulZeroOneClass R] (a : α) (b : R) : b • single a 1 = single a b

theorem Finsupp.comapDomain_smul {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [Zero M] [SMulZeroClass R M] {f : α → β} (r : R) (v : β →₀ M) (hfv : Set.InjOn f (f ⁻¹' ↑v.support)) (hfrv : Set.InjOn f (f ⁻¹' ↑(r • v).support) := ⋯) : comapDomain f (r • v) hfrv = r • comapDomain f v hfv

theorem Finsupp.comapDomain_smul_of_injective {α : Type u_1} {β : Type u_2} {M : Type u_3} {R : Type u_6} [Zero M] [SMulZeroClass R M] {f : α → β} (hf : Function.Injective f) (r : R) (v : β →₀ M) : comapDomain f (r • v) ⋯ = r • comapDomain f v ⋯

A version of Finsupp.comapDomain_smul that's easier to use.

theorem Finsupp.sum_smul_index {α : Type u_1} {M : Type u_3} {R : Type u_6} [MulZeroClass R] [AddCommMonoid M] {g : α →₀ R} {b : R} {h : α → R → M} (h0 : ∀ (i : α), h i 0 = 0) : (b • g).sum h = g.sum fun (i : α) (a : R) => h i (b * a)

theorem Finsupp.sum_smul_index' {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [Zero M] [SMulZeroClass R M] [AddCommMonoid N] {g : α →₀ M} {b : R} {h : α → M → N} (h0 : ∀ (i : α), h i 0 = 0) : (b • g).sum h = g.sum fun (i : α) (c : M) => h i (b • c)

theorem Finsupp.sum_smul_index_addMonoidHom {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [AddZeroClass M] [AddCommMonoid N] [SMulZeroClass R M] {g : α →₀ M} {b : R} {h : α → M →+ N} : ((b • g).sum fun (a : α) => ⇑(h a)) = g.sum fun (i : α) (c : M) => (h i) (b • c)

A version of Finsupp.sum_smul_index' for bundled additive maps.

instance Finsupp.noZeroSMulDivisors {M : Type u_3} {R : Type u_6} [Zero R] [Zero M] [SMulZeroClass R M] {ι : Type u_7} [NoZeroSMulDivisors R M] : NoZeroSMulDivisors R (ι →₀ M)

def Finsupp.DistribMulActionHom.single {α : Type u_1} {M : Type u_3} {R : Type u_6} [Monoid R] [AddMonoid M] [DistribMulAction R M] (a : α) : M →+[R] α →₀ M

Finsupp.single as a DistribMulActionSemiHom.

See also Finsupp.lsingle for the version as a linear map.

Equations

• Finsupp.DistribMulActionHom.single a = { toFun := (↑(Finsupp.singleAddHom a)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Finsupp.distribMulActionHom_ext {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] {f g : (α →₀ M) →+[R] N} (h : ∀ (a : α) (m : M), f (single a m) = g (single a m)) : f = g

theorem Finsupp.distribMulActionHom_ext' {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] {f g : (α →₀ M) →+[R] N} (h : ∀ (a : α), f.comp (DistribMulActionHom.single a) = g.comp (DistribMulActionHom.single a)) : f = g

See note [partially-applied ext lemmas].

theorem Finsupp.distribMulActionHom_ext'_iff {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_6} [Monoid R] [AddMonoid M] [AddMonoid N] [DistribMulAction R M] [DistribMulAction R N] {f g : (α →₀ M) →+[R] N} : f = g ↔ ∀ (a : α), f.comp (DistribMulActionHom.single a) = g.comp (DistribMulActionHom.single a)