Properties of the semimodule Π₀ i, M i
Given an indexed collection of R
-semimodules M i
, the R
-semimodule structure on Π₀ i, M i
is defined in data.dfinsupp
.
In this file we define linear_map
versions of various maps:
dfinsupp.lsingle a : M →ₗ[R] Π₀ i, M i
:dfinsupp.single a
as a linear map;dfinsupp.lmk s : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i
:dfinsupp.single a
as a linear map;dfinsupp.lapply i : (Π₀ i, M i) →ₗ[R] M
: the mapλ f, f i
as a linear map;dfinsupp.lsum
:dfinsupp.sum
ordfinsupp.lift_add_hom
as alinear_map
;
Implementation notes
This file should try to mirror linear_algebra.finsupp
where possible. The API of finsupp
is
much more developed, but many lemmas in that file should be eligible to copy over.
Tags
function with finite support, semimodule, linear algebra
dfinsupp.mk
as a linear_map
.
Equations
- dfinsupp.lmk s = {to_fun := dfinsupp.mk s, map_add' := _, map_smul' := _}
dfinsupp.single
as a linear_map
Equations
- dfinsupp.lsingle i = {to_fun := dfinsupp.single i, map_add' := _, map_smul' := _}
Two R
-linear maps from Π₀ i, M i
which agree on each single i x
agree everywhere.
Two R
-linear maps from Π₀ i, M i
which agree on each single i x
agree everywhere.
See note [partially-applied ext lemmas].
After apply this lemma, if M = R
then it suffices to verify φ (single a 1) = ψ (single a 1)
.
Interpret λ (f : Π₀ i, M i), f i
as a linear map.
The dfinsupp
version of finsupp.lsum
.