Properties of the module α →₀ M
#
Given an R
-module M
, the R
-module structure on α →₀ M
is defined in
Data.Finsupp.Basic
.
In this file we define LinearMap
versions of various maps:
Finsupp.lsingle a : M →ₗ[R] ι →₀ M
:Finsupp.single a
as a linear map;Finsupp.lapply a : (ι →₀ M) →ₗ[R] M
: the mapfun f ↦ f a
as a linear map;Finsupp.lsubtypeDomain (s : Set α) : (α →₀ M) →ₗ[R] (s →₀ M)
: restriction to a subtype as a linear map;Finsupp.restrictDom
:Finsupp.filter
as a linear map toFinsupp.supported s
;Finsupp.lmapDomain
: a linear map version ofFinsupp.mapDomain
;
Tags #
function with finite support, module, linear algebra
Given Finite α
, linearEquivFunOnFinite R
is the natural R
-linear equivalence between
α →₀ β
and α → β
.
Equations
Instances For
Interpret Finsupp.single a
as a linear map.
Equations
Instances For
Two R
-linear maps from Finsupp X M
which agree on each single x y
agree everywhere.
Two R
-linear maps from Finsupp X M
which agree on each single x y
agree everywhere.
We formulate this fact using equality of linear maps φ.comp (lsingle a)
and ψ.comp (lsingle a)
so that the ext
tactic can apply a type-specific extensionality lemma to prove equality of these
maps. E.g., if M = R
, then it suffices to verify φ (single a 1) = ψ (single a 1)
.
Interpret Finsupp.subtypeDomain s
as a linear map.
Equations
Instances For
Interpret Finsupp.mapDomain
as a linear map.
Equations
Instances For
Given f : α → β
and a proof hf
that f
is injective, lcomapDomain f hf
is the linear map
sending l : β →₀ M
to the finitely supported function from α
to M
given by composing
l
with f
.
This is the linear version of Finsupp.comapDomain
.
Equations
Instances For
Finsupp.mapRange
as a LinearMap
.
Equations
Instances For
Finsupp.mapRange
as a LinearEquiv
.
Equations
Instances For
The linear equivalence between α × β →₀ M
and α →₀ β →₀ M
.
This is the LinearEquiv
version of Finsupp.finsuppProdEquiv
.
Equations
Instances For
If Subsingleton R
, then M ≃ₗ[R] ι →₀ R
for any type ι
.