Properties of the semimodule α →₀ M
Given an R
-semimodule M
, the R
-semimodule structure on α →₀ M
is defined in
data.finsupp.basic
.
In this file we define finsupp.supported s
to be the set {f : α →₀ M | f.support ⊆ s}
interpreted as a submodule of α →₀ M
. We also define linear_map
versions of various maps:
finsupp.lsingle a : M →ₗ[R] ι →₀ M
:finsupp.single a
as a linear map;finsupp.lapply a : (ι →₀ M) →ₗ[R] M
: the mapλ f, f a
as a linear map;finsupp.lsubtype_domain (s : set α) : (α →₀ M) →ₗ[R] (s →₀ M)
: restriction to a subtype as a linear map;finsupp.restrict_dom
:finsupp.filter
as a linear map tofinsupp.supported s
;finsupp.lsum
:finsupp.sum
orfinsupp.lift_add_hom
as alinear_map
;finsupp.total α M R (v : ι → M)
: sendsl : ι → R
to the linear combination ofv i
with coefficientsl i
;finsupp.total_on
: a restricted version offinsupp.total
with domainfinsupp.supported R R s
and codomainsubmodule.span R (v '' s)
;finsupp.supported_equiv_finsupp
: a linear equivalence between the functionsα →₀ M
supported ons
and the functionss →₀ M
;finsupp.lmap_domain
: a linear map version offinsupp.map_domain
;finsupp.dom_lcongr
: alinear_equiv
version offinsupp.dom_congr
;finsupp.congr
: if the setss
andt
are equivalent, thensupported M R s
is equivalent tosupported M R t
;finsupp.lcongr
: alinear_equiv
alence betweenα →₀ M
andβ →₀ N
constructed usinge : α ≃ β
ande' : M ≃ₗ[R] N
.
Tags
function with finite support, semimodule, linear algebra
Interpret finsupp.single a
as a linear map.
Equations
- finsupp.lsingle a = {to_fun := (finsupp.single_add_hom a).to_fun, map_add' := _, map_smul' := _}
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 λ (f : α →₀ M), f a
as a linear map.
Equations
- finsupp.lapply a = {to_fun := (finsupp.apply_add_hom a).to_fun, map_add' := _, map_smul' := _}
Interpret finsupp.subtype_domain s
as a linear map.
Equations
- finsupp.lsubtype_domain s = {to_fun := finsupp.subtype_domain (λ (x : α), x ∈ s), map_add' := _, map_smul' := _}
finsupp.supported M R s
is the R
-submodule of all p : α →₀ M
such that p.support ⊆ s
.
Interpret finsupp.filter s
as a linear map from α →₀ M
to supported M R s
.
Equations
- finsupp.restrict_dom M R s = linear_map.cod_restrict (finsupp.supported M R s) {to_fun := finsupp.filter (λ (_x : α), _x ∈ s), map_add' := _, map_smul' := _} _
Interpret finsupp.restrict_support_equiv
as a linear equivalence between
supported M R s
and s →₀ M
.
Equations
- finsupp.supported_equiv_finsupp s = let F : ↥(finsupp.supported M R s) ≃ (↥s →₀ M) := finsupp.restrict_support_equiv s M in F.to_linear_equiv _
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.lift_add_hom
.
We define this as an additive equivalence. For a commutative R
, this equivalence can be
upgraded further to a linear equivalence.
Interpret finsupp.lmap_domain
as a linear map.
Equations
- finsupp.lmap_domain M R f = {to_fun := finsupp.map_domain f, map_add' := _, map_smul' := _}
Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and evaluates this linear combination.
Equations
- finsupp.total α M R v = ⇑finsupp.lsum (λ (i : α), linear_map.id.smul_right (v i))
finsupp.total_on M v s
interprets p : α →₀ R
as a linear combination of a
subset of the vectors in v
, mapping it to the span of those vectors.
The subset is indicated by a set s : set α
of indices.
Equations
- finsupp.total_on α M R v s = linear_map.cod_restrict (submodule.span R (v '' s)) ((finsupp.total α M R v).comp (finsupp.supported R R s).subtype) _
An equivalence of domains induces a linear equivalence of finitely supported functions.
Equations
An equivalence of sets induces a linear equivalence of finsupp
s supported on those sets.
Equations
- finsupp.congr s t e = (finsupp.supported_equiv_finsupp s).trans ((finsupp.dom_lcongr e).trans (finsupp.supported_equiv_finsupp t).symm)
An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the corresponding finitely supported functions.
Equations
- finsupp.lcongr e₁ e₂ = (finsupp.dom_lcongr e₁).trans {to_fun := finsupp.map_range ⇑e₂ _, map_add' := _, map_smul' := _, inv_fun := finsupp.map_range ⇑(e₂.symm) _, left_inv := _, right_inv := _}