/[mojave]/metaprl/theories/czf/czf_itt_hom.mli
ViewVC logotype

Log of /metaprl/theories/czf/czf_itt_hom.mli

Parent Directory Parent Directory | Revision Log Revision Log


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: 1469 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: 1046 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: 917 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

  ViewVC Help
Powered by ViewVC 1.1.26