605: Finite Direct Product of Groups Is 'Groups - Homomorphisms' Isomorphic to Direct Product of Corresponding Isomorphic Groups|T.B.P.

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

description/proof of that finite direct product of groups is 'groups - homomorphisms' isomorphic to direct product of corresponding isomorphic groups

Topics

About: group

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 {the groups}

G_{1} \times . . . \times G_{n}

= the direct product

{G_{1}^{'}, . . ., G_{n}^{'}}

\subseteq {the groups}

G_{1}^{'} \times . . . \times G_{n}^{'}

= the direct product

{f_{1}, . . ., f_{n}}

f_{j} : G_{j} \to G_{j}^{'} \in {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 {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