945: Product Module

<The previous article in this series | The table of contents of this series | The next article in this series>

definition of product module

---

Topics

About: module

---

The table of contents of this article

• Starting Context
• Target Context
• Orientation
• Main Body
• 1: Structured Description 1
• 2: Structured Description 2
• 3: Note

---

Starting Context

• The reader knows a definition of %ring name% module.
• The reader knows a definition of product set.

---

Target Context

• The reader will have a definition of product module.

---

Orientation

There is a list of definitions discussed so far in this site.

There is a list of propositions discussed so far in this site.

---

Main Body

---

1: Structured Description 1

Here is the rules of Structured Description.

Entities:
$J$: $\in \{\text{ the possibly uncountable index sets }\}$
$R$: $\in \{\text{ the rings }\}$
$\{M_j|j\in J\}$: $\subseteq \{\text{ the }R\text{ modules }\}$
$\ast {\times }_{j\in J}{M}_j$: $=\text{ the product set }$, $\in \{\text{ the }R\text{ modules }\}$, with the operations specified below
//

Conditions:
$\mathrm{\forall }r\in R,\mathrm{\forall }f\in {\times }_{j\in J}{M}_j(\mathrm{\forall }j\in J((rf)(j)=r(f(j))))$
$\wedge$
$\mathrm{\forall }f,f^{\prime }\in {\times }_{j\in J}{M}_j(\mathrm{\forall }j\in J((f+f^{\prime })(j)=f(j)+f^{\prime }(j)))$
//

---

2: Structured Description 2

Here is the rules of Structured Description.

Entities:
$R$: $\in \{\text{ the rings }\}$
$\{M_1,...,M_k\}$: $\subseteq \{\text{ the }R\text{ modules }\}$
$\ast M_1\times ...\times M_k$: $=\text{ the product set }$, $\in \{\text{ the }R\text{ modules }\}$, with the operations specified below
//

Conditions:
$\mathrm{\forall }r\in R,\mathrm{\forall }m=(m_1,...,m_k)\in M_1\times ...\times M_k(rm=(r{m}_1,...,r{m}_k))$
$\wedge$
$\mathrm{\forall }m=(m_1,...,m_k),m^{\prime }=(m_1^{\prime },...,m_k^{\prime })\in M_1\times ...\times M_k(m+m^{\prime }=(m_1+m_1^{\prime },...,m_k+m_k^{\prime }))$
//

---

3: Note

Let us see that ${\times }_{j\in J}{M}_j$ is indeed an $M$ module.

1) $\mathrm{\forall }m,m^{\prime }\in {\times }_{j\in J}{M}_j(m+m^{\prime }\in {\times }_{j\in J}{M}_j)$ (closed-ness under addition): for each $j\in J$, $(m+m^{\prime })(j)=m(j)+m^{\prime }(j)\in M_j$.

2) $\mathrm{\forall }m,m^{\prime }\in {\times }_{j\in J}{M}_j(m+m^{\prime }=m^{\prime }+m)$ (commutativity of addition): for each $j\in J$, $(m+m^{\prime })(j)=m(j)+m^{\prime }(j)=m^{\prime }(j)+m(j)=(m^{\prime }+m)(j)$.

3) $\mathrm{\forall }m,m^{\prime },m^{″}\in {\times }_{j\in J}{M}_j((m+m^{\prime })+m^{″}=m+(m^{\prime }+m^{″}))$ (associativity of additions); for each $j\in J$, $((m+m^{\prime })+m^{″})(j)=(m+m^{\prime })(j)+m^{″}(j)=m(j)+m^{\prime }(j)+m^{″}(j)=m(j)+(m^{\prime }+m^{″})(j)=(m+(m^{\prime }+m^{″}))(j)$.

4) $\mathrm{\exists }0\in {\times }_{j\in J}{M}_j(\mathrm{\forall }m\in {\times }_{j\in J}{M}_j(m+0=m))$ (existence of 0 element): $m_0\in {\times }_{j\in J}{M}_j$ such that for each $j\in J$, $m_0(j)=0$ is $0$, because $(m+m_0)(j)=m(j)+m_0(j)=m(j)+0=m(j)$.

5) $\mathrm{\forall }m\in {\times }_{j\in J}{M}_j(\mathrm{\exists }{m}^{\prime }\in {\times }_{j\in J}{M}_j(m^{\prime }+m=0))$ (existence of inverse element): $m^{\prime }\in {\times }_{j\in J}{M}_j$ such that for each $j\in J$, $m^{\prime }(j)=-m(j)$ is such a one, because $(m^{\prime }+m)(j)=m^{\prime }(j)+m(j)=-m(j)+m(j)=0=m_0(j)$.

6) $\mathrm{\forall }m\in {\times }_{j\in J}{M}_j,\mathrm{\forall }r\in R(r.m\in {\times }_{j\in J}{M}_j)$ (closed-ness under scalar multiplication): for each $j\in J$, $(r.m)(j)=rm(j)\in M_j$.

7) $\mathrm{\forall }m\in {\times }_{j\in J}{M}_j,\mathrm{\forall }{r}_1,r_2\in R((r_1+r_2).m=r_1.m+r_2.m)$ (scalar multiplication distributability for scalars addition): for each $j\in J$, $((r_1+r_2).m)(j)=(r_1+r_2)m(j)=r_{1}m(j)+r_{2}m(j)=(r_{1}m)(j)+(r_{2}m)(j)=(r_1.m+r_2.m)(j))$.

8) $\mathrm{\forall }m,m^{\prime }\in {\times }_{j\in J}{M}_j,\mathrm{\forall }r\in R(r.(m+m^{\prime })=r.m+r.m^{\prime })$ (scalar multiplication distributability for elements addition): for each $j\in J$, $(r.(m+m^{\prime }))(j)=r(m+m^{\prime })(j)=r(m(j)+m^{\prime }(j))=rm(j)+r{m}^{\prime }(j)=(rm)(j)+(r{m}^{\prime })(j)=(r.m+r.m^{\prime })(j)$.

9) $\mathrm{\forall }m\in {\times }_{j\in J}{M}_j,\mathrm{\forall }{r}_1,r_2\in R((r_1{r}_2).m=r_1.(r_2.m))$ (associativity of scalar multiplications): for each $j\in J$, $((r_1{r}_2).m)(j)=(r_1{r}_2)m(j)=r_1(r_{2}m(j))=r_1.(r_2.m)(j)$.

10) $\mathrm{\forall }m\in {\times }_{j\in J}{M}_j(1.m=m)$ (identity of 1 multiplication): for each $j\in J$, $(1.m)(j)=1m(j)=m(j)$.

Let us see that $M_1\times ...\times M_k$ is indeed an $R$ module.

1) $\mathrm{\forall }m,m^{\prime }\in M_1\times ...\times M_k(m+m^{\prime }\in M_1\times ...\times M_k)$ (closed-ness under addition): for $m=(m_1,...,m_k)$ and $m^{\prime }=(m_1^{\prime },...,m_k^{\prime })$, $m+m^{\prime }=(m_1,...,m_k)+(m_1^{\prime },...,m_k^{\prime })=(m_1+m_1^{\prime },...,m_k+m_k^{\prime })\in M_1\times ...\times M_k$.

2) $\mathrm{\forall }m,m^{\prime }\in M_1\times ...\times M_k(m+m^{\prime }=m^{\prime }+m)$ (commutativity of addition): for $m=(m_1,...,m_k)$ and $m^{\prime }=(m_1^{\prime },...,m_k^{\prime })$, $m+m^{\prime }=(m_1,...,m_k)+(m_1^{\prime },...,m_k^{\prime })=(m_1+m_1^{\prime },...,m_k+m_k^{\prime })=(m_1^{\prime }+m_1,...,m_k^{\prime }+m_k)=m^{\prime }+m$.

3) $\mathrm{\forall }m,m^{\prime },m^{″}\in M_1\times ...\times M_k((m+m^{\prime })+m^{″}=m+(m^{\prime }+m^{″}))$ (associativity of additions); for $m=(m_1,...,m_k)$, $m^{\prime }=(m_1^{\prime },...,m_k^{\prime })$, and $m^{″}=(m_1^{″},...,m_k^{″})$, $(m+m^{\prime })+m^{″}=(m_1+m_1^{\prime },...,m_k+m_k^{\prime })+(m_1^{″},...,m_k^{″})=(m_1+m_1^{\prime }+m_1^{″},...,m_k+m_k^{\prime }+m_k^{″})=m+(m_1^{\prime }+m_1^{″},...,m_k^{\prime }+m_k^{″})=m+(m^{\prime }+m^{″})$.

4) $\mathrm{\exists }0\in M_1\times ...\times M_k(\mathrm{\forall }m\in M_1\times ...\times M_k(m+0=m))$ (existence of 0 element): $m_0\in M_1\times ...\times M_k$ such that $m_0=(0,...,0)$ is $0$, because for $m=(m_1,...,m_k)$, $m+m_0=(m_1,...,m_k)+(0,...,0)=(m_1+0,...,m_k+0)=(m_1,...,m_k)=m$.

5) $\mathrm{\forall }m\in M_1\times ...\times M_k(\mathrm{\exists }{m}^{\prime }\in M_1\times ...\times M_k(m^{\prime }+m=0))$ (existence of inverse element): $m^{\prime }\in M_1\times ...\times M_k$ such that for $m=(m_1,...,m_k)$, $m^{\prime }=(-m_1,...,-m_k)$ is such a one, because $m^{\prime }+m=(-m_1,...,-m_k)+(m_1,...,m_k)=(-m_1+m_1,...,-m_k+m_k)=(0,...,0)=m_0$.

6) $\mathrm{\forall }m\in M_1\times ...\times M_k,\mathrm{\forall }r\in R(r.m\in M_1\times ...\times M_k)$ (closed-ness under scalar multiplication): for $m=(m_1,...,m_k)$, $r.m=(r{m}_1,...,r{m}_k)\in M_j$.

7) $\mathrm{\forall }m\in M_1\times ...\times M_k,\mathrm{\forall }{r}_1,r_2\in R((r_1+r_2).m=r_1.m+r_2.m)$ (scalar multiplication distributability for scalars addition): for $m=(m_1,...,m_k)$, $(r_1+r_2).m=((r_1+r_2)m_1,...,(r_1+r_2)m_k)=(r_1{m}_1+r_2{m}_1,...,r_1{m}_k+r_2{m}_k)=(r_1{m}_1,...,r_1{m}_k)+(r_2{m}_1,...,r_2{m}_k)=r_1.m+r_2.m)$.

8) $\mathrm{\forall }m,m^{\prime }\in M_1\times ...\times M_k,\mathrm{\forall }r\in R(r.(m+m^{\prime })=r.m+r.m^{\prime })$ (scalar multiplication distributability for elements addition): for $m=(m_1,...,m_k)$ and $m^{\prime }=(m_1^{\prime },...,m_k^{\prime })$, $r.(m+m^{\prime })=r(m_1+m_1^{\prime },...,m_k+m_k^{\prime })=(r(m_1+m_1^{\prime }),...,r(m_k+m_k^{\prime }))=(r{m}_1+r{m}_1^{\prime },...,r{m}_k+r{m}_k^{\prime })=(r{m}_1,...,r{m}_k)+(r{m}_1^{\prime },...,r{m}_k^{\prime })=r.m+r.m^{\prime }$.

9) $\mathrm{\forall }m\in M_1\times ...\times M_k,\mathrm{\forall }{r}_1,r_2\in R((r_1{r}_2).m=r_1.(r_2.m))$ (associativity of scalar multiplications): for $m=(m_1,...,m_k)$, $(r_1{r}_2).m=(r_1{r}_2)(m_1,...,m_k)=(r_1{r}_2{m}_1,...,r_1{r}_2{m}_k)=r_1(r_2{m}_1,...,r_2{m}_k)=r_1.(r_2.m)$.

10) $\mathrm{\forall }m\in M_1\times ...\times M_k(1.m=m)$ (identity of 1 multiplication): for $m=(m_1,...,m_k)$, $1.m=1(m_1,...,m_k)=(1m_1,...,1m_k)=(m_1,...,m_k)=m$.

---

References

<The previous article in this series | The table of contents of this series | The next article in this series>