/[mojave]/metaprl/theories/czf/czf_itt_hom.prla # Log of /metaprl/theories/czf/czf_itt_hom.prla

 Links to HEAD: (view) (download) (annotate) Sticky Revision:

Revision 3573 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 9 06:02:02 2002 UTC (19 years, 2 months ago) by xiny
File length: 483192 byte(s)
Diff to previous 3559
```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.

```

Revision 3559 - (view) (download) (annotate) - [select for diffs]
Modified Tue Apr 2 08:46:33 2002 UTC (19 years, 2 months ago) by xiny
File length: 193681 byte(s)
Diff to previous 3547
```Changed def of homomorphisms and reproved all rules;
Added tactics "homIdT" and "homInvT".

Not finished yet. Will do the rest after fixing errors in subgroups
and cylic subgroups.

```

Revision 3547 - (view) (download) (annotate) - [select for diffs]
Added Sun Mar 24 08:26:30 2002 UTC (19 years, 3 months ago) by xiny
File length: 146820 byte(s)
```Defined homomorphism for groups. A map f of a group G into a group G'
is a homomorphism if f(a * b) = f(a) * f(b).

Proved some properties of homomorphism with the definition.

Since I would redo groups soon, this homomorphism file is not complete.

```

This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

 Diffs between and Type of Diff should be a Colored Diff Long Colored Diff Full Colored Diff Unidiff Context Diff Side by Side

 ViewVC Help Powered by ViewVC 1.1.26