Sums as a linear map

Given an R-module M, the R-module structure on α →₀ M is defined in Data.Finsupp.Basic.

Main definitions

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

Tags

function with finite support, module, linear algebra

theorem Finsupp.smul_sum {α : Type u_1} {β : Type u_2} {R : Type u_3} {M : Type u_5} [Zero β] [AddCommMonoid M] [DistribSMul R M] {v : α →₀ β} {c : R} {h : α → β → M} : c • v.sum h = v.sum fun (a : α) (b : β) => c • h a b

@[simp]

theorem Finsupp.sum_smul_index_semilinearMap' {α : Type u_1} {R : Type u_3} {R₂ : Type u_4} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R₂ M₂] {σ : R →+* R₂} {v : α →₀ M} {c : R} {h : α → M →ₛₗ[σ] M₂} : ((c • v).sum fun (a : α) => ⇑(h a)) = σ c • v.sum fun (a : α) => ⇑(h a)

theorem Finsupp.sum_smul_index_linearMap' {α : Type u_1} {R : Type u_3} {M : Type u_5} {M₂ : Type u_6} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M₂] [Module R M₂] {v : α →₀ M} {c : R} {h : α → M →ₗ[R] M₂} : ((c • v).sum fun (a : α) => ⇑(h a)) = c • v.sum fun (a : α) => ⇑(h a)

instance LinearMap.CompatibleSMul.finsupp_dom (R : Type u_9) (S : Type u_10) (M : Type u_11) (N : Type u_12) (ι : Type u_13) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module S M] [Module S N] [SMulZeroClass R M] [DistribSMul R N] [CompatibleSMul M N R S] : CompatibleSMul (ι →₀ M) N R S

instance LinearMap.CompatibleSMul.finsupp_cod (R : Type u_9) (S : Type u_10) (M : Type u_11) (N : Type u_12) (ι : Type u_13) [Semiring S] [AddCommMonoid M] [AddCommMonoid N] [Module S M] [Module S N] [SMul R M] [SMulZeroClass R N] [CompatibleSMul M N R S] : CompatibleSMul M (ι →₀ N) R S

def Finsupp.lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [Semiring R] [Semiring R₂] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} [Module S N] [SMulCommClass R₂ S N] : (α → M →ₛₗ[σ] N) ≃ₗ[S] (α →₀ M) →ₛₗ[σ] N

Lift a family of linear maps M →ₗ[R] N indexed by x : α to a linear map from α →₀ M to N using Finsupp.sum. This is an upgraded version of Finsupp.liftAddHom.

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

@[simp]

theorem Finsupp.coe_lsum {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [Semiring R] [Semiring R₂] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} [Module S N] [SMulCommClass R₂ S N] (f : α → M →ₛₗ[σ] N) : ⇑((lsum S) f) = fun (d : α →₀ M) => d.sum fun (i : α) => ⇑(f i)

theorem Finsupp.lsum_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [Semiring R] [Semiring R₂] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} [Module S N] [SMulCommClass R₂ S N] (f : α → M →ₛₗ[σ] N) (l : α →₀ M) : ((lsum S) f) l = l.sum fun (b : α) => ⇑(f b)

theorem Finsupp.lsum_single {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [Semiring R] [Semiring R₂] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} [Module S N] [SMulCommClass R₂ S N] (f : α → M →ₛₗ[σ] N) (i : α) (m : M) : ((lsum S) f) (single i m) = (f i) m

@[simp]

theorem Finsupp.lsum_comp_lsingle {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [Semiring R] [Semiring R₂] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} [Module S N] [SMulCommClass R₂ S N] (f : α → M →ₛₗ[σ] N) (i : α) : (lsum S) f ∘ₛₗ lsingle i = f i

theorem Finsupp.lsum_symm_apply {α : Type u_1} {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} (S : Type u_8) [Semiring R] [Semiring R₂] [Semiring S] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} [Module S N] [SMulCommClass R₂ S N] (f : (α →₀ M) →ₛₗ[σ] N) (x : α) : (lsum S).symm f x = f ∘ₛₗ lsingle x

noncomputable def Finsupp.lift (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_9) : (X → M) ≃+ ((X →₀ R) →ₗ[R] M)

A slight rearrangement from lsum gives us the bijection underlying the free-forgetful adjunction for R-modules.

@[simp]

theorem Finsupp.lift_symm_apply (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_9) (f : (X →₀ R) →ₗ[R] M) (x : X) : (lift M R X).symm f x = f (single x 1)

@[simp]

theorem Finsupp.lift_apply (M : Type u_2) (R : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_9) (f : X → M) (g : X →₀ R) : ((lift M R X) f) g = g.sum fun (x : X) (r : R) => r • f x

noncomputable def Finsupp.llift (M : Type u_2) (R : Type u_5) (S : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] (X : Type u_9) [Module S M] [SMulCommClass R S M] : (X → M) ≃ₗ[S] (X →₀ R) →ₗ[R] M

Given compatible S and R-module structures on M and a type X, the set of functions X → M is S-linearly equivalent to the R-linear maps from the free R-module on X to M.

@[simp]

theorem Finsupp.llift_apply (M : Type u_2) (R : Type u_5) (S : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] (X : Type u_9) [Module S M] [SMulCommClass R S M] (f : X → M) (x : X →₀ R) : ((llift M R S X) f) x = ((lift M R X) f) x

@[simp]

theorem Finsupp.llift_symm_apply (M : Type u_2) (R : Type u_5) (S : Type u_8) [Semiring R] [Semiring S] [AddCommMonoid M] [Module R M] (X : Type u_9) [Module S M] [SMulCommClass R S M] (f : (X →₀ R) →ₗ[R] M) (x : X) : (llift M R S X).symm f x = f (single x 1)

def Finsupp.domLCongr {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_9} {α₂ : Type u_10} (e : α₁ ≃ α₂) : (α₁ →₀ M) ≃ₗ[R] α₂ →₀ M

An equivalence of domains induces a linear equivalence of finitely supported functions.

This is Finsupp.domCongr as a LinearEquiv. See also LinearMap.funCongrLeft for the case of arbitrary functions.

@[simp]

theorem Finsupp.domLCongr_apply {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_9} {α₂ : Type u_10} (e : α₁ ≃ α₂) (v : α₁ →₀ M) : (Finsupp.domLCongr e) v = (Finsupp.domCongr e) v

@[simp]

theorem Finsupp.domLCongr_refl {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] : Finsupp.domLCongr (Equiv.refl α) = LinearEquiv.refl R (α →₀ M)

theorem Finsupp.domLCongr_trans {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_9} {α₂ : Type u_10} {α₃ : Type u_11} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃) : Finsupp.domLCongr f ≪≫ₗ Finsupp.domLCongr f₂ = Finsupp.domLCongr (f.trans f₂)

@[simp]

theorem Finsupp.domLCongr_symm {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_9} {α₂ : Type u_10} (f : α₁ ≃ α₂) : (Finsupp.domLCongr f).symm = Finsupp.domLCongr f.symm

theorem Finsupp.domLCongr_single {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] {α₁ : Type u_9} {α₂ : Type u_10} (e : α₁ ≃ α₂) (i : α₁) (m : M) : (Finsupp.domLCongr e) (single i m) = single (e i) m

def Finsupp.lcongr {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} {σ_inv : R₂ →+* R} [RingHomInvPair σ σ_inv] [RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10} (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) : (ι →₀ M) ≃ₛₗ[σ] κ →₀ N

An equivalence of domain and a linear equivalence of codomain induce a linear equivalence of the corresponding finitely supported functions.

@[simp]

theorem Finsupp.lcongr_single {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} {σ_inv : R₂ →+* R} [RingHomInvPair σ σ_inv] [RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10} (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) (i : ι) (m : M) : (lcongr e₁ e₂) (single i m) = single (e₁ i) (e₂ m)

@[simp]

theorem Finsupp.lcongr_apply_apply {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} {σ_inv : R₂ →+* R} [RingHomInvPair σ σ_inv] [RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10} (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) (f : ι →₀ M) (k : κ) : ((lcongr e₁ e₂) f) k = e₂ (f (e₁.symm k))

theorem Finsupp.lcongr_symm_single {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} {σ_inv : R₂ →+* R} [RingHomInvPair σ σ_inv] [RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10} (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) (k : κ) (n : N) : (lcongr e₁ e₂).symm (single k n) = single (e₁.symm k) (e₂.symm n)

@[simp]

theorem Finsupp.lcongr_symm {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [Semiring R] [Semiring R₂] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R₂ N] {σ : R →+* R₂} {σ_inv : R₂ →+* R} [RingHomInvPair σ σ_inv] [RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10} (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) : (lcongr e₁ e₂).symm = lcongr e₁.symm e₂.symm

theorem Submodule.finsuppSum_mem (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {β : Type u_5} [Zero β] (S : Submodule R M) (f : ι →₀ β) (g : ι → β → M) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S

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

theorem Submodule.finsupp_sum_mem (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {ι : Type u_4} {β : Type u_5} [Zero β] (S : Submodule R M) (f : ι →₀ β) (g : ι → β → M) (h : ∀ (c : ι), f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S

Alias of Submodule.finsuppSum_mem.

def LinearMap.splittingOfFinsuppSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f) : (α →₀ R) →ₗ[R] M

A surjective linear map to finitely supported functions has a splitting.

theorem LinearMap.splittingOfFinsuppSurjective_splits {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f) : f ∘ₗ f.splittingOfFinsuppSurjective s = id

theorem LinearMap.leftInverse_splittingOfFinsuppSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f) : Function.LeftInverse ⇑f ⇑(f.splittingOfFinsuppSurjective s)

theorem LinearMap.splittingOfFinsuppSurjective_injective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (f : M →ₗ[R] α →₀ R) (s : Function.Surjective ⇑f) : Function.Injective ⇑(f.splittingOfFinsuppSurjective s)

theorem LinearMap.coe_finsupp_sum {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) : ⇑(t.sum g) = ⇑(t.sum fun (i : ι) (d : γ) => g i d)

@[simp]

theorem LinearMap.finsupp_sum_apply {R : Type u_4} {R₂ : Type u_5} {M : Type u_6} {M₂ : Type u_7} {ι : Type u_8} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : Type u_9} [Zero γ] (t : ι →₀ γ) (g : ι → γ → M →ₛₗ[σ₁₂] M₂) (b : M) : (t.sum g) b = t.sum fun (i : ι) (d : γ) => (g i d) b

def Submodule.mulLeftMap {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_5} (m : ι → ↥M) : (ι →₀ ↥N) →ₗ[R] S

If M and N are submodules of an R-algebra S, m : ι → M is a family of elements, then there is an R-linear map from ι →₀ N to S which maps { n_i } to the sum of m_i * n_i. This is used in the definition of linearly disjointness.

theorem Submodule.mulLeftMap_apply {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] {M N : Submodule R S} {ι : Type u_5} (m : ι → ↥M) (n : ι →₀ ↥N) : (mulLeftMap N m) n = n.sum fun (i : ι) (n : ↥N) => ↑(m i) * ↑n

@[simp]

theorem Submodule.mulLeftMap_apply_single {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] {M N : Submodule R S} {ι : Type u_5} (m : ι → ↥M) (i : ι) (n : ↥N) : (mulLeftMap N m) (Finsupp.single i n) = ↑(m i) * ↑n

def Submodule.mulRightMap {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] (M : Submodule R S) {N : Submodule R S} {ι : Type u_5} (n : ι → ↥N) : (ι →₀ ↥M) →ₗ[R] S

If M and N are submodules of an R-algebra S, n : ι → N is a family of elements, then there is an R-linear map from ι →₀ M to S which maps { m_i } to the sum of m_i * n_i. This is used in the definition of linearly disjointness.

theorem Submodule.mulRightMap_apply {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] {M N : Submodule R S} {ι : Type u_5} (n : ι → ↥N) (m : ι →₀ ↥M) : (M.mulRightMap n) m = m.sum fun (i : ι) (m : ↥M) => ↑m * ↑(n i)

@[simp]

theorem Submodule.mulRightMap_apply_single {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] {M N : Submodule R S} {ι : Type u_5} (n : ι → ↥N) (i : ι) (m : ↥M) : (M.mulRightMap n) (Finsupp.single i m) = ↑m * ↑(n i)

theorem Submodule.mulLeftMap_eq_mulRightMap_of_commute {R : Type u_1} [Semiring R] {S : Type u_4} [Semiring S] [Module R S] [SMulCommClass R R S] [IsScalarTower R S S] [SMulCommClass R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_5} (m : ι → ↥M) (hc : ∀ (i : ι) (n : ↥N), Commute ↑(m i) ↑n) : mulLeftMap N m = N.mulRightMap m

theorem Submodule.mulLeftMap_eq_mulRightMap {R : Type u_1} [Semiring R] {S : Type u_5} [CommSemiring S] [Module R S] [SMulCommClass R R S] [SMulCommClass R S S] [IsScalarTower R S S] {M : Submodule R S} (N : Submodule R S) {ι : Type u_6} (m : ι → ↥M) : mulLeftMap N m = N.mulRightMap m