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 map fun f ↦ f i as a linear map;

• DFinsupp.lsum: DFinsupp.sum or DFinsupp.liftAddHom as a LinearMap;

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

def DFinsupp.lmk {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) : ((i : ↑↑s) → M ↑i) →ₗ[R] Π₀ (i : ι), M i

DFinsupp.mk as a LinearMap.

def DFinsupp.lsingle {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) : M i →ₗ[R] Π₀ (i : ι), M i

DFinsupp.single as a LinearMap

theorem DFinsupp.lhom_ext {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] ⦃φ : (Π₀ (i : ι), M i) →ₗ[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.

theorem DFinsupp.lhom_ext' {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] ⦃φ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ ⦃ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι), LinearMap.comp φ (DFinsupp.lsingle i) = LinearMap.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 : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) : (Π₀ (i : ι), M i) →ₗ[R] M i

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

@[simp]

theorem DFinsupp.lmk_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) (x : (i : ↑↑s) → M ↑i) : ↑(DFinsupp.lmk s) x = DFinsupp.mk s x

@[simp]

theorem DFinsupp.lsingle_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (x : M i) : ↑(DFinsupp.lsingle i) x = DFinsupp.single i x

@[simp]

theorem DFinsupp.lapply_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (f : Π₀ (i : ι), M i) : ↑(DFinsupp.lapply i) f = ↑f i

instance DFinsupp.addCommMonoidOfLinearMap {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] : AddCommMonoid (Π₀ (i : ι), M i →ₗ[R] N)

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.

instance DFinsupp.moduleOfLinearMap {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass 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, 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.

instance DFinsupp.instEquivLikeLinearEquiv {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_8) (M₂ : Type u_9) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] : EquivLike (M ≃ₛₗ[σ] M₂) M M₂

@[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_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) : ↑(LinearEquiv.symm (DFinsupp.lsum S)) F i = LinearMap.comp F (DFinsupp.lsingle 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_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (a : Π₀ (i : ι), M i) : ↑(↑(DFinsupp.lsum S) F) a = ↑(DFinsupp.sumAddHom fun i => LinearMap.toAddMonoidHom (F i)) a

def DFinsupp.lsum {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass 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.

theorem DFinsupp.lsum_single {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass 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 sumAddHom with DFinsupp.lsum_apply_apply.

Bundled versions of DFinsupp.mapRange

The names should match the equivalent bundled Finsupp.mapRange definitions.

theorem DFinsupp.mapRange_smul {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ 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.mapRange f hf (r • g) = r • DFinsupp.mapRange f hf g

@[simp]

theorem DFinsupp.mapRange.linearMap_apply {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) : ↑(DFinsupp.mapRange.linearMap f) x = DFinsupp.mapRange (fun i x => ↑(f i) x) (_ : ∀ (i : ι), ↑(f i) 0 = 0) x

def DFinsupp.mapRange.linearMap {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) : (Π₀ (i : ι), β₁ i) →ₗ[R] Π₀ (i : ι), β₂ i

DFinsupp.mapRange as a LinearMap.

@[simp]

theorem DFinsupp.mapRange.linearMap_id {ι : Type u_1} {R : Type u_2} [dec_ι : DecidableEq ι] [Semiring R] {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₂ i)] : (DFinsupp.mapRange.linearMap fun i => LinearMap.id) = LinearMap.id

theorem DFinsupp.mapRange.linearMap_comp {ι : Type u_1} {R : Type u_2} [Semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (f₂ : (i : ι) → β i →ₗ[R] β₁ i) : (DFinsupp.mapRange.linearMap fun i => LinearMap.comp (f i) (f₂ i)) = LinearMap.comp (DFinsupp.mapRange.linearMap f) (DFinsupp.mapRange.linearMap f₂)

theorem DFinsupp.sum_mapRange_index.linearMap {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ 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.mapRange.linearMap f) l) = ↑(↑(DFinsupp.lsum ℕ) fun i => LinearMap.comp (h i) (f i)) l

@[simp]

theorem DFinsupp.mapRange.linearEquiv_apply {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) : ↑(DFinsupp.mapRange.linearEquiv e) x = DFinsupp.mapRange (fun i x => ↑(e i) x) (_ : ∀ (i : ι), ↑(e i) 0 = 0) x

def DFinsupp.mapRange.linearEquiv {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) : (Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₂ i

DFinsupp.mapRange.linearMap as a LinearEquiv.

@[simp]

theorem DFinsupp.mapRange.linearEquiv_refl {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → Module R (β₁ i)] : (DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl R (Π₀ (i : ι), β₁ i)

theorem DFinsupp.mapRange.linearEquiv_trans {ι : Type u_1} {R : Type u_2} [Semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β i ≃ₗ[R] β₁ i) (f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i) : (DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.trans (f i) (f₂ i)) = LinearEquiv.trans (DFinsupp.mapRange.linearEquiv f) (DFinsupp.mapRange.linearEquiv f₂)

@[simp]

theorem DFinsupp.mapRange.linearEquiv_symm {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) : LinearEquiv.symm (DFinsupp.mapRange.linearEquiv e) = DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.symm (e i)

def DFinsupp.coprodMap {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N) : (Π₀ (i : ι), M i) →ₗ[R] N

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.

theorem DFinsupp.coprodMap_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [(x : N) → Decidable (x ≠ 0)] (f : (i : ι) → M i →ₗ[R] N) (x : Π₀ (i : ι), M i) : ↑(DFinsupp.coprodMap f) x = DFinsupp.sum (DFinsupp.mapRange (fun i => ↑(f i)) (_ : ∀ (x : ι), ↑(f x) 0 = 0) x) fun x => id

theorem DFinsupp.coprodMap_apply_single {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i) : ↑(DFinsupp.coprodMap f) (DFinsupp.single i x) = ↑(f i) x

theorem Submodule.dfinsupp_sum_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {β : ι → Type u_6} [(i : ι) → 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) : DFinsupp.sum f g ∈ S

theorem Submodule.dfinsupp_sumAddHom_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {β : ι → Type u_6} [(i : ι) → AddZeroClass (β i)] (S : Submodule R N) (f : Π₀ (i : ι), β i) (g : (i : ι) → β i →+ N) (h : ∀ (c : ι), ↑f c ≠ 0 → ↑(g c) (↑f c) ∈ S) : ↑(DFinsupp.sumAddHom g) f ∈ S

theorem Submodule.iSup_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) : iSup p = LinearMap.range (↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (p i))

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.

theorem Submodule.biSup_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) : ⨆ (i : ι) (x : p i), S i = LinearMap.range (LinearMap.comp (↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (S i)) (DFinsupp.filterLinearMap R (fun i => { x // x ∈ S i }) p))

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.

theorem Submodule.mem_iSup_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) (x : N) : x ∈ iSup p ↔ ∃ f, ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (p i)) f = x

theorem Submodule.mem_iSup_iff_exists_dfinsupp' {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) [(i : ι) → (x : { x // x ∈ p i }) → Decidable (x ≠ 0)] (x : N) : x ∈ iSup p ↔ ∃ f, (DFinsupp.sum f fun i xi => ↑xi) = x

A variant of Submodule.mem_iSup_iff_exists_dfinsupp with the RHS fully unfolded.

theorem Submodule.mem_biSup_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) (x : N) : x ∈ ⨆ (i : ι) (x : p i), S i ↔ ∃ f, ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (S i)) (DFinsupp.filter p f) = x

theorem Submodule.mem_iSup_finset_iff_exists_sum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] {s : Finset ι} (p : ι → Submodule R N) (a : N) : a ∈ ⨆ (i : ι) (_ : i ∈ s), p i ↔ ∃ μ, (Finset.sum s fun i => ↑(μ i)) = a

theorem CompleteLattice.independent_iff_forall_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) : CompleteLattice.Independent p ↔ ∀ (i : ι) (x : { x // x ∈ p i }) (v : Π₀ (i : ι), { x // x ∈ p i }), ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (p i)) (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 CompleteLattice.independent_of_dfinsupp_lsum_injective and CompleteLattice.Independent.dfinsupp_lsum_injective.

theorem CompleteLattice.independent_of_dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) (h : Function.Injective ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (p i))) : CompleteLattice.Independent p

theorem CompleteLattice.independent_of_dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [dec_ι : DecidableEq ι] [AddCommMonoid N] (p : ι → AddSubmonoid N) (h : Function.Injective ↑(DFinsupp.sumAddHom fun i => AddSubmonoid.subtype (p i))) : CompleteLattice.Independent p

theorem CompleteLattice.lsum_comp_mapRange_toSpanSingleton {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] [(m : R) → Decidable (m ≠ 0)] (p : ι → Submodule R N) {v : ι → N} (hv : ∀ (i : ι), v i ∈ p i) : LinearMap.comp (↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (p i)) (LinearMap.comp (DFinsupp.mapRange.linearMap fun i => LinearMap.toSpanSingleton R { x // x ∈ p i } { val := v i, property := hv i }) ↑(finsuppLequivDFinsupp R)) = Finsupp.total ι N R v

Combining DFinsupp.lsum with LinearMap.toSpanSingleton is the same as Finsupp.total

theorem CompleteLattice.independent_of_dfinsupp_sumAddHom_injective' {ι : Type u_1} {N : Type u_5} [dec_ι : DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) (h : Function.Injective ↑(DFinsupp.sumAddHom fun i => AddSubgroup.subtype (p i))) : CompleteLattice.Independent p

theorem CompleteLattice.Independent.dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] {p : ι → Submodule R N} (h : CompleteLattice.Independent p) : Function.Injective ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (p i))

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.

theorem CompleteLattice.Independent.dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [dec_ι : DecidableEq ι] [AddCommGroup N] {p : ι → AddSubgroup N} (h : CompleteLattice.Independent p) : Function.Injective ↑(DFinsupp.sumAddHom fun i => AddSubgroup.subtype (p i))

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

theorem CompleteLattice.independent_iff_dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [dec_ι : DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] (p : ι → Submodule R N) : CompleteLattice.Independent p ↔ Function.Injective ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (p i))

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.

theorem CompleteLattice.independent_iff_dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [dec_ι : DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) : CompleteLattice.Independent p ↔ Function.Injective ↑(DFinsupp.sumAddHom fun i => AddSubgroup.subtype (p i))

A family of additive subgroups over an additive group are independent if and only if DFinsupp.sumAddHom applied with AddSubgroup.subtype is injective.

theorem CompleteLattice.Independent.linearIndependent {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] (p : ι → Submodule R N) (hp : CompleteLattice.Independent p) {v : ι → N} (hv : ∀ (i : ι), v i ∈ p i) (hv' : ∀ (i : ι), v i ≠ 0) : LinearIndependent R v

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

theorem CompleteLattice.independent_iff_linearIndependent_of_ne_zero {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] {v : ι → N} (h_ne_zero : ∀ (i : ι), v i ≠ 0) : (CompleteLattice.Independent fun i => Submodule.span R {v i}) ↔ LinearIndependent R v