description/proof of that finite direct product of groups is 'groups - homomorphisms' isomorphic to direct product of corresponding isomorphic groups
Topics
About: group
The table of contents of this article
- Starting Context
- Target Context
- Orientation
- Main Body
- 1: Structured Description
- 2: Natural Language Description
- 3: Proof
Starting Context
- The reader knows a definition of direct product of structures.
- The reader knows a definition of %category name% isomorphism.
- The reader admits the proposition that any bijective group homomorphism is a 'groups - homomorphisms' isomorphism.
Target Context
- The reader will have a description and a proof of the proposition that any finite direct product of groups is 'groups - homomorphisms' isomorphic to the direct product of any corresponding isomorphic groups.
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:
\(\{G_1, ..., G_n\}\): \(\subseteq \{\text{ the groups }\}\)
\(G_1 \times ... \times G_n\): \(= \text{ the direct product }\)
\(\{G'_1, ..., G'_n\}\): \(\subseteq \{\text{ the groups }\}\)
\(G'_1 \times ... \times G'_n\): \(= \text{ the direct product }\)
\(\{f_1, ..., f_n\}\): \(f_j: G_j \to G'_j \in \{\text{ the 'groups - homomorphisms' isomorphisms }\}\)
\(f\): \(: G_1 \times ... \times G_n \to G'_1 \times ... \times G'_n, (p_1, ..., p_n) \mapsto (f_1 (p_1), ..., f_n (p_n))\)
//
Statements:
\(f \in \{\text{ the 'groups - homomorphisms' isomorphisms }\}\)
//
2: Natural Language Description
For any groups, \(G_1, ..., G_n\), the direct product, \(G_1 \times ... \times G_n\), any groups, \(G'_1, ..., G'_n\), such that there is a 'groups - homomorphisms' isomorphism, \(f_j: G_j \to G'_j\), and the direct product, \(G'_1 \times ... \times G'_n\), \(f: G_1 \times ... \times G_n \to G'_1 \times ... \times G'_n, (p_1, ..., p_n) \mapsto (f_1 (p_1), ..., f_n (p_n))\) is a 'groups - homomorphisms' isomorphism.
3: Proof
\(f\) is bijective, because for each \((p_1, ..., p_n) \neq (p'_1, ..., p'_n) \in G_1 \times ... \times G_n\), \(p_k \neq p'_k\) for a \(k\), and \(f_k (p_k) \neq f_k (p'_k)\); for each \((p'_1, ..., p'_n) \in G'_1 \times ... \times G'_n\), there is the \((p_1, ..., p_n) \in G_1 \times ... \times G_n\) such that \((f_1 (p_1), ..., f_n (p_n)) = (p'_1, ..., p'_n)\), because \(f_j\) is bijective.
Let us prove that \(f\) is a group homomorphism. \(f ((1, ..., 1)) = (f_1 (1), ..., f_n (1)) = (1, ..., 1)\), which is the identity element of \(G'_1 \times ... \times G'_n\). \(f ((p_1, ..., p_n) (p'_1, ..., p'_n)) = f ((p_1 p'_1, ..., p_n p'_n)) = (f_1 (p_1 p'_1), ..., f_n (p_n p'_n)) = (f_1 (p_1) f_1 (p'_1), ..., f_n (p_n) f_n (p'_n)) = (f_1 (p_1), ..., f_n (p_n)) (f_1 (p'_1), ..., f_n (p'_n)) = f ((p_1, ..., p_n)) f ((p'_1, ..., p'_n))\). \(f ((p_1, ..., p_n)^{-1}) = f ((p_1^{-1}, ..., p_n^{-1})) = (f_1 (p_1^{-1}), ..., f_n (p_n^{-1})) = (f_1 (p_1)^{-1}, ..., f_n (p_n)^{-1}) = (f_1 (p_1), ..., f_n (p_n))^{-1} = f ((p_1, ..., p_n))^{-1}\). So, \(f\) is a group homomorphism.
\(f\) is a 'groups - homomorphisms' isomorphism, by the proposition that any bijective group homomorphism is a 'groups - homomorphisms' isomorphism.
