English
For any finitely supported M-valued function f, applying lsum to a function l returns l evaluated after summing with f.
Русский
Для любой функции с конечной поддержкой, значение lsum применяется к результату суммы с f.
LaTeX
$$$$ \mathrm{lsum}_S f(l) = l.sum (\lambda b. f(b)). $$$$
Lean4
/-- Lift a family of linear maps `M →ₗ[R] N` indexed by `x : α` to a linear map from `α →₀ M` to
`N` using `Finsupp.sum`. This is an upgraded version of `Finsupp.liftAddHom`.
See note [bundled maps over different rings] for why separate `R` and `S` semirings are used.
-/
def lsum : (α → M →ₛₗ[σ] N) ≃ₗ[S] (α →₀ M) →ₛₗ[σ] N
where
toFun
F :=
{ toFun := fun d => d.sum fun i => F i
map_add' := (liftAddHom (α := α) (M := M) (N := N) fun x => (F x).toAddMonoidHom).map_add
map_smul' := fun c f => by simp [sum_smul_index', smul_sum] }
invFun F x := F.comp (lsingle x)
left_inv
F := by
ext x y
simp
right_inv
F := by
ext x y
simp
map_add' F
G := by
ext x y
simp
map_smul' F
G := by
ext x y
simp
