description/proof of that injective group homomorphism is 'groups - homomorphisms' isomorphism onto range
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 group.
- The reader knows a definition of Injection.
- The reader knows a definition of %structure kind name% homomorphism.
- The reader knows a definition of %category name% isomorphism.
- The reader admits the proposition that for any group homomorphism, the range of the homomorphism is a subgroup of the codomain.
- 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 injective group homomorphism is a 'groups - homomorphisms' isomorphism onto the range of the homomorphism.
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\): \(\in \{\text{ the groups }\}\)
\(G_2\): \(\in \{\text{ the groups }\}\)
\(f\): \(G_1 \to G_2\), \(\in \{\text{ the injections }\} \cap \{\text{ the group homomorphisms }\}\)
\(f'\): \(G_1 \to f (G_1)\), \(g \mapsto f (g)\)
//
Statements:
\(f (G_1) \in \{\text{ the subgroups of } G_2\}\)
\(\land\)
\(f' \in \{\text{ the 'groups - homomorphisms' isomorphisms }\}\)
//
2: Natural Language Description
For any groups, \(G_1, G_2\), and any injective group homomorphism, \(f: G_1 \to G_2\), \(f (G_1) \subseteq G_2\) is a subgroup of \(G_2\) and \(f': G_1 \to f (G_1)\) is a 'groups - homomorphisms' isomorphism.
3: Proof
\(f (G_1)\) is a subgroup of \(G_2\), by the proposition that for any group homomorphism, the range of the homomorphism is a subgroup of the codomain.
\(f'\) is a bijective group homomorphism.
So, \(f'\) is a 'groups - homomorphisms' isomorphism, by the proposition that any bijective group homomorphism is a 'groups - homomorphisms' isomorphism.
