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 \vert j \in J\}\): \(\subseteq \{\text{ the } R \text{ modules }\}\)
\(*\times_{j \in J} M_j\): \(= \text{ the product set }\), \(\in \{\text{ the } R \text{ modules }\}\), with the operations specified below
//
Conditions:
\(\forall r \in R, \forall f \in \times_{j \in J} M_j (\forall j \in J ((r f) (j) = r (f (j))))\)
\(\land\)
\(\forall f, f' \in \times_{j \in J} M_j (\forall j \in J ((f + f') (j) = f (j) + f' (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 }\}\)
\(*M_1 \times ... \times M_k\): \(= \text{ the product set }\), \(\in \{\text{ the } R \text{ modules }\}\), with the operations specified below
//
Conditions:
\(\forall r \in R, \forall m = (m_1, ..., m_k) \in M_1 \times ... \times M_k (r m = (r m_1, ..., r m_k))\)
\(\land\)
\(\forall m = (m_1, ..., m_k), m' = (m'_1, ..., m'_k) \in M_1 \times ... \times M_k (m + m' = (m_1 + m'_1, ..., m_k + m'_k))\)
//
3: Note
Let us see that \(\times_{j \in J} M_j\) is indeed an \(M\) module.
1) \(\forall m, m' \in \times_{j \in J} M_j (m + m' \in \times_{j \in J} M_j)\) (closed-ness under addition): for each \(j \in J\), \((m + m') (j) = m (j) + m' (j) \in M_j\).
2) \(\forall m, m' \in \times_{j \in J} M_j (m + m' = m' + m)\) (commutativity of addition): for each \(j \in J\), \((m + m') (j) = m (j) + m' (j) = m' (j) + m (j) = (m' + m) (j)\).
3) \(\forall m, m', m'' \in \times_{j \in J} M_j ((m + m') + m'' = m + (m' + m''))\) (associativity of additions); for each \(j \in J\), \(((m + m') + m'') (j) = (m + m') (j) + m'' (j) = m (j) + m' (j) + m'' (j) = m (j) + (m' + m'') (j) = (m + (m' + m'')) (j)\).
4) \(\exists 0 \in \times_{j \in J} M_j (\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) \(\forall m \in \times_{j \in J} M_j (\exists m' \in \times_{j \in J} M_j (m' + m = 0))\) (existence of inverse element): \(m' \in \times_{j \in J} M_j\) such that for each \(j \in J\), \(m' (j) = - m (j)\) is such a one, because \((m' + m) (j) = m' (j) + m (j) = - m (j) + m (j) = 0 = m_0 (j)\).
6) \(\forall m \in \times_{j \in J} M_j, \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) = r m (j) \in M_j\).
7) \(\forall m \in \times_{j \in J} M_j, \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) \(\forall m, m' \in \times_{j \in J} M_j, \forall r \in R (r . (m + m') = r . m + r . m')\) (scalar multiplication distributability for elements addition): for each \(j \in J\), \((r . (m + m')) (j) = r (m + m') (j) = r (m (j) + m' (j)) = r m (j) + r m' (j) = (r m) (j) + (r m') (j) = (r . m + r . m') (j)\).
9) \(\forall m \in \times_{j \in J} M_j, \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) \(\forall m \in \times_{j \in J} M_j (1 . m = m)\) (identity of 1 multiplication): for each \(j \in J\), \((1 . m) (j) = 1 m (j) = m (j)\).
Let us see that \(M_1 \times ... \times M_k\) is indeed an \(R\) module.
1) \(\forall m, m' \in M_1 \times ... \times M_k (m + m' \in M_1 \times ... \times M_k)\) (closed-ness under addition): for \(m = (m_1, ..., m_k)\) and \(m' = (m'_1, ..., m'_k)\), \(m + m' = (m_1, ..., m_k) + (m'_1, ..., m'_k) = (m_1 + m'_1, ..., m_k + m'_k) \in M_1 \times ... \times M_k\).
2) \(\forall m, m' \in M_1 \times ... \times M_k (m + m' = m' + m)\) (commutativity of addition): for \(m = (m_1, ..., m_k)\) and \(m' = (m'_1, ..., m'_k)\), \(m + m' = (m_1, ..., m_k) + (m'_1, ..., m'_k) = (m_1 + m'_1, ..., m_k + m'_k) = (m'_1 + m_1, ..., m'_k + m_k) = m' + m\).
3) \(\forall m, m', m'' \in M_1 \times ... \times M_k ((m + m') + m'' = m + (m' + m''))\) (associativity of additions); for \(m = (m_1, ..., m_k)\), \(m' = (m'_1, ..., m'_k)\), and \(m'' = (m''_1, ..., m''_k)\), \((m + m') + m'' = (m_1 + m'_1, ..., m_k + m'_k) + (m''_1, ..., m''_k) = (m_1 + m'_1 + m''_1, ..., m_k + m'_k + m''_k) = m + (m'_1 + m''_1, ..., m'_k + m''_k) = m + (m' + m'')\).
4) \(\exists 0 \in M_1 \times ... \times M_k (\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) \(\forall m \in M_1 \times ... \times M_k (\exists m' \in M_1 \times ... \times M_k (m' + m = 0))\) (existence of inverse element): \(m' \in M_1 \times ... \times M_k\) such that for \(m = (m_1, ..., m_k)\), \(m' = (- m_1, ..., - m_k)\) is such a one, because \(m' + m = (- m_1, ..., - m_k) + (m_1, ..., m_k) = (- m_1 + m_1, ..., - m_k + m_k) = (0, ..., 0) = m_0\).
6) \(\forall m \in M_1 \times ... \times M_k, \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) \(\forall m \in M_1 \times ... \times M_k, \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) \(\forall m, m' \in M_1 \times ... \times M_k, \forall r \in R (r . (m + m') = r . m + r . m')\) (scalar multiplication distributability for elements addition): for \(m = (m_1, ..., m_k)\) and \(m' = (m'_1, ..., m'_k)\), \(r . (m + m') = r (m_1 + m'_1, ..., m_k + m'_k) = (r (m_1 + m'_1), ..., r (m_k + m'_k)) = (r m_1 + r m'_1, ..., r m_k + r m'_k) = (r m_1, ..., r m_k) + (r m'_1, ..., r m'_k) = r . m + r . m'\).
9) \(\forall m \in M_1 \times ... \times M_k, \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) \(\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) = (1 m_1, ..., 1 m_k) = (m_1, ..., m_k) = m\).
