English
Restriction of Finsupp to a subtype: there is a natural linear map from α →₀ M to s →₀ M given by restricting the support to s and projecting onto the subtype. This linear map preserves addition and scalar multiplication.
Русский
Ограничение Finsupp до подтипа: существует естественное линейное отображение из α →₀ M в s →₀ M, задаваемое ограничением подопорости на s и проекцией на подтип.
LaTeX
$$$\\text{lsubtypeDomain} : (α \\to_0 M) \\to_\\ell[R] (s \\to_0 M)$ with $\\text{toFun} := \\text{subtypeDomain}(\\lambda x. x\\in s)$$$
Lean4
/-- Interpret `Finsupp.subtypeDomain s` as a linear map. -/
def lsubtypeDomain : (α →₀ M) →ₗ[R] s →₀ M
where
toFun := subtypeDomain fun x => x ∈ s
map_add' _ _ := subtypeDomain_add
map_smul' _ _ := ext fun _ => rfl
