English
For a finite index set s ⊆ ι, the map lmk(s) sends a family of elements (x_i) with i ∈ s to the dependent finite-support function over ι whose coordinates are x_i for i ∈ s and 0 otherwise; this is a linear map from the product over i∈s of M_i into the dfinsupp over ι.
Русский
Для конечного множества индексов s ⊆ ι отображение lmk(s) отправляет семейство элементов (x_i) с i ∈ s в зависимое dfinsupp'-похождение на ι, координаты которого равны x_i при i ∈ s и равны 0 иначе; это линейное отображение из произведения по i∈s в dfinsupp по ι.
LaTeX
$$$\\mathrm{lmk}(s) : (\\forall i : (↑s : Set ι), M_i) \\to_ℓ[R] \\Pi_0 i, M_i\\quad\\text{so that}\\quad \\mathrm{lmk}(s)(x) = \\mathrm{mk}\;s\\;x$$$
Lean4
/-- `DFinsupp.mk` as a `LinearMap`. -/
def lmk (s : Finset ι) : (∀ i : (↑s : Set ι), M i) →ₗ[R] Π₀ i, M i
where
toFun := mk s
map_add' _ _ := mk_add
map_smul' c x := mk_smul c x
