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

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

source
@[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).

source
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
source
@[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) :
⇑(dfinsupp.lmk s) x = dfinsupp.mk s x
source
@[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) :
⇑(dfinsupp.lsingle i) x = dfinsupp.single i x
source
@[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) :
⇑(dfinsupp.lapply i) f = ⇑f i
source
@[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
source
@[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
source
@[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 : ι) :
⇑((dfinsupp.lsum S).symm) F i = F.comp (dfinsupp.lsingle i)
source
@[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)) ᾰ
source
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
source
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) :
⇑(⇑(dfinsupp.lsum S) F) (dfinsupp.single i x) = ⇑(F i) x

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.

source
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) :
dfinsupp.map_range f hf (r • g) = r • dfinsupp.map_range f hf g
source
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
source
@[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) (ᾰ : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
⇑(dfinsupp.map_range.linear_map f) ᾰ = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(f i) x) _ ᾰ
source
@[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)] :
dfinsupp.map_range.linear_map (λ (i : ι), linear_map.id) = linear_map.id
source
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) :
dfinsupp.map_range.linear_map (λ (i : ι), (f i).comp (f₂ i)) = (dfinsupp.map_range.linear_map f).comp (dfinsupp.map_range.linear_map f₂)
source
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} :
⇑(⇑(dfinsupp.lsum ℕ) h) (⇑(dfinsupp.map_range.linear_map f) l) = ⇑(⇑(dfinsupp.lsum ℕ) (λ (i : ι), (h i).comp (f i))) l
source
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
source
@[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) (ᾰ : Π₀ (i : ι), (λ (i : ι), β₁ i) i) :
⇑(dfinsupp.map_range.linear_equiv e) ᾰ = dfinsupp.map_range (λ (i : ι) (x : β₁ i), ⇑(e i) x) _ ᾰ
source
@[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)
source
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) :
dfinsupp.map_range.linear_equiv (λ (i : ι), (f i).trans (f₂ i)) = (dfinsupp.map_range.linear_equiv f).trans (dfinsupp.map_range.linear_equiv f₂)
source
@[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) :
(dfinsupp.map_range.linear_equiv e).symm = dfinsupp.map_range.linear_equiv (λ (i : ι), (e i).symm)
source
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
source
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 ≠ 0 → g c (⇑f c) ∈ S) :
f.sum g ∈ S
source
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) :
⇑(dfinsupp.sum_add_hom g) f ∈ S
source
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 = (⇑(dfinsupp.lsum ℕ) (λ (i : ι), (p i).subtype)).range

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.

source
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) = ((⇑(dfinsupp.lsum ℕ) (λ (i : ι), (S i).subtype)).comp (dfinsupp.filter_linear_map R (λ (i : ι), ↥(S i)) p)).range

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.

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

source
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
source
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) = ↑x → x = 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.

source
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))) :
complete_lattice.independent p
source
theorem complete_lattice.independent_of_dfinsupp_sum_add_hom_injective {ι : Type u_1} {N : Type u_5} [dec_ι : decidable_eq ι] [add_comm_monoid N] (p : ι → add_submonoid N) (h : function.injective ⇑(dfinsupp.sum_add_hom (λ (i : ι), (p i).subtype))) :
complete_lattice.independent p
source
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) :
(⇑(dfinsupp.lsum ℕ) (λ (i : ι), (p i).subtype)).comp ((dfinsupp.map_range.linear_map (λ (i : ι), linear_map.to_span_singleton R ↥(p i) ⟨v i, _⟩)).comp (finsupp_lequiv_dfinsupp R).to_linear_map) = finsupp.total ι N R v

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

source
theorem complete_lattice.independent_of_dfinsupp_sum_add_hom_injective' {ι : Type u_1} {N : Type u_5} [dec_ι : decidable_eq ι] [add_comm_group N] (p : ι → add_subgroup N) (h : function.injective ⇑(dfinsupp.sum_add_hom (λ (i : ι), (p i).subtype))) :
complete_lattice.independent p
source
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) :
function.injective ⇑(⇑(dfinsupp.lsum ℕ) (λ (i : ι), (p i).subtype))

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.

source
theorem complete_lattice.independent.dfinsupp_sum_add_hom_injective {ι : Type u_1} {N : Type u_5} [dec_ι : decidable_eq ι] [add_comm_group N] {p : ι → add_subgroup N} (h : complete_lattice.independent p) :
function.injective ⇑(dfinsupp.sum_add_hom (λ (i : ι), (p i).subtype))

The canonical map out of a direct sum of a family of additive subgroups is injective when the additive subgroups are complete_lattice.independent.

source
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) :
complete_lattice.independent p ↔ function.injective ⇑(⇑(dfinsupp.lsum ℕ) (λ (i : ι), (p i).subtype))

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.

source
theorem complete_lattice.independent_iff_dfinsupp_sum_add_hom_injective {ι : Type u_1} {N : Type u_5} [dec_ι : decidable_eq ι] [add_comm_group N] (p : ι → add_subgroup N) :
complete_lattice.independent p ↔ function.injective ⇑(dfinsupp.sum_add_hom (λ (i : ι), (p i).subtype))

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.

source
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) :
linear_independent R v

If a family of submodules is independent, then a choice of nonzero vector from each submodule forms a linearly independent family.