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 Mathlib.Data.DFinsupp.Module.
In this file we define LinearMap versions of various maps:
DFinsupp.lsingle a : M →ₗ[R] Π₀ i, M i:DFinsupp.single aas a linear map;DFinsupp.lmk s : (Π i : (↑s : Set ι), M i) →ₗ[R] Π₀ i, M i:DFinsupp.mkas a linear map;DFinsupp.lapply i : (Π₀ i, M i) →ₗ[R] M: the mapfun f ↦ f ias a linear map;DFinsupp.lsum:DFinsupp.sumorDFinsupp.liftAddHomas 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 applying 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.
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
Equations
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 DFinsupps.
This is an intermediate result used to prove
iSupIndep_of_dfinsupp_lsum_injective and
iSupIndep.dfinsupp_lsum_injective.
Alias of iSupIndep_iff_forall_dfinsupp.
Independence of a family of submodules can be expressed as a quantifier over DFinsupps.
This is an intermediate result used to prove
iSupIndep_of_dfinsupp_lsum_injective and
iSupIndep.dfinsupp_lsum_injective.
Alias of iSupIndep_of_dfinsupp_lsum_injective.
Combining DFinsupp.lsum with LinearMap.toSpanSingleton is the same as
Finsupp.linearCombination
If DFinsupp.sumAddHom applied with AddSubmonoid.subtype is injective then the additive
subgroups are independent.
Alias of iSupIndep_of_dfinsupp_sumAddHom_injective'.
If DFinsupp.sumAddHom applied with AddSubmonoid.subtype is injective then the additive
subgroups are independent.
The canonical map out of a direct sum of a family of submodules is injective when the submodules
are iSupIndep.
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.
Alias of iSupIndep.dfinsupp_lsum_injective.
The canonical map out of a direct sum of a family of submodules is injective when the submodules
are iSupIndep.
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 iSupIndep.
Alias of iSupIndep.dfinsupp_sumAddHom_injective.
The canonical map out of a direct sum of a family of additive subgroups is injective when the
additive subgroups are iSupIndep.
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
iSupIndep.dfinsupp_lsum_injective for details.
Alias of iSupIndep_iff_dfinsupp_lsum_injective.
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
iSupIndep.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.
Alias of iSupIndep_iff_dfinsupp_sumAddHom_injective.
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 iSupIndep.linearIndependent'.
Alias of iSupIndep.linearIndependent.
If a family of submodules is independent, then a choice of nonzero vector from each submodule forms a linearly independent family.
See also iSupIndep.linearIndependent'.