|
11443
|
1 |
<!-- $Id$ -->
|
|
|
2 |
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
|
|
|
3 |
|
|
|
4 |
<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
|
|
|
5 |
|
|
|
6 |
<P>This directory presents proofs about group theory, by
|
|
|
7 |
Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.)
|
|
|
8 |
These theories use locales and were indeed the original motivation for
|
|
|
9 |
locales. However, this treatment of groups must still be regarded as
|
|
|
10 |
experimental. We can expect to see refinements in the future.
|
|
|
11 |
|
|
|
12 |
Here is an outline of the directory's contents:
|
|
|
13 |
|
|
|
14 |
<UL>
|
|
|
15 |
<LI>Theory <A HREF="Bij.thy"><CODE>Bij</CODE></A>
|
|
|
16 |
defines bijections over sets and operations on them and shows that they
|
|
|
17 |
are a group.
|
|
|
18 |
|
|
|
19 |
<LI>Theory <A HREF="DirProd.thy"><CODE>DirProd</CODE></A>
|
|
|
20 |
defines the product of two groups and proves that it is a group again.
|
|
|
21 |
|
|
|
22 |
<LI>Theory <A HREF="FactGroup.thy"><CODE>FactGroup</CODE></A>
|
|
|
23 |
defines the factorization of a group and shows that the factorization a
|
|
|
24 |
normal subgroup is a group.
|
|
|
25 |
|
|
|
26 |
<LI>Theory <A HREF="Homomorphism.thy"><CODE>Homomorphism</CODE></A>
|
|
|
27 |
defines homomorphims and automorphisms for groups and rings and shows that
|
|
|
28 |
ring automorphisms are a group by using the previous result for
|
|
|
29 |
bijections.
|
|
|
30 |
|
|
|
31 |
<LI>Theory <A HREF="Ring.thy"><CODE>Ring</CODE></A>
|
|
|
32 |
and <A HREF="RingConstr.thy"><CODE>RingConstr</CODE></A>
|
|
|
33 |
defines rings, proves a few basic theorems and constructs a lambda
|
|
|
34 |
function to extract the group that is part of the ring showing that it is
|
|
|
35 |
an abelian group.
|
|
|
36 |
|
|
|
37 |
<LI>Theory <A HREF="Sylow.thy"><CODE>Sylow</CODE></A>
|
|
|
38 |
contains a proof of the first Sylow theorem.
|
|
|
39 |
|
|
|
40 |
</UL>
|
|
|
41 |
|
|
|
42 |
<HR>
|
|
|
43 |
<P>Last modified on $Date$
|
|
|
44 |
|
|
|
45 |
<ADDRESS>
|
|
|
46 |
<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
|
|
|
47 |
</ADDRESS>
|
|
|
48 |
</BODY></HTML>
|