definition of quotient module of module by submodule
Topics
About: module
The table of contents of this article
Starting Context
- The reader knows a definition of %ring name% module.
- The reader knows a definition of quotient set.
Target Context
- The reader will have a definition of quotient module of module by submodule.
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
Here is the rules of Structured Description.
Entities:
\( R\): \(\in \{\text{ the rings }\}\)
\( M'\): \(\in \{\text{ the } R \text{ modules }\}\)
\( M\): \(\in \{\text{ the submodules of } M'\}\)
\( \sim\): \(\in \{\text{ the equivalence relations on } M'\}\), such that \(\forall m'_1, m'_2 \in M' (m'_1 \sim m'_2 \iff m'_1 - m'_2 \in M)\)
\(*M' / M\): \(= M' / \sim\), \(\in \{\text{ the } R \text{ modules }\}\), with the operations specified below
//
Conditions:
\(\forall r \in R, \forall [m_1], [m_2] \in M' / M (r [m_1] = [r m_1] \land [m_1] + [m_2] = [m_1 + m_2])\)
//
2: Note
Let us see that \(M' / M\) is indeed well-defined.
Let us see that \(\sim\) is indeed an equivalence relation on \(M'\).
For each \(m' \in M'\), \(m' \sim m'\), because \(m' - m' = 0 \in M\).
For each \(m'_1, m'_2 \in M'\), \(m'_1 \sim m'_2\) implies that \(m'_2 \sim m'_1\), because as \(m'_1 - m'_2 \in V\), \(m'_2 - m'_1 = - (m'_1 - m'_2) \in M\).
For each \(m'_1, m'_2, m'_3 \in M'\), \(m'_1 \sim m'_2\) and \(m'_2 \sim m'_3\) implies that \(m'_1 \sim m'_3\), because as \(m'_1 - m'_2 \in M\) and \(m'_2 - m'_3 \in M\), \(m'_1 - m'_3 = m'_1 - m'_2 + m'_2 - m'_3 = (m'_1 - m'_2) + (m'_2 - m'_3) \in M\).
So, \(M' / \sim\) is well-defined as a set.
Let us see that the operations are well-defined.
For \(r [m_1] = [r m_1]\), \([r m_1]\) does not depend on the choice of the representative, \(m_1\), because letting \([m_1] = [n_1]\), \(n_1 - m_1 := m \in M\), and \([r n_1] = [r (m_1 + m)] = [r m_1 + r m]\), but \(r m_1 + r m - r m_1 = r m \in M\), so, \([r n_1] = [r m_1]\).
For \([m_1] + [m_2] = [m_1 + m_2]\), \([m_1 + m_2]\) does not depend on the choices of the representatives, \(m_1, m_2\), because letting \([m_1] = [n_1]\) and \([m_2] = [n_2]\), as \(n_1 - m_1, n_2 - m_2 \in M\), \(n_1 + n_2 - (m_1 + m_2) = (n_1 - m_1) + (n_2 - m_2) \in M\), so, \([n_1 + n_2] = [m_1 + m_2]\).
Let us see that \(M' / M\) is indeed an \(R\) module.
1) \(\forall [m_1], [m_2] \in M' / M ([m_1] + [m_2] \in M' / M)\) (closed-ness under addition): \([m_1] + [m_2] = [m_1 + m_2] \in M' / M\).
2) \(\forall [m_1], [m_2] \in M' / M ([m_1] + [m_2] = [m_2] + [m_1])\) (commutativity of addition): \([m_1] + [m_2] = [m_1 + m_2] = [m_2 + m_1] = [m_2] + [m_1]\).
3) \(\forall [m_1], [m_2], [m_3] \in M' / M (([m_1] + [m_2]) + [m_3] = [m_1] + ([m_2] + [m_3]))\) (associativity of additions): \(([m_1] + [m_2]) + [m_3] = ([m_1 + m_2]) + [m_3] = [m_1 + m_2 + m_3] = [m_1] + [m_2 + m_3] = [m_1] + ([m_2] + [m_3])\).
4) \(\exists [0] \in M' / M (\forall [m] \in M' / M ([m] + [0] = [m]))\) (existence of 0 element): \([0] \in M' / M\), and \([m] + [0] = [m + 0] = [m]\).
5) \(\forall [m] \in M' / M (\exists [m'] \in M' / M ([m'] + [m] = [0]))\) (existence of inverse vector): \([m'] := [- m] \in M' / M\), and \([m'] + [m] = [- m] + [m] = [- m + m] = [0]\).
6) \(\forall [m] \in M' / M, \forall r \in R (r . [m] \in M' / M)\) (closed-ness under scalar multiplication): \(r . [m] = [r m] \in M' / M\).
7) \(\forall [m] \in M' / M, \forall r_1, r_2 \in R ((r_1 + r_2) . [m] = r_1 . [m] + r_2 . [m])\) (scalar multiplication distributability for scalars addition): \((r_1 + r_2) . [m] = [(r_1 + r_2) m] = [r_1 m + r_2 m] = [r_1 m] + [r_2 m] = r_1 . [m] + r_2 . [m]\).
8) \(\forall [m_1], [m_2] \in M' / M, \forall r \in R (r . ([m_1] + [m_2]) = r . [m_1] + r . [m_2])\) (scalar multiplication distributability for elements addition): \(r . ([m_1] + [m_2]) = r . [m_1 + m_2] = [r (m_1 + m_2)] = [r m_1 + r m_2] = [r m_1] + [r m_2] = r . [m_1] + r . [m_2]\).
9) \(\forall [m] \in M' / M, \forall r_1, r_2 \in R ((r_1 r_2) . [m] = r_1 . (r_2 . [m]))\) (associativity of scalar multiplications): \((r_1 r_2) . [m] = [(r_1 r_2) m] = [r_1 (r_2 m)] = r_1 . (r_2 . [m])\).
10) \(\forall [m] \in M' / M (1 . [m] = [m])\) (identity of 1 multiplication): \(1 . [m] = [1 m] = [m]\).
