# 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} [] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] :
Module R (⨁ (i : ι), M i)
theorem DirectSum.smul_apply {R : Type u} [] {ι : 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) [] (ι : Type v) [dec_ι : ] (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (s : ) :
((i : s) → M i) →ₗ[R] ⨁ (i : ι), M i

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

Instances For
def DirectSum.lof (R : Type u) [] (ι : Type v) [dec_ι : ] (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.

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

Scalar multiplication commutes with direct sums.

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

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

theorem DirectSum.support_smul {R : Type u} [] {ι : Type v} [dec_ι : ] {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) [] (ι : Type v) [dec_ι : ] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : Type u₁) [] [Module R N] (φ : (i : ι) → M i →ₗ[R] N) :
(⨁ (i : ι), M i) →ₗ[R] N

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

Instances For
theorem DirectSum.coe_toModule_eq_coe_toAddMonoid (R : Type u) [] (ι : Type v) [dec_ι : ] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (N : Type u₁) [] [Module R N] (φ : (i : ι) → M i →ₗ[R] N) :
↑() = ↑(DirectSum.toAddMonoid fun i => )

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) [] {ι : Type v} [dec_ι : ] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u₁} [] [Module R N] {φ : (i : ι) → M i →ₗ[R] N} (i : ι) (x : M i) :
↑() (↑(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) [] {ι : Type v} [dec_ι : ] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u₁} [] [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) [] {ι : Type v} [dec_ι : ] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {N : Type u₁} [] [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) [] {ι : Type v} [dec_ι : ] {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.

Instances For
@[simp]
theorem DirectSum.linearEquivFunOnFintype_apply (R : Type u) [] (ι : Type v) (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [] :
∀ (a : Π₀ (i : ι), (fun i => (fun i => M i) i) i) (a_1 : ι), ↑() a a_1 = a a_1
def DirectSum.linearEquivFunOnFintype (R : Type u) [] (ι : Type v) (M : ιType w) [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [] :
(⨁ (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.

Instances For
@[simp]
theorem DirectSum.linearEquivFunOnFintype_lof (R : Type u) [] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [] [] (i : ι) (m : M i) :
↑() (↑(DirectSum.lof R ι M i) m) =
@[simp]
theorem DirectSum.linearEquivFunOnFintype_symm_single (R : Type u) [] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [] [] (i : ι) (m : M i) :
↑() () = ↑(DirectSum.lof R ι M i) m
@[simp]
theorem DirectSum.linearEquivFunOnFintype_symm_coe (R : Type u) [] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [] (f : ⨁ (i : ι), M i) :
↑() f = f
def DirectSum.lid (R : Type u) [] (M : Type v) (ι : ) [] [Module R M] [] :
(⨁ (x : ι), M) ≃ₗ[R] M

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

Instances For
def DirectSum.component (R : Type u) [] (ι : 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.

Instances For
theorem DirectSum.apply_eq_component (R : Type u) [] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (f : ⨁ (i : ι), M i) (i : ι) :
f i = ↑() f
theorem DirectSum.ext (R : Type u) [] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {f : ⨁ (i : ι), M i} {g : ⨁ (i : ι), M i} (h : ∀ (i : ι), ↑() f = ↑() g) :
f = g
theorem DirectSum.ext_iff (R : Type u) [] {ι : 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 : ι), ↑() f = ↑() g
@[simp]
theorem DirectSum.lof_apply (R : Type u) [] {ι : Type v} [dec_ι : ] {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) [] {ι : Type v} [dec_ι : ] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (b : M i) :
↑() (↑(DirectSum.lof R ι M i) b) = b
theorem DirectSum.component.of (R : Type u) [] {ι : Type v} [dec_ι : ] {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (j : ι) (b : M j) :
↑() (↑(DirectSum.lof R ι M j) b) = if h : j = i then Eq.recOn h b else 0
def DirectSum.lequivCongrLeft (R : Type u) [] {ι : 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.

Instances For
@[simp]
theorem DirectSum.lequivCongrLeft_apply (R : Type u) [] {ι : Type v} {M : ιType w} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] {κ : Type u_1} (h : ι κ) (f : ⨁ (i : ι), M i) (k : κ) :
↑(↑() f) k = f (h.symm k)
def DirectSum.sigmaLcurry (R : Type u) [] {ι : Type v} [dec_ι : ] {α : ι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.

Instances For
@[simp]
theorem DirectSum.sigmaLcurry_apply (R : Type u) [] {ι : Type v} [dec_ι : ] {α : ι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) :
↑(↑(↑() f) i) j = f { fst := i, snd := j }
noncomputable def DirectSum.sigmaLuncurry (R : Type u) [] {ι : 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.

Instances For
@[simp]
theorem DirectSum.sigmaLuncurry_apply (R : Type u) [] {ι : 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) :
↑(↑() f) { fst := i, snd := j } = ↑(f i) j
def DirectSum.sigmaLcurryEquiv (R : Type u) [] {ι : Type v} [dec_ι : ] {α : ι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.

Instances For
@[simp]
theorem DirectSum.lequivProdDirectSum_apply (R : Type u) [] {ι : Type v} [dec_ι : ] {α : Type w} [(i : ) → AddCommMonoid (α i)] [(i : ) → Module R (α i)] :
∀ (a : ⨁ (i : ), α i), = Equiv.toFun DirectSum.addEquivProdDirectSum.toEquiv a
@[simp]
theorem DirectSum.lequivProdDirectSum_symm_apply (R : Type u) [] {ι : Type v} [dec_ι : ] {α : Type w} [(i : ) → AddCommMonoid (α i)] [(i : ) → Module R (α i)] :
∀ (a : α none × ⨁ (i : ι), α (some i)), = Equiv.invFun DirectSum.addEquivProdDirectSum.toEquiv a
noncomputable def DirectSum.lequivProdDirectSum (R : Type u) [] {ι : Type v} [dec_ι : ] {α : Type w} [(i : ) → AddCommMonoid (α i)] [(i : ) → Module R (α i)] :
(⨁ (i : ), α i) ≃ₗ[R] α none × ⨁ (i : ι), α (some i)

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

Instances For
def DirectSum.coeLinearMap {R : Type u} [] {ι : Type v} [dec_ι : ] {M : Type u_1} [] [Module R M] (A : ι) :
(⨁ (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.

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

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

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

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

noncomputable def DirectSum.IsInternal.collectedBasis {R : Type u} [] {ι : Type v} [dec_ι : ] {M : Type u_1} [] [Module R M] {A : ι} (h : ) {α : ι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.

Instances For
@[simp]
theorem DirectSum.IsInternal.collectedBasis_coe {R : Type u} [] {ι : Type v} [dec_ι : ] {M : Type u_1} [] [Module R M] {A : ι} (h : ) {α : ιType u_2} (v : (i : ι) → Basis (α i) R { x // x A i }) :
= fun a => ↑(↑(v a.fst) a.snd)
theorem DirectSum.IsInternal.collectedBasis_mem {R : Type u} [] {ι : Type v} [dec_ι : ] {M : Type u_1} [] [Module R M] {A : ι} (h : ) {α : ιType u_2} (v : (i : ι) → Basis (α i) R { x // x A i }) (a : (i : ι) × α i) :
A a.fst
theorem DirectSum.IsInternal.isCompl {R : Type u} [] {ι : Type v} [dec_ι : ] {M : Type u_1} [] [Module R M] {A : ι} {i : ι} {j : ι} (hij : i j) (h : Set.univ = {i, j}) (hi : ) :
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_ι : ] {M : Type u_1} [] [Module R M] {A : ι} (hi : ) (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_independent_and_iSup_eq_top {R : Type u} [Ring R] {ι : Type v} [dec_ι : ] {M : Type u_1} [] [Module R M] (A : ι) :

iff version of DirectSum.isInternal_submodule_of_independent_of_iSup_eq_top, DirectSum.IsInternal.submodule_independent, and DirectSum.IsInternal.submodule_iSup_eq_top.

theorem DirectSum.isInternal_submodule_iff_isCompl {R : Type u} [Ring R] {ι : Type v} [dec_ι : ] {M : Type u_1} [] [Module R M] (A : ι) {i : ι} {j : ι} (hij : i j) (h : Set.univ = {i, j}) :
IsCompl (A i) (A 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.

theorem DirectSum.IsInternal.addSubmonoid_independent {ι : Type v} [dec_ι : ] {M : Type u_2} [] {A : ι} (h : ) :
theorem DirectSum.IsInternal.addSubgroup_independent {ι : Type v} [dec_ι : ] {M : Type u_2} [] {A : ι} (h : ) :