Metamath Proof Explorer

Table of Contents - 11.1.1. Direct sum of left modules

According to Wikipedia ("Direct sum of modules", 28-Mar-2019, "Let R be a ring, and { M<sub>i</sub>: i &isin; I } a family of left R-modules indexed by the set I. The direct sum of {M<sub>i</sub>} is then defined to be the set of all sequences (&alpha;<sub>i</sub>) where &alpha;<sub>i</sub> &isin; M<sub>i</sub> and &alpha;<sub>i</sub> = 0 for cofinitely many indices i. (The direct product is analogous but the indices do not need to cofinitely vanish.)". In this definition, "cofinitely many" means "almost all" or "for all but finitely many". Furthemore, "This set inherits the module structure via componentwise addition and scalar multiplication. Explicitly, two such sequences &alpha; and &beta; can be added by writing (&alpha; + &beta;)<sub>i</sub> = &alpha;<sub>i</sub> + &beta;<sub>i</sub> for all i (note that this is again zero for all but finitely many indices), and such a sequence can be multiplied with an element r from R by defining r(&alpha;)<sub>i</sub> = (r&alpha;)<sub>i</sub> for all i.". <br> In [Lang] p. 128, the definition of the direct sum of left modules is based on direct sums of abelian groups ("We define on [the direct sum of abelian groups M<sub>i</sub>] M a structure of A-module: If (x<sub>i</sub>)<sub>i &isin; I</sub> is an element of M, i.e. a familiy of elements x<sub>i</sub> &isin; M<sub>i</sub> such that x<sub>i</sub> = 0 for almost all i, and if a &isin; A, then we define a(x<sub>i</sub>)<sub>i &isin; I</sub> = (ax<sub>i</sub>)<sub>i &isin; I</sub>, that is we define multiplication by a componentwise.") which itself is based on the direct product of abelian groups ([Lang] p. 36: "Let {A<sub>i</sub>}<sub>i &isin; I</sub> be a family of abelian groups. We define their direct sum A ... to be the subset of the direct product ... consisting of all families (x<sub>i</sub>)<sub>i &isin; I</sub> with x<sub>i</sub> &isin; A<sub>i</sub> such that x<sub>i</sub> = 0 for all but a finite number of indices i"). <br> In short, the <b>direct sum</b> of a familiy of (left) modules {M<sub>i</sub>}<sub>i &isin; I</sub> is the restriction of the direct product of {M<sub>i</sub>}<sub>i &isin; I</sub> to the elements with index function having finite support, as formalized by the definition df-dsmm.

  1. cdsmm
  2. df-dsmm
  3. reldmdsmm
  4. dsmmval
  5. dsmmbase
  6. dsmmval2
  7. dsmmbas2
  8. dsmmfi
  9. dsmmelbas
  10. dsmm0cl
  11. dsmmacl
  12. prdsinvgd2
  13. dsmmsubg
  14. dsmmlss
  15. dsmmlmod