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

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_3} {M : ι → Type u_5} [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.

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

DFinsupp.single as a LinearMap

theorem DFinsupp.lhom_ext {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [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), φ (single i x) = ψ (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_3} {M : ι → Type u_5} {N : Type u_6} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] ⦃φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι), φ ∘ₗ lsingle i = ψ ∘ₗ 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).

theorem DFinsupp.lhom_ext'_iff {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] {φ ψ : (Π₀ (i : ι), M i) →ₗ[R] N} : φ = ψ ↔ ∀ (i : ι), φ ∘ₗ lsingle i = ψ ∘ₗ lsingle i

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

@[simp]

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

def DFinsupp.lapply {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [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.lapply_apply {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (f : Π₀ (i : ι), M i) : (lapply i) f = f i

theorem DFinsupp.injective_pi_lapply {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] : Function.Injective ⇑(LinearMap.pi lapply)

@[simp]

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

@[simp]

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

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

def DFinsupp.domLCongr {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (e : ι ≃ ι') : (Π₀ (i : ι), M i) ≃ₗ[R] Π₀ (i : ι'), M (e.symm i)

DFinsupp.equivCongrLeft as a linear equivalence.

This is the DFinsupp version of Finsupp.domLCongr.

@[simp]

theorem DFinsupp.domLCongr_apply {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (e : ι ≃ ι') (a✝ : Π₀ (i : ι), M i) : (domLCongr e) a✝ = comapDomain' ⇑e.symm ⋯ a✝

def DFinsupp.sigmaCurryLEquiv {ι : Type u_1} {R : Type u_3} [Semiring R] {α : ι → Type u_7} {M : (i : ι) → α i → Type u_8} [(i : ι) → (j : α i) → AddCommMonoid (M i j)] [(i : ι) → (j : α i) → Module R (M i j)] [DecidableEq ι] : (Π₀ (i : (x : ι) × α x), M i.fst i.snd) ≃ₗ[R] Π₀ (i : ι) (j : α i), M i j

DFinsupp.sigmaCurryEquiv as a linear equivalence.

This is the DFinsupp version of Finsupp.finsuppProdLEquiv.

@[simp]

theorem DFinsupp.sigmaCurryLEquiv_symm_apply {ι : Type u_1} {R : Type u_3} [Semiring R] {α : ι → Type u_7} {M : (i : ι) → α i → Type u_8} [(i : ι) → (j : α i) → AddCommMonoid (M i j)] [(i : ι) → (j : α i) → Module R (M i j)] [DecidableEq ι] (a✝ : Π₀ (i : ι) (j : α i), M i j) : sigmaCurryLEquiv.symm a✝ = sigmaCurryEquiv.symm a✝

@[simp]

theorem DFinsupp.sigmaCurryLEquiv_apply {ι : Type u_1} {R : Type u_3} [Semiring R] {α : ι → Type u_7} {M : (i : ι) → α i → Type u_8} [(i : ι) → (j : α i) → AddCommMonoid (M i j)] [(i : ι) → (j : α i) → Module R (M i j)] [DecidableEq ι] (a✝ : Π₀ (i : (x : ι) × α x), M i.fst i.snd) : sigmaCurryLEquiv a✝ = sigmaCurryEquiv a✝

def DFinsupp.linearEquivFunOnFintype {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] : (Π₀ (i : ι), M i) ≃ₗ[R] (i : ι) → M i

DFinsupp.equivFunOnFintype as a linear equivalence.

This is the DFinsupp version of Finsupp.linearEquivFunOnFintype.

@[simp]

theorem DFinsupp.linearEquivFunOnFintype_apply {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (a✝ : Π₀ (i : ι), M i) (i : ι) : linearEquivFunOnFintype a✝ i = a✝ i

@[simp]

theorem DFinsupp.linearEquivFunOnFintype_symm_apply {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (a✝ : (i : ι) → M i) : linearEquivFunOnFintype.symm a✝ = equivFunOnFintype.symm a✝

def DFinsupp.lsum {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [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.

@[simp]

theorem DFinsupp.lsum_apply_apply {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [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) : ((lsum S) F) a = (sumAddHom fun (i : ι) => (F i).toAddMonoidHom) a

@[simp]

theorem DFinsupp.lsum_symm_apply {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [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 : ι) : (lsum S).symm F i = F ∘ₗ lsingle i

theorem DFinsupp.lsum_single {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} {N : Type u_6} [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) : ((lsum S) F) (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.

theorem DFinsupp.lsum_lsingle {ι : Type u_1} {R : Type u_3} (S : Type u_4) {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] [Semiring S] [(i : ι) → Module S (M i)] [∀ (i : ι), SMulCommClass R S (M i)] : (lsum S) lsingle = LinearMap.id

theorem DFinsupp.iSup_range_lsingle {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] : ⨆ (i : ι), LinearMap.range (lsingle i) = ⊤

Bundled versions of DFinsupp.mapRange

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

theorem DFinsupp.mker_mapRangeAddMonoidHom {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) : AddMonoidHom.mker (mapRange.addMonoidHom f) = AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun (i : ι) => AddMonoidHom.mker (f i))

theorem DFinsupp.mrange_mapRangeAddMonoidHom {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) : AddMonoidHom.mrange (mapRange.addMonoidHom f) = AddSubmonoid.comap coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun (i : ι) => AddMonoidHom.mrange (f i))

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

def DFinsupp.mapRange.linearMap {ι : Type u_1} {R : Type u_3} [Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(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_apply {ι : Type u_1} {R : Type u_3} [Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) : (linearMap f) x = mapRange (fun (i : ι) (x : β₁ i) => (f i) x) ⋯ x

@[simp]

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

theorem DFinsupp.mapRange.linearMap_comp {ι : Type u_1} {R : Type u_3} [Semiring R] {β : ι → Type u_7} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(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) : (linearMap fun (i : ι) => f i ∘ₗ f₂ i) = linearMap f ∘ₗ linearMap f₂

theorem DFinsupp.sum_mapRange_index.linearMap {ι : Type u_1} {R : Type u_3} {N : Type u_6} [Semiring R] [AddCommMonoid N] [Module R N] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(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} : ((lsum ℕ) h) ((mapRange.linearMap f) l) = ((lsum ℕ) fun (i : ι) => h i ∘ₗ f i) l

theorem DFinsupp.ker_mapRangeLinearMap {ι : Type u_1} {R : Type u_3} [Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) : LinearMap.ker (mapRange.linearMap f) = Submodule.comap (coeFnLinearMap R) (Submodule.pi Set.univ fun (i : ι) => LinearMap.ker (f i))

theorem DFinsupp.range_mapRangeLinearMap {ι : Type u_1} {R : Type u_3} [Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) : LinearMap.range (mapRange.linearMap f) = Submodule.comap (coeFnLinearMap R) (Submodule.pi Set.univ fun (x : ι) => LinearMap.range (f x))

def DFinsupp.mapRange.linearEquiv {ι : Type u_1} {R : Type u_3} [Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(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_apply {ι : Type u_1} {R : Type u_3} [Semiring R] {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) : (linearEquiv e) x = mapRange (fun (i : ι) (x : β₁ i) => (e i) x) ⋯ x

@[simp]

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

theorem DFinsupp.mapRange.linearEquiv_trans {ι : Type u_1} {R : Type u_3} [Semiring R] {β : ι → Type u_7} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(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) : (linearEquiv fun (i : ι) => f i ≪≫ₗ f₂ i) = linearEquiv f ≪≫ₗ linearEquiv f₂

@[simp]

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

theorem DFinsupp.ker_mapRangeAddMonoidHom {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommGroup (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i) : (mapRange.addMonoidHom f).ker = AddSubgroup.comap coeFnAddMonoidHom (AddSubgroup.pi Set.univ fun (x : ι) => (f x).ker)

theorem DFinsupp.range_mapRangeAddMonoidHom {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [(i : ι) → AddCommGroup (β₁ i)] [(i : ι) → AddCommGroup (β₂ i)] (f : (i : ι) → β₂ i →+ β₁ i) : (mapRange.addMonoidHom f).range = AddSubgroup.comap coeFnAddMonoidHom (AddSubgroup.pi Set.univ fun (x : ι) => (f x).range)

def DFinsupp.coprodMap {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [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_3} {M : ι → Type u_5} {N : Type u_6} [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) : (coprodMap f) x = (mapRange (fun (i : ι) => ⇑(f i)) ⋯ x).sum fun (x : ι) => id

theorem DFinsupp.coprodMap_apply_single {ι : Type u_1} {R : Type u_3} {M : ι → Type u_5} {N : Type u_6} [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) : (coprodMap f) (single i x) = (f i) x

theorem Submodule.dfinsuppSum_mem {ι : Type u_1} {R : Type u_3} {N : Type u_6} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → Type u_7} [(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

@[deprecated Submodule.dfinsuppSum_mem (since := "2025-04-06")]

theorem Submodule.dfinsupp_sum_mem {ι : Type u_1} {R : Type u_3} {N : Type u_6} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → Type u_7} [(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

Alias of Submodule.dfinsuppSum_mem.

theorem Submodule.dfinsuppSumAddHom_mem {ι : Type u_1} {R : Type u_3} {N : Type u_6} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → Type u_7} [(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

@[deprecated Submodule.dfinsuppSumAddHom_mem (since := "2025-04-06")]

theorem Submodule.dfinsupp_sumAddHom_mem {ι : Type u_1} {R : Type u_3} {N : Type u_6} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → Type u_7} [(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

Alias of Submodule.dfinsuppSumAddHom_mem.

theorem Submodule.iSup_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_3} {N : Type u_6} [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_3} {N : Type u_6} [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_3} {N : Type u_6} [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_3} {N : Type u_6} [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_3} {N : Type u_6} [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_3} {N : Type u_6} [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_3} {N : Type u_6} [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_3} {N : Type u_6} [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.

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

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

@[deprecated iSupIndep_of_dfinsuppSumAddHom_injective (since := "2025-04-06")]

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

Alias of iSupIndep_of_dfinsuppSumAddHom_injective.

theorem lsum_comp_mapRange_toSpanSingleton {ι : Type u_1} {R : Type u_3} {N : Type u_6} [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_dfinsuppSumAddHom_injective' {ι : Type u_1} {N : Type u_6} [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_dfinsuppSumAddHom_injective' (since := "2025-04-06")]

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

Alias of iSupIndep_of_dfinsuppSumAddHom_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_3} {N : Type u_6} [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.

theorem iSupIndep.dfinsuppSumAddHom_injective {ι : Type u_1} {N : Type u_6} [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.dfinsuppSumAddHom_injective (since := "2025-04-06")]

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

Alias of iSupIndep.dfinsuppSumAddHom_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_3} {N : Type u_6} [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.

theorem iSupIndep_iff_dfinsuppSumAddHom_injective {ι : Type u_1} {N : Type u_6} [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_dfinsuppSumAddHom_injective (since := "2025-04-06")]

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

Alias of iSupIndep_iff_dfinsuppSumAddHom_injective.

---

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

noncomputable def iSupIndep.linearEquiv {ι : Type u_1} {R : Type u_3} {N : Type u_6} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ (i : ι), p i = ⊤) : (Π₀ (i : ι), ↥(p i)) ≃ₗ[R] N

If (pᵢ)ᵢ is a family of independent submodules that generates the whole module N, then N is isomorphic to the direct sum of the submodules.

@[simp]

theorem iSupIndep.linearEquiv_apply {ι : Type u_1} {R : Type u_3} {N : Type u_6} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ (i : ι), p i = ⊤) (a✝ : Π₀ (i : ι), ↥(p i)) : (ind.linearEquiv iSup_top) a✝ = (DFinsupp.sumAddHom fun (i : ι) => (p i).subtype.toAddMonoidHom) a✝

theorem iSupIndep.linearEquiv_symm_apply {ι : Type u_1} {R : Type u_3} {N : Type u_6} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] {p : ι → Submodule R N} (ind : iSupIndep p) (iSup_top : ⨆ (i : ι), p i = ⊤) {i : ι} {x : N} (h : x ∈ p i) : (ind.linearEquiv iSup_top).symm x = DFinsupp.single i ⟨x, h⟩

theorem iSupIndep.linearIndependent {R : Type u_3} {N : Type u_6} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] {ι : Type u_7} (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'.

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

theorem LinearMap.coe_dfinsuppSum {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_12} [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)

@[deprecated LinearMap.coe_dfinsuppSum (since := "2025-04-06")]

theorem LinearMap.coe_dfinsupp_sum {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_12} [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)

Alias of LinearMap.coe_dfinsuppSum.

@[simp]

theorem LinearMap.dfinsuppSum_apply {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_12} [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

@[deprecated LinearMap.dfinsuppSum_apply (since := "2025-04-06")]

theorem LinearMap.dfinsupp_sum_apply {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_12} [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

Alias of LinearMap.dfinsuppSum_apply.

@[simp]

theorem LinearMap.map_dfinsuppSumAddHom {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_12} [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

@[deprecated LinearMap.map_dfinsuppSumAddHom (since := "2025-04-06")]

theorem LinearMap.map_dfinsupp_sumAddHom {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_12} [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

Alias of LinearMap.map_dfinsuppSumAddHom.

@[simp]

theorem LinearEquiv.map_dfinsuppSumAddHom {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {γ : ι → Type u_12} [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

@[deprecated LinearEquiv.map_dfinsuppSumAddHom (since := "2025-04-06")]

theorem LinearEquiv.map_dfinsupp_sumAddHom {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} {ι : Type u_11} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {γ : ι → Type u_12} [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

Alias of LinearEquiv.map_dfinsuppSumAddHom.