Properties of the module Π₀ i, M i
#
Given an indexed collection of R
-modules M i
, the R
-module 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, module, 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.
Typeclass inference can't find dfinsupp.add_comm_monoid
without help for this case.
This instance allows it to be found where it is needed on the LHS of the colon in
dfinsupp.module_of_linear_map
.
Typeclass inference can't find dfinsupp.module
without help for this case.
This is needed to define dfinsupp.lsum
below.
The cause seems to be an inability to unify the Π i, add_comm_monoid (M i →ₗ[R] N)
instance that
we have with the Π i, has_zero (M i →ₗ[R] N)
instance which appears as a parameter to the
dfinsupp
type.
Equations
The dfinsupp
version of finsupp.lsum
.
See note [bundled maps over different rings] for why separate R
and S
semirings are used.
Equations
- dfinsupp.lsum S = {to_fun := λ (F : Π (i : ι), M i →ₗ[R] N), {to_fun := ⇑(dfinsupp.sum_add_hom (λ (i : ι), (F i).to_add_monoid_hom)), map_add' := _, map_smul' := _}, map_add' := _, map_smul' := _, inv_fun := λ (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι), F.comp (dfinsupp.lsingle i), left_inv := _, right_inv := _}
While simp
can prove this, it is often convenient to avoid unfolding lsum
into sum_add_hom
with dfinsupp.lsum_apply_apply
.
Bundled versions of dfinsupp.map_range
#
The names should match the equivalent bundled finsupp.map_range
definitions.
dfinsupp.map_range
as an linear_map
.
Equations
- dfinsupp.map_range.linear_map f = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _, map_add' := _, map_smul' := _}
dfinsupp.map_range.linear_map
as an linear_equiv
.
Equations
- dfinsupp.map_range.linear_equiv e = {to_fun := dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _, map_add' := _, map_smul' := _, inv_fun := dfinsupp.map_range (λ (i : ι) (x : β₂ i), ⇑((e i).symm) x) _, left_inv := _, right_inv := _}
The direct sum of free modules is free.
Note that while this is stated for dfinsupp
not direct_sum
, the types are defeq.
Equations
- dfinsupp.basis b = {repr := (dfinsupp.map_range.linear_equiv (λ (i : ι), (b i).repr)).trans (sigma_finsupp_lequiv_dfinsupp R).symm}
The supremum of a family of submodules is equal to the range of dfinsupp.lsum
; that is
every element in the supr
can be produced from taking a finite number of non-zero elements
of p i
, coercing them to N
, and summing them.
The bounded supremum of a family of commutative additive submonoids is equal to the range of
dfinsupp.sum_add_hom
composed with dfinsupp.filter_add_monoid_hom
; that is, every element in the
bounded supr
can be produced from taking a finite number of non-zero elements from the S i
that
satisfy p i
, coercing them to γ
, and summing them.
A variant of submodule.mem_supr_iff_exists_dfinsupp
with the RHS fully unfolded.
Independence of a family of submodules can be expressed as a quantifier over dfinsupp
s.
This is an intermediate result used to prove
complete_lattice.independent_of_dfinsupp_lsum_injective
and
complete_lattice.independent.dfinsupp_lsum_injective
.
Combining dfinsupp.lsum
with linear_map.to_span_singleton
is the same as finsupp.total
The canonical map out of a direct sum of a family of submodules is injective when the submodules
are complete_lattice.independent
.
Note that this is not generally true for [semiring R]
, for instance when A
is the
ℕ
-submodules of the positive and negative integers.
See counterexamples/direct_sum_is_internal.lean
for a proof of this fact.
The canonical map out of a direct sum of a family of additive subgroups is injective when the
additive subgroups are complete_lattice.independent
.
A family of submodules over an additive group are independent if and only iff dfinsupp.lsum
applied with submodule.subtype
is injective.
Note that this is not generally true for [semiring R]
; see
complete_lattice.independent.dfinsupp_lsum_injective
for details.
A family of additive subgroups over an additive group are independent if and only if
dfinsupp.sum_add_hom
applied with add_subgroup.subtype
is injective.
If a family of submodules is independent
, then a choice of nonzero vector from each submodule
forms a linearly independent family.
See also complete_lattice.independent.linear_independent'
.