Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2002-04-08 23:02:02 -0700 (Mon, 08 Apr 2002)
Revision: 3573
Log message:
1. Defined kernels using "hom" and "group_bvd":
f is a homomorphism of g1 into g2. The elements of g1,
which are mapped into the identity of g2, form a subgroup
h of g called the kernel of f.
2. Added and proved the following properties of homomorphisms:
i. Let f: G -> G' be a group homomorphism of G into G'.
If H is a subgroup of G, then f[H] is a subgroup of G'.
ii. Let f: G -> G' be a group homomorphism of G into G'.
If H is a subgroup of G', then the inverse image of
H is a subgroup of G.
3. Added and proved the following properties of kernels:
i. Let f: G -> G' be a group homomorphism of G into G'.
The kernel of f is a subgroup of G.
ii. Let f: G1 -> G2 be a group homomorphism of G1 into G2.
Let H be the kernel of f. For any a in G1, the set
{ x in G1 | f(x) = f(a) } is the left coset aH of H.
iii.Let f: G1 -> G2 be a group homomorphism of G1 into G2.
Let H be the kernel of f. For any a in G1, the set
{ x in G1 | f(x) = f(a) } is also the right coset Ha of H.
iv. A group homomorphism f: G1 -> G2 is a one-to-one map
if and only if Ker(f) = {id(g1)}.
v. The kernel of a homomorphism f: G1 -> G2 is a normal
subgroup of G1.
Tactics:
kernelSubgroupT, kernelLcosetT, kernelRcosetT, kernelNormalSubgT
Note:
The property that "A group homomorphism f: G1 -> G2 is a one-to-
one map if and only if Ker(f) = {id(g1)}." can also be written
into a tactics when necessary.
Changes | Path |
+168 -2 | metaprl/theories/czf/czf_itt_hom.ml |
+9 -1 | metaprl/theories/czf/czf_itt_hom.mli |
+12050 -822 | metaprl/theories/czf/czf_itt_hom.prla |