English
There is a pointwise scalar action of functions on finsupps: the module structure of α → β on Finsupp α β is defined by g • f = mapDomain (g • ·) f.
Русский
Существует точечное действие скаляров на FinSupp: структуру модуля для Finsupp α β над α → β задают как g • f = mapDomain (g • ·) f.
LaTeX
$$$ [\\text{Module } (α \\to β) (α \\to_0 β)]$ with $ (g \\cdot f)(a) = f(a)$, i.e., the action is by domain precomposition: $(g \\cdot f)(a) = g(a) \\cdot f(a)$$$
Lean4
instance pointwiseScalar [Semiring β] : SMul (α → β) (α →₀ β) where
smul f
g :=
Finsupp.ofSupportFinite (fun a ↦ f a • g a)
(by
apply Set.Finite.subset g.finite_support
simp only [Function.support_subset_iff, Finsupp.mem_support_iff, Ne, Finsupp.fun_support_eq, Finset.mem_coe]
intro x hx h
apply hx
rw [h, smul_zero])
