mathlib documentation

linear_algebra.dfinsupp

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:

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

def dfinsupp.lmk {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] (s : finset ι) :
(Π (i : s), M i) →ₗ[R] Π₀ (i : ι), M i

dfinsupp.mk as a linear_map.

Equations
def dfinsupp.lsingle {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] (i : ι) :
M i →ₗ[R] Π₀ (i : ι), M i

dfinsupp.single as a linear_map

Equations
theorem dfinsupp.lhom_ext {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι) (x : M i), φ (dfinsupp.single i x) = ψ (dfinsupp.single i x)) :
φ = ψ

Two R-linear maps from Π₀ i, M i which agree on each single i x agree everywhere.

@[ext]
theorem dfinsupp.lhom_ext' {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι), φ.comp (dfinsupp.lsingle i) = ψ.comp (dfinsupp.lsingle i)) :
φ = ψ

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).

def dfinsupp.lapply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] (i : ι) :
(Π₀ (i : ι), M i) →ₗ[R] M i

Interpret λ (f : Π₀ i, M i), f i as a linear map.

Equations
@[simp]
theorem dfinsupp.lmk_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] (s : finset ι) (x : Π (i : s), (λ (i : ι), M i) i) :
@[simp]
theorem dfinsupp.lsingle_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] (i : ι) (x : M i) :
@[simp]
theorem dfinsupp.lapply_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] (i : ι) (f : Π₀ (i : ι), M i) :
@[protected, instance]
def dfinsupp.add_comm_monoid_of_linear_map {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] :
add_comm_monoid (Π₀ (i : ι), M i →ₗ[R] N)

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.

Equations
@[protected, instance]
def dfinsupp.module_of_linear_map {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : ι → Type u_4} {N : Type u_5} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] :
module S (Π₀ (i : ι), M i →ₗ[R] N)

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
@[simp]
theorem dfinsupp.lsum_symm_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) :
@[simp]
theorem dfinsupp.lsum_apply_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] (F : Π (i : ι), M i →ₗ[R] N) (ᾰ : Π₀ (i : ι), (λ (i : ι), M i) i) :
((dfinsupp.lsum S) F) = (dfinsupp.sum_add_hom (λ (i : ι), (F i).to_add_monoid_hom))
def dfinsupp.lsum {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] :
(Π (i : ι), M i →ₗ[R] N) ≃ₗ[S] (Π₀ (i : ι), M i) →ₗ[R] N

The dfinsupp version of finsupp.lsum.

See note [bundled maps over different rings] for why separate R and S semirings are used.

Equations
theorem dfinsupp.lsum_single {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] [add_comm_monoid N] [module R N] [semiring S] [module S N] [smul_comm_class R S N] (F : Π (i : ι), M i →ₗ[R] N) (i : ι) (x : M i) :

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.

theorem dfinsupp.map_range_smul {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ iβ₂ i) (hf : ∀ (i : ι), f i 0 = 0) (r : R) (hf' : ∀ (i : ι) (x : β₁ i), f i (r x) = r f i x) (g : Π₀ (i : ι), β₁ i) :
def dfinsupp.map_range.linear_map {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ i →ₗ[R] β₂ i) :
(Π₀ (i : ι), β₁ i) →ₗ[R] Π₀ (i : ι), β₂ i

dfinsupp.map_range as an linear_map.

Equations
@[simp]
theorem dfinsupp.map_range.linear_map_apply {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ i →ₗ[R] β₂ i) (x : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
(dfinsupp.map_range.linear_map f) x = dfinsupp.map_range (λ (i : ι) (x : β₁ i), (f i) x) _ x
@[simp]
theorem dfinsupp.map_range.linear_map_id {ι : Type u_1} {R : Type u_2} [semiring R] {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₂ i)] :
theorem dfinsupp.map_range.linear_map_comp {ι : Type u_1} {R : Type u_2} [semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β₁ i →ₗ[R] β₂ i) (f₂ : Π (i : ι), β i →ₗ[R] β₁ i) :
theorem dfinsupp.sum_map_range_index.linear_map {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] [Π (i : ι) (x : β₁ i), decidable (x 0)] [Π (i : ι) (x : β₂ i), decidable (x 0)] {f : Π (i : ι), β₁ i →ₗ[R] β₂ i} {h : Π (i : ι), β₂ i →ₗ[R] N} {l : Π₀ (i : ι), β₁ i} :
def dfinsupp.map_range.linear_equiv {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (e : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) :
(Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₂ i

dfinsupp.map_range.linear_map as an linear_equiv.

Equations
@[simp]
theorem dfinsupp.map_range.linear_equiv_apply {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (e : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) (x : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
(dfinsupp.map_range.linear_equiv e) x = dfinsupp.map_range (λ (i : ι) (x : β₁ i), (e i) x) _ x
@[simp]
theorem dfinsupp.map_range.linear_equiv_refl {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), module R (β₁ i)] :
dfinsupp.map_range.linear_equiv (λ (i : ι), linear_equiv.refl R (β₁ i)) = linear_equiv.refl R (Π₀ (i : ι), β₁ i)
theorem dfinsupp.map_range.linear_equiv_trans {ι : Type u_1} {R : Type u_2} [semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β i)] [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (f : Π (i : ι), β i ≃ₗ[R] β₁ i) (f₂ : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) :
@[simp]
theorem dfinsupp.map_range.linear_equiv_symm {ι : Type u_1} {R : Type u_2} [semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [Π (i : ι), add_comm_monoid (β₁ i)] [Π (i : ι), add_comm_monoid (β₂ i)] [Π (i : ι), module R (β₁ i)] [Π (i : ι), module R (β₂ i)] (e : Π (i : ι), β₁ i ≃ₗ[R] β₂ i) :
noncomputable def dfinsupp.basis {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [semiring R] [Π (i : ι), add_comm_monoid (M i)] [Π (i : ι), module R (M i)] {η : ι → Type u_3} (b : Π (i : ι), basis (η i) R (M i)) :
basis (Σ (i : ι), η i) R (Π₀ (i : ι), M i)

The direct sum of free modules is free.

Note that while this is stated for dfinsupp not direct_sum, the types are defeq.

Equations
theorem submodule.dfinsupp_sum_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] {β : ι → Type u_3} [Π (i : ι), has_zero (β i)] [Π (i : ι) (x : β i), decidable (x 0)] (S : submodule R N) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i → N) (h : ∀ (c : ι), f c 0g c (f c) S) :
f.sum g S
theorem submodule.dfinsupp_sum_add_hom_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] {β : ι → Type u_3} [Π (i : ι), add_zero_class (β i)] (S : submodule R N) (f : Π₀ (i : ι), β i) (g : Π (i : ι), β i →+ N) (h : ∀ (c : ι), f c 0(g c) (f c) S) :
theorem submodule.supr_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) :
supr p = linear_map.range ((dfinsupp.lsum ) (λ (i : ι), (p i).subtype))

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.

theorem submodule.bsupr_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → Prop) [decidable_pred p] (S : ι → submodule R N) :
(⨆ (i : ι) (h : p i), S i) = linear_map.range (((dfinsupp.lsum ) (λ (i : ι), (S i).subtype)).comp (dfinsupp.filter_linear_map R (λ (i : ι), (S i)) p))

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.

theorem submodule.mem_supr_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) (x : N) :
x supr p ∃ (f : Π₀ (i : ι), (p i)), ((dfinsupp.lsum ) (λ (i : ι), (p i).subtype)) f = x
theorem submodule.mem_supr_iff_exists_dfinsupp' {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) [Π (i : ι) (x : (p i)), decidable (x 0)] (x : N) :
x supr p ∃ (f : Π₀ (i : ι), (p i)), f.sum (λ (i : ι) (xi : (p i)), xi) = x

A variant of submodule.mem_supr_iff_exists_dfinsupp with the RHS fully unfolded.

theorem submodule.mem_bsupr_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → Prop) [decidable_pred p] (S : ι → submodule R N) (x : N) :
(x ⨆ (i : ι) (h : p i), S i) ∃ (f : Π₀ (i : ι), (S i)), ((dfinsupp.lsum ) (λ (i : ι), (S i).subtype)) (dfinsupp.filter p f) = x
theorem submodule.mem_supr_finset_iff_exists_sum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [semiring R] [add_comm_monoid N] [module R N] {s : finset ι} (p : ι → submodule R N) (a : N) :
(a ⨆ (i : ι) (H : i s), p i) ∃ (μ : Π (i : ι), (p i)), s.sum (λ (i : ι), (μ i)) = a
theorem complete_lattice.independent_iff_forall_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) :
complete_lattice.independent p ∀ (i : ι) (x : (p i)) (v : Π₀ (i : ι), (p i)), ((dfinsupp.lsum ) (λ (i : ι), (p i).subtype)) (dfinsupp.erase i v) = xx = 0

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.

theorem complete_lattice.independent_of_dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] (p : ι → submodule R N) (h : function.injective ((dfinsupp.lsum ) (λ (i : ι), (p i).subtype))) :
theorem complete_lattice.lsum_comp_map_range_to_span_singleton {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [semiring R] [add_comm_monoid N] [module R N] [Π (m : R), decidable (m 0)] (p : ι → submodule R N) {v : ι → N} (hv : ∀ (i : ι), v i p i) :

Combining dfinsupp.lsum with linear_map.to_span_singleton is the same as finsupp.total

theorem complete_lattice.independent.dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [ring R] [add_comm_group N] [module R N] {p : ι → submodule R N} (h : complete_lattice.independent p) :

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.

theorem complete_lattice.independent_iff_dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : decidable_eq ι] [ring R] [add_comm_group N] [module R N] (p : ι → submodule R N) :

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.

theorem complete_lattice.independent.linear_independent {ι : Type u_1} {R : Type u_2} {N : Type u_5} [ring R] [add_comm_group N] [module R N] [no_zero_smul_divisors R N] (p : ι → submodule R N) (hp : complete_lattice.independent p) {v : ι → N} (hv : ∀ (i : ι), v i p i) (hv' : ∀ (i : ι), v i 0) :

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'.

theorem complete_lattice.independent_iff_linear_independent_of_ne_zero {ι : Type u_1} {R : Type u_2} {N : Type u_5} [ring R] [add_comm_group N] [module R N] [no_zero_smul_divisors R N] {v : ι → N} (h_ne_zero : ∀ (i : ι), v i 0) :