Documentation

Mathlib.LinearAlgebra.DFinsupp

Properties of the module Π₀ i, M i #

Given an indexed collection of R-modules M i, the R-module structure on Π₀ i, M i is defined in Data.DFinsupp.

In this file we define LinearMap versions of various maps:

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
Instances For
    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
    Instances For
      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 ⦃ψ : (Π₀ (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'_iff {ι : 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} {ψ : (Π₀ (i : ι), M i) →ₗ[R] N} :
      φ = ψ ∀ (i : ι), φ ∘ₗ DFinsupp.lsingle i = ψ ∘ₗ DFinsupp.lsingle i
      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 ⦃ψ : (Π₀ (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 apply 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) :
      @[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) :
      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' := }
      Instances For
        @[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.

        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
        @[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
        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.
        Instances For
          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) :
          @[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
          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
          Instances For
            @[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) :
            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
            @[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
            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.
            Instances For
              @[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) :
              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
              Instances For
                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) :
                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 : ι) → β iN) (h : ∀ (c : ι), f c 0g 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) :
                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 (i : ι) (xi : (p i)) => 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 is, p i ∃ (μ : (i : ι) → (p i)), is, (μ i) = a
                theorem CompleteLattice.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) :
                CompleteLattice.Independent p ∀ (i : ι) (x : (p i)) (v : Π₀ (i : ι), (p i)), ((DFinsupp.lsum ) fun (i : ι) => (p i).subtype) (DFinsupp.erase i v) = xx = 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} [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ιSubmodule R N) (h : Function.Injective ((DFinsupp.lsum ) fun (i : ι) => (p i).subtype)) :
                theorem CompleteLattice.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 CompleteLattice.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 : CompleteLattice.Independent 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 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.

                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} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] (p : ιSubmodule R N) :
                CompleteLattice.Independent 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 CompleteLattice.Independent.dfinsupp_lsum_injective for details.

                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 {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 : CompleteLattice.Independent p) {v : ιN} (hv : ∀ (i : ι), v i p i) (hv' : ∀ (i : ι), v i 0) :

                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 {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) :
                theorem LinearMap.coe_dfinsupp_sum {R : Type u_6} {R₂ : Type u_8} {M : Type u_14} {M₂ : Type u_17} {ι : Type u_22} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ιType u_25} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ iM →ₛₗ[σ₁₂] 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_8} {M : Type u_14} {M₂ : Type u_17} {ι : Type u_22} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ιType u_25} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ iM →ₛₗ[σ₁₂] 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_8} {M : Type u_14} {M₂ : Type u_17} {ι : Type u_22} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ιType u_25} [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