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 a as a linear map;

• DFinsupp.lmk s : (Π i : (↑s : Set ι), M i) →ₗ[R] Π₀ i, M i: DFinsupp.mk 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} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (s : Finset ι) : ((i : ↑↑s) → M ↑i) →ₗ[R] Π₀ (i : ι), M i

DFinsupp.mk as a LinearMap.

Equations

• DFinsupp.lmk s = { toFun := DFinsupp.mk s, map_add' := ⋯, map_smul' := ⋯ }

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

DFinsupp.single as a LinearMap

Equations

• DFinsupp.lsingle i = { toFun := DFinsupp.single i, map_add' := ⋯, map_smul' := ⋯ }

theorem DFinsupp.lhom_ext {ι : 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 ι] ⦃φ ψ : (Π₀ (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} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι), φ ∘ₗ DFinsupp.lsingle i = ψ ∘ₗ 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 applying this lemma, if M = R then it suffices to verify φ (single a 1) = ψ (single a 1).

@[simp]

theorem DFinsupp.lmk_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (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} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) (x : M i) : (DFinsupp.lsingle i) x = DFinsupp.single i x

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.

Equations

• DFinsupp.lapply i = { toFun := fun (f : Π₀ (i : ι), M i) => f i, map_add' := ⋯, map_smul' := ⋯ }

@[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

@[simp]

theorem DFinsupp.lapply_comp_lsingle_same {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) : DFinsupp.lapply i ∘ₗ DFinsupp.lsingle i = LinearMap.id

@[simp]

theorem DFinsupp.lapply_comp_lsingle_of_ne {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i i' : ι) (h : i ≠ i') : DFinsupp.lapply i ∘ₗ DFinsupp.lsingle i' = 0

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.

Equations

• DFinsupp.addCommMonoidOfLinearMap = inferInstance

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.

Equations

• DFinsupp.moduleOfLinearMap = DFinsupp.module

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₂

Equations

• DFinsupp.instEquivLikeLinearEquiv σ M M₂ = inferInstance

def DFinsupp.lsum {ι : 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] [DecidableEq ι] [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.

Equations

• One or more equations did not get rendered due to their size.

@[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} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [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 : ι) => (F i).toAddMonoidHom) a

@[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} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) : (DFinsupp.lsum S).symm F i = F ∘ₗ DFinsupp.lsingle i

theorem DFinsupp.lsum_single {ι : 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] [DecidableEq ι] [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

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.

Equations

• DFinsupp.mapRange.linearMap f = { toFun := DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (f i) x) ⋯, map_add' := ⋯, map_smul' := ⋯ }

@[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 : β₁ i) => (f i) x) ⋯ x

@[simp]

theorem DFinsupp.mapRange.linearMap_id {ι : Type u_1} {R : Type u_2} [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 : ι) => f i ∘ₗ f₂ i) = 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} [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)] [DecidableEq ι] {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 : ι) => h i ∘ₗ f i) l

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.

Equations

• One or more equations did not get rendered due to their size.

@[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 : β₁ i) => (e i) x) ⋯ x

@[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 : ι) => f i ≪≫ₗ f₂ i) = 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) : (DFinsupp.mapRange.linearEquiv e).symm = DFinsupp.mapRange.linearEquiv fun (i : ι) => (e i).symm

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.

Equations

• DFinsupp.coprodMap f = ((DFinsupp.lsum ℕ) fun (x : ι) => LinearMap.id) ∘ₗ DFinsupp.mapRange.linearMap f

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.mapRange (fun (i : ι) => ⇑(f i)) ⋯ x).sum 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} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → 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) : f.sum g ∈ S

theorem Submodule.dfinsupp_sumAddHom_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → 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} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Submodule R N) : iSup p = LinearMap.range ((DFinsupp.lsum ℕ) fun (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 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} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) : ⨆ (i : ι), ⨆ (_ : p i), S i = LinearMap.range (((DFinsupp.lsum ℕ) fun (i : ι) => (S i).subtype) ∘ₗ DFinsupp.filterLinearMap R (fun (i : ι) => ↥(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} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Submodule R N) (x : N) : x ∈ iSup p ↔ ∃ (f : Π₀ (i : ι), ↥(p i)), ((DFinsupp.lsum ℕ) fun (i : ι) => (p i).subtype) f = x

A characterisation of the span of a family of submodules.

See also Submodule.mem_iSup_iff_exists_finsupp.

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

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

See also Submodule.mem_iSup_iff_exists_finsupp.

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

theorem Submodule.mem_iSup_iff_exists_finsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) (x : N) : x ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ (i : ι), f i ∈ p i) ∧ (f.sum fun (_i : ι) (xi : N) => xi) = x

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

theorem iSupIndep_iff_forall_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) : iSupIndep p ↔ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((DFinsupp.lsum ℕ) fun (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 iSupIndep_of_dfinsupp_lsum_injective and iSupIndep.dfinsupp_lsum_injective.

@[deprecated iSupIndep_iff_forall_dfinsupp]

theorem independent_iff_forall_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) : iSupIndep p ↔ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((DFinsupp.lsum ℕ) fun (i : ι) => (p i).subtype) (DFinsupp.erase i v) = ↑x → x = 0

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.

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

@[deprecated iSupIndep_of_dfinsupp_lsum_injective]

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

Alias of iSupIndep_of_dfinsupp_lsum_injective.

theorem iSupIndep_of_dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommMonoid N] (p : ι → AddSubmonoid N) (h : Function.Injective ⇑(DFinsupp.sumAddHom fun (i : ι) => (p i).subtype)) : iSupIndep p

@[deprecated iSupIndep_of_dfinsupp_sumAddHom_injective]

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

Alias of iSupIndep_of_dfinsupp_sumAddHom_injective.

theorem lsum_comp_mapRange_toSpanSingleton {ι : Type u_1} {R : Type u_2} {N : Type u_5} [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) : ((DFinsupp.lsum ℕ) fun (i : ι) => (p i).subtype) ∘ₗ (DFinsupp.mapRange.linearMap fun (i : ι) => LinearMap.toSpanSingleton R ↥(p i) ⟨v i, ⋯⟩) ∘ₗ ↑(finsuppLequivDFinsupp R) = Finsupp.linearCombination R v

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

theorem iSupIndep_of_dfinsupp_sumAddHom_injective' {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) (h : Function.Injective ⇑(DFinsupp.sumAddHom fun (i : ι) => (p i).subtype)) : iSupIndep p

If DFinsupp.sumAddHom applied with AddSubmonoid.subtype is injective then the additive subgroups are independent.

@[deprecated iSupIndep_of_dfinsupp_sumAddHom_injective']

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

Alias of iSupIndep_of_dfinsupp_sumAddHom_injective'.

---

If DFinsupp.sumAddHom applied with AddSubmonoid.subtype is injective then the additive subgroups are independent.

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

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.

@[deprecated iSupIndep.dfinsupp_lsum_injective]

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

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.

theorem iSupIndep.dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] {p : ι → AddSubgroup N} (h : iSupIndep p) : Function.Injective ⇑(DFinsupp.sumAddHom fun (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 iSupIndep.

@[deprecated iSupIndep.dfinsupp_sumAddHom_injective]

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

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.

theorem iSupIndep_iff_dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] (p : ι → Submodule R N) : iSupIndep p ↔ Function.Injective ⇑((DFinsupp.lsum ℕ) fun (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 iSupIndep.dfinsupp_lsum_injective for details.

@[deprecated iSupIndep_iff_dfinsupp_lsum_injective]

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

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.

theorem iSupIndep_iff_dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) : iSupIndep p ↔ Function.Injective ⇑(DFinsupp.sumAddHom fun (i : ι) => (p i).subtype)

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

@[deprecated iSupIndep_iff_dfinsupp_sumAddHom_injective]

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

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.

theorem iSupIndep.linearIndependent {R : Type u_2} {N : Type u_5} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] {ι : Type u_6} (p : ι → Submodule R N) (hp : iSupIndep 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 iSupIndep.linearIndependent'.

@[deprecated iSupIndep.linearIndependent]

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

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

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

@[deprecated iSupIndep_iff_linearIndependent_of_ne_zero]

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

Alias of iSupIndep_iff_linearIndependent_of_ne_zero.

theorem LinearMap.coe_dfinsupp_sum {R : Type u_6} {R₂ : Type u_7} {M : Type u_8} {M₂ : Type u_9} {ι : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_11} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂) : ⇑(t.sum g) = ⇑(t.sum fun (i : ι) (d : γ i) => g i d)

@[simp]

theorem LinearMap.dfinsupp_sum_apply {R : Type u_6} {R₂ : Type u_7} {M : Type u_8} {M₂ : Type u_9} {ι : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_11} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂) (b : M) : (t.sum g) b = t.sum fun (i : ι) (d : γ i) => (g i d) b

@[simp]

theorem LinearMap.map_dfinsupp_sumAddHom {R : Type u_6} {R₂ : Type u_7} {M : Type u_8} {M₂ : Type u_9} {ι : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_11} [DecidableEq ι] [(i : ι) → AddZeroClass (γ i)] (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ (i : ι), γ i} {g : (i : ι) → γ i →+ M} : f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun (i : ι) => f.toAddMonoidHom.comp (g i)) t

@[simp]

theorem LinearEquiv.map_dfinsupp_sumAddHom {R : Type u_6} {R₂ : Type u_7} {M : Type u_8} {M₂ : Type u_9} {ι : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {γ : ι → Type u_11} [DecidableEq ι] [(i : ι) → AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i →+ M) : f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun (i : ι) => f.toAddEquiv.toAddMonoidHom.comp (g i)) t