Properties of the module Π₀ i, M i #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 aas a linear map; -
dfinsupp.lmk s : (Π i : (↑s : set ι), M i) →ₗ[R] Π₀ i, M i:dfinsupp.single aas a linear map; -
dfinsupp.lapply i : (Π₀ i, M i) →ₗ[R] M: the mapλ f, f ias a linear map; -
dfinsupp.lsum:dfinsupp.sumordfinsupp.lift_add_homas 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 := _}
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 linear_map.coprod for the binary product version.
Equations
- dfinsupp.coprod_map f = (⇑(finsupp.lsum ℕ) (λ (i : ι), linear_map.id)).comp ((finsupp_lequiv_dfinsupp R).symm.to_linear_map.comp (dfinsupp.map_range.linear_map f))
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 dfinsupps.
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'.