Documentation

Mathlib.Algebra.DirectSum.Module

Direct sum of modules #

The first part of the file provides constructors for direct sums of modules. It provides a construction of the direct sum using the universal property and proves its uniqueness (DirectSum.toModule.unique).

The second part of the file covers the special case of direct sums of submodules of a fixed module M. There is a canonical linear map from this direct sum to M (DirectSum.coeLinearMap), and the construction is of particular importance when this linear map is an equivalence; that is, when the submodules provide an internal decomposition of M. The property is defined more generally elsewhere as DirectSum.IsInternal, but its basic consequences on Submodules are established in this file.

instance DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum {R : Type u} [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :
Module R (⨁ (i : ι), M i)
Equations
  • DirectSum.instModuleDirectSumInstAddCommMonoidDirectSum = DFinsupp.module
Equations
  • One or more equations did not get rendered due to their size.
theorem DirectSum.smul_apply {R : Type u} [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (b : R) (v : ⨁ (i : ι), M i) (i : ι) :
↑(b v) i = b v i
def DirectSum.lmk (R : Type u) [Semiring R] (ι : Type v) [dec_ι : DecidableEq ι] (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) :
((i : s) → M i) →ₗ[R] ⨁ (i : ι), M i

Create the direct sum given a family M of R modules indexed over ι.

Equations
Instances For
    def DirectSum.lof (R : Type u) [Semiring R] (ι : Type v) [dec_ι : DecidableEq ι] (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) :
    M i →ₗ[R] ⨁ (i : ι), M i

    Inclusion of each component into the direct sum.

    Equations
    Instances For
      theorem DirectSum.lof_eq_of (R : Type u) [Semiring R] (ι : Type v) [dec_ι : DecidableEq ι] (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (b : M i) :
      ↑(DirectSum.lof R ι M i) b = ↑(DirectSum.of M i) b
      theorem DirectSum.single_eq_lof (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (b : M i) :
      DFinsupp.single i b = ↑(DirectSum.lof R ι M i) b
      theorem DirectSum.mk_smul (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : Finset ι) (c : R) (x : (i : s) → M i) :
      ↑(DirectSum.mk M s) (c x) = c ↑(DirectSum.mk M s) x

      Scalar multiplication commutes with direct sums.

      theorem DirectSum.of_smul (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (c : R) (x : M i) :
      ↑(DirectSum.of M i) (c x) = c ↑(DirectSum.of M i) x

      Scalar multiplication commutes with the inclusion of each component into the direct sum.

      theorem DirectSum.support_smul {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → (x : M i) → Decidable (x 0)] (c : R) (v : ⨁ (i : ι), M i) :
      def DirectSum.toModule (R : Type u) [Semiring R] (ι : Type v) [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : Type u₁) [AddCommMonoid N] [Module R N] (φ : (i : ι) → M i →ₗ[R] N) :
      (⨁ (i : ι), M i) →ₗ[R] N

      The linear map constructed using the universal property of the coproduct.

      Equations
      Instances For
        theorem DirectSum.coe_toModule_eq_coe_toAddMonoid (R : Type u) [Semiring R] (ι : Type v) [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : Type u₁) [AddCommMonoid N] [Module R N] (φ : (i : ι) → M i →ₗ[R] N) :

        Coproducts in the categories of modules and additive monoids commute with the forgetful functor from modules to additive monoids.

        @[simp]
        theorem DirectSum.toModule_lof (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u₁} [AddCommMonoid N] [Module R N] {φ : (i : ι) → M i →ₗ[R] N} (i : ι) (x : M i) :
        ↑(DirectSum.toModule R ι N φ) (↑(DirectSum.lof R ι M i) x) = ↑(φ i) x

        The map constructed using the universal property gives back the original maps when restricted to each component.

        theorem DirectSum.toModule.unique (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u₁} [AddCommMonoid N] [Module R N] (ψ : (⨁ (i : ι), M i) →ₗ[R] N) (f : ⨁ (i : ι), M i) :
        ψ f = ↑(DirectSum.toModule R ι N fun i => LinearMap.comp ψ (DirectSum.lof R ι M i)) f

        Every linear map from a direct sum agrees with the one obtained by applying the universal property to each of its components.

        theorem DirectSum.linearMap_ext (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u₁} [AddCommMonoid N] [Module R N] ⦃ψ : (⨁ (i : ι), M i) →ₗ[R] N ⦃ψ' : (⨁ (i : ι), M i) →ₗ[R] N (H : ∀ (i : ι), LinearMap.comp ψ (DirectSum.lof R ι M i) = LinearMap.comp ψ' (DirectSum.lof R ι M i)) :
        ψ = ψ'

        Two LinearMaps out of a direct sum are equal if they agree on the generators.

        See note [partially-applied ext lemmas].

        def DirectSum.lsetToSet (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (S : Set ι) (T : Set ι) (H : S T) :
        (⨁ (i : S), M i) →ₗ[R] ⨁ (i : T), M i

        The inclusion of a subset of the direct summands into a larger subset of the direct summands, as a linear map.

        Equations
        Instances For
          @[simp]
          theorem DirectSum.linearEquivFunOnFintype_apply (R : Type u) [Semiring R] (ι : Type v) (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] :
          ∀ (a : Π₀ (i : ι), (fun i => (fun i => M i) i) i) (a_1 : ι), ↑(DirectSum.linearEquivFunOnFintype R ι M) a a_1 = a a_1
          def DirectSum.linearEquivFunOnFintype (R : Type u) [Semiring R] (ι : Type v) (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] :
          (⨁ (i : ι), M i) ≃ₗ[R] (i : ι) → M i

          Given Fintype α, linearEquivFunOnFintype R is the natural R-linear equivalence between ⨁ i, M i and ∀ i, M i.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem DirectSum.linearEquivFunOnFintype_lof (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] (i : ι) (m : M i) :
            @[simp]
            theorem DirectSum.linearEquivFunOnFintype_symm_single (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] [DecidableEq ι] (i : ι) (m : M i) :
            @[simp]
            theorem DirectSum.linearEquivFunOnFintype_symm_coe (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [Fintype ι] (f : ⨁ (i : ι), M i) :
            def DirectSum.lid (R : Type u) [Semiring R] (M : Type v) (ι : optParam (Type u_1) PUnit.{u_1 + 1} ) [AddCommMonoid M] [Module R M] [Unique ι] :
            (⨁ (x : ι), M) ≃ₗ[R] M

            The natural linear equivalence between ⨁ _ : ι, M and M when Unique ι.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def DirectSum.component (R : Type u) [Semiring R] (ι : Type v) (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) :
              (⨁ (i : ι), M i) →ₗ[R] M i

              The projection map onto one component, as a linear map.

              Equations
              Instances For
                theorem DirectSum.apply_eq_component (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (f : ⨁ (i : ι), M i) (i : ι) :
                f i = ↑(DirectSum.component R ι M i) f
                theorem DirectSum.ext (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {f : ⨁ (i : ι), M i} {g : ⨁ (i : ι), M i} (h : ∀ (i : ι), ↑(DirectSum.component R ι M i) f = ↑(DirectSum.component R ι M i) g) :
                f = g
                theorem DirectSum.ext_iff (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {f : ⨁ (i : ι), M i} {g : ⨁ (i : ι), M i} :
                f = g ∀ (i : ι), ↑(DirectSum.component R ι M i) f = ↑(DirectSum.component R ι M i) g
                @[simp]
                theorem DirectSum.lof_apply (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (b : M i) :
                ↑(↑(DirectSum.lof R ι M i) b) i = b
                @[simp]
                theorem DirectSum.component.lof_self (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (b : M i) :
                ↑(DirectSum.component R ι M i) (↑(DirectSum.lof R ι M i) b) = b
                theorem DirectSum.component.of (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (j : ι) (b : M j) :
                ↑(DirectSum.component R ι M i) (↑(DirectSum.lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0
                def DirectSum.lequivCongrLeft (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type u_1} (h : ι κ) :
                (⨁ (i : ι), M i) ≃ₗ[R] ⨁ (k : κ), M (h.symm k)

                Reindexing terms of a direct sum is linear.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem DirectSum.lequivCongrLeft_apply (R : Type u) [Semiring R] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type u_1} (h : ι κ) (f : ⨁ (i : ι), M i) (k : κ) :
                  ↑(↑(DirectSum.lequivCongrLeft R h) f) k = f (h.symm k)
                  def DirectSum.sigmaLcurry (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {α : ιType u_1} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] :
                  (⨁ (i : (i : ι) × α i), δ i.fst i.snd) →ₗ[R] ⨁ (i : ι) (j : α i), δ i j

                  curry as a linear map.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    theorem DirectSum.sigmaLcurry_apply (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {α : ιType u_1} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] (f : ⨁ (i : (x : ι) × α x), δ i.fst i.snd) (i : ι) (j : α i) :
                    ↑(↑(↑(DirectSum.sigmaLcurry R) f) i) j = f { fst := i, snd := j }
                    noncomputable def DirectSum.sigmaLuncurry (R : Type u) [Semiring R] {ι : Type v} {α : ιType u_1} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → DecidableEq (δ i j)] :
                    (⨁ (i : ι) (j : α i), δ i j) →ₗ[R] ⨁ (i : (x : ι) × α x), δ i.fst i.snd

                    uncurry as a linear map.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem DirectSum.sigmaLuncurry_apply (R : Type u) [Semiring R] {ι : Type v} {α : ιType u_1} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → DecidableEq (δ i j)] (f : ⨁ (i : ι) (j : α i), δ i j) (i : ι) (j : α i) :
                      ↑(↑(DirectSum.sigmaLuncurry R) f) { fst := i, snd := j } = ↑(f i) j
                      def DirectSum.sigmaLcurryEquiv (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {α : ιType u_1} {δ : (i : ι) → α iType w} [(i : ι) → (j : α i) → AddCommMonoid (δ i j)] [(i : ι) → (j : α i) → Module R (δ i j)] [(i : ι) → DecidableEq (α i)] [(i : ι) → (j : α i) → DecidableEq (δ i j)] :
                      (⨁ (i : (x : ι) × α x), δ i.fst i.snd) ≃ₗ[R] ⨁ (i : ι) (j : α i), δ i j

                      curryEquiv as a linear equiv.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem DirectSum.lequivProdDirectSum_apply (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] [(i : Option ι) → Module R (α i)] :
                        ∀ (a : ⨁ (i : Option ι), α i), ↑(DirectSum.lequivProdDirectSum R) a = Equiv.toFun DirectSum.addEquivProdDirectSum.toEquiv a
                        @[simp]
                        theorem DirectSum.lequivProdDirectSum_symm_apply (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] [(i : Option ι) → Module R (α i)] :
                        ∀ (a : α none × ⨁ (i : ι), α (some i)), ↑(LinearEquiv.symm (DirectSum.lequivProdDirectSum R)) a = Equiv.invFun DirectSum.addEquivProdDirectSum.toEquiv a
                        noncomputable def DirectSum.lequivProdDirectSum (R : Type u) [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {α : Option ιType w} [(i : Option ι) → AddCommMonoid (α i)] [(i : Option ι) → Module R (α i)] :
                        (⨁ (i : Option ι), α i) ≃ₗ[R] α none × ⨁ (i : ι), α (some i)

                        Linear isomorphism obtained by separating the term of index none of a direct sum over Option ι.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          def DirectSum.coeLinearMap {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] (A : ιSubmodule R M) :
                          (⨁ (i : ι), { x // x A i }) →ₗ[R] M

                          The canonical embedding from ⨁ i, A i to M where A is a collection of Submodule R M indexed by ι. This is DirectSum.coeAddMonoidHom as a LinearMap.

                          Equations
                          Instances For
                            @[simp]
                            theorem DirectSum.coeLinearMap_of {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] (A : ιSubmodule R M) (i : ι) (x : { x // x A i }) :
                            ↑(DirectSum.coeLinearMap A) (↑(DirectSum.of (fun i => { x // x A i }) i) x) = x
                            theorem DirectSum.IsInternal.submodule_iSup_eq_top {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ιSubmodule R M} (h : DirectSum.IsInternal A) :

                            If a direct sum of submodules is internal then the submodules span the module.

                            theorem DirectSum.IsInternal.submodule_independent {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ιSubmodule R M} (h : DirectSum.IsInternal A) :

                            If a direct sum of submodules is internal then the submodules are independent.

                            noncomputable def DirectSum.IsInternal.collectedBasis {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ιSubmodule R M} (h : DirectSum.IsInternal A) {α : ιType u_2} (v : (i : ι) → Basis (α i) R { x // x A i }) :
                            Basis ((i : ι) × α i) R M

                            Given an internal direct sum decomposition of a module M, and a basis for each of the components of the direct sum, the disjoint union of these bases is a basis for M.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem DirectSum.IsInternal.collectedBasis_coe {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ιSubmodule R M} (h : DirectSum.IsInternal A) {α : ιType u_2} (v : (i : ι) → Basis (α i) R { x // x A i }) :
                              ↑(DirectSum.IsInternal.collectedBasis h v) = fun a => ↑(↑(v a.fst) a.snd)
                              theorem DirectSum.IsInternal.collectedBasis_mem {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ιSubmodule R M} (h : DirectSum.IsInternal A) {α : ιType u_2} (v : (i : ι) → Basis (α i) R { x // x A i }) (a : (i : ι) × α i) :
                              theorem DirectSum.IsInternal.isCompl {R : Type u} [Semiring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommMonoid M] [Module R M] {A : ιSubmodule R M} {i : ι} {j : ι} (hij : i j) (h : Set.univ = {i, j}) (hi : DirectSum.IsInternal A) :
                              IsCompl (A i) (A j)

                              When indexed by only two distinct elements, DirectSum.IsInternal implies the two submodules are complementary. Over a Ring R, this is true as an iff, as DirectSum.isInternal_submodule_iff_isCompl.

                              theorem DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] {A : ιSubmodule R M} (hi : CompleteLattice.Independent A) (hs : iSup A = ) :

                              Note that this is not generally true for [Semiring R]; see CompleteLattice.Independent.dfinsupp_lsum_injective for details.

                              theorem DirectSum.isInternal_submodule_iff_isCompl {R : Type u} [Ring R] {ι : Type v} [dec_ι : DecidableEq ι] {M : Type u_1} [AddCommGroup M] [Module R M] (A : ιSubmodule R M) {i : ι} {j : ι} (hij : i j) (h : Set.univ = {i, j}) :

                              If a collection of submodules has just two indices, i and j, then DirectSum.IsInternal is equivalent to isCompl.

                              Now copy the lemmas for subgroup and submonoids.