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 LinearMap
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 mapfun f ↦ f i
as a linear map;DFinsupp.lsum
:DFinsupp.sum
orDFinsupp.liftAddHom
as aLinearMap
;
Implementation notes #
This file should try to mirror LinearAlgebra.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 LinearMap
.
Equations
- DFinsupp.lmk s = { toFun := DFinsupp.mk s, map_add' := ⋯, map_smul' := ⋯ }
Instances For
DFinsupp.single
as a LinearMap
Equations
- DFinsupp.lsingle i = { toFun := DFinsupp.single i, map_add' := ⋯, map_smul' := ⋯ }
Instances For
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 fun (f : Π₀ i, M i) ↦ f i
as a linear map.
Equations
- DFinsupp.lapply i = { toFun := fun (f : Π₀ (i : ι), M i) => f i, map_add' := ⋯, map_smul' := ⋯ }
Instances For
Typeclass inference can't find DFinsupp.addCommMonoid
without help for this case.
This instance allows it to be found where it is needed on the LHS of the colon in
DFinsupp.moduleOfLinearMap
.
Equations
- DFinsupp.addCommMonoidOfLinearMap = inferInstance
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, AddCommMonoid (M i →ₗ[R] N)
instance that
we have with the ∀ i, Zero (M i →ₗ[R] N)
instance which appears as a parameter to the
DFinsupp
type.
Equations
- DFinsupp.moduleOfLinearMap = DFinsupp.module
Equations
- DFinsupp.instEquivLikeLinearEquiv σ M M₂ = inferInstance
The DFinsupp
version of Finsupp.lsum
.
See note [bundled maps over different rings] for why separate R
and S
semirings are used.
Equations
- One or more equations did not get rendered due to their size.
Instances For
While simp
can prove this, it is often convenient to avoid unfolding lsum
into sumAddHom
with DFinsupp.lsum_apply_apply
.
Bundled versions of DFinsupp.mapRange
#
The names should match the equivalent bundled Finsupp.mapRange
definitions.
DFinsupp.mapRange
as a LinearMap
.
Equations
- DFinsupp.mapRange.linearMap f = { toFun := DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (f i) x) ⋯, map_add' := ⋯, map_smul' := ⋯ }
Instances For
DFinsupp.mapRange.linearMap
as a LinearEquiv
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a family of linear maps f i : M i →ₗ[R] N
, we can form a linear map
(Π₀ i, M i) →ₗ[R] N
which sends x : Π₀ i, M i
to the sum over i
of f i
applied to x i
.
This is the map coming from the universal property of Π₀ i, M i
as the coproduct of the M i
.
See also LinearMap.coprod
for the binary product version.
Equations
- DFinsupp.coprodMap f = ((DFinsupp.lsum ℕ) fun (x : ι) => LinearMap.id) ∘ₗ DFinsupp.mapRange.linearMap f
Instances For
The supremum of a family of submodules is equal to the range of DFinsupp.lsum
; that is
every element in the iSup
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.sumAddHom
composed with DFinsupp.filter_add_monoid_hom
; that is, every element in the
bounded iSup
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 characterisation of the span of a family of submodules.
See also Submodule.mem_iSup_iff_exists_finsupp
.
A variant of Submodule.mem_iSup_iff_exists_dfinsupp
with the RHS fully unfolded.
See also Submodule.mem_iSup_iff_exists_finsupp
.
Independence of a family of submodules can be expressed as a quantifier over DFinsupp
s.
This is an intermediate result used to prove
CompleteLattice.independent_of_dfinsupp_lsum_injective
and
CompleteLattice.Independent.dfinsupp_lsum_injective
.
Combining DFinsupp.lsum
with LinearMap.toSpanSingleton
is the same as
Finsupp.linearCombination
The canonical map out of a direct sum of a family of submodules is injective when the submodules
are CompleteLattice.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/DirectSumIsInternal.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 CompleteLattice.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
CompleteLattice.Independent.dfinsupp_lsum_injective
for details.
A family of additive subgroups over an additive group are independent if and only if
DFinsupp.sumAddHom
applied with AddSubgroup.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 CompleteLattice.Independent.linearIndependent'
.