paulson@7998

1 
<! $Id$ >

paulson@7998

2 
<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>

paulson@7998

3 

paulson@7998

4 
<H2>Algebra: Theories of Rings and Polynomials</H2>

paulson@7998

5 

paulson@7998

6 
<P>This development of univariate polynomials is separated into an

paulson@7998

7 
abstract development of rings and the development of polynomials

paulson@7998

8 
itself. The formalisation is based on [Jacobson1985], and polynomials

paulson@7998

9 
have a sparse, mathematical representation. These theories were

paulson@7998

10 
developed as a base for the integration of a computer algebra system

paulson@7998

11 
to Isabelle [Ballarin1999], and was designed to match implementations

paulson@7998

12 
of these domains in some typed computer algebra systems. Summary:

paulson@7998

13 

paulson@7998

14 
<P><EM>Rings:</EM>

paulson@7998

15 
Classes of rings are represented by axiomatic type classes. The

paulson@7998

16 
following are available:

paulson@7998

17 

paulson@7998

18 
<PRE>

paulson@7998

19 
ringS: Syntactic class

paulson@7998

20 
ring: Commutative rings with one (including a summation

paulson@7998

21 
operator, which is needed for the polynomials)

paulson@7998

22 
domain: Integral domains

paulson@7998

23 
factorial: Factorial domains (divisor chain condition is missing)

paulson@7998

24 
pid: Principal ideal domains

paulson@7998

25 
field: Fields

paulson@7998

26 
</PRE>

paulson@7998

27 

paulson@7998

28 
Also, some facts about ring homomorphisms and ideals are mechanised.

paulson@7998

29 

paulson@7998

30 
<P><EM>Polynomials:</EM>

paulson@7998

31 
Polynomials have a natural, mathematical representation. Facts about

paulson@7998

32 
the following topics are provided:

paulson@7998

33 

paulson@7998

34 
<MENU>

paulson@7998

35 
<LI>Degree function

paulson@7998

36 
<LI> Universal Property, evaluation homomorphism

paulson@7998

37 
<LI>Long division (existence and uniqueness)

paulson@7998

38 
<LI>Polynomials over a ring form a ring

paulson@7998

39 
<LI>Polynomials over an integral domain form an integral domain

paulson@7998

40 
</MENU>

paulson@7998

41 

paulson@7998

42 
<P>Still missing are

paulson@7998

43 
Polynomials over a factorial domain form a factorial domain

paulson@7998

44 
(difficult), and polynomials over a field form a pid.

paulson@7998

45 

paulson@7998

46 
<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.

paulson@7998

47 

paulson@7998

48 
<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,

paulson@7998

49 
Author's <A HREF="http://iakswww.ira.uka.de/iakscalmet/ballarin/publications.html">PhD thesis</A>, 1999.

paulson@7998

50 

paulson@13944

51 
<H2>GroupTheory  Group Theory using Locales, including Sylow's Theorem</H2>

paulson@13944

52 

paulson@13944

53 
<P>This directory presents proofs about group theory, by

paulson@13944

54 
Florian Kammüller. (Later, Larry Paulson simplified some of the proofs.)

paulson@13944

55 
These theories use locales and were indeed the original motivation for

paulson@13944

56 
locales. However, this treatment of groups must still be regarded as

paulson@13944

57 
experimental. We can expect to see refinements in the future.

paulson@13944

58 

paulson@13944

59 
Here is an outline of the directory's contents:

paulson@13944

60 

paulson@13944

61 
<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines

paulson@13944

62 
semigroups, groups, homomorphisms and the subgroup relation. It also defines

paulson@13944

63 
the product of two groups. It defines the factorization of a group and shows

paulson@13944

64 
that the factorization a normal subgroup is a group.

paulson@13944

65 

paulson@13944

66 
<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>

paulson@13944

67 
defines bijections over sets and operations on them and shows that they

paulson@13944

68 
are a group. It shows that automorphisms form a group.

paulson@13944

69 

paulson@13944

70 
<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves

paulson@13944

71 
a few basic theorems. Ring automorphisms are shown to form a group.

paulson@13944

72 

paulson@13944

73 
<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>

paulson@13944

74 
contains a proof of the first Sylow theorem.

paulson@13944

75 

paulson@13944

76 
<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends

paulson@13944

77 
abelian groups by a summation operator for finite sets (provided by

paulson@13944

78 
Clemens Ballarin).

paulson@13944

79 
</UL>

paulson@13944

80 

paulson@7998

81 
<HR>

paulson@7998

82 
<P>Last modified on $Date$

paulson@7998

83 

paulson@7998

84 
<ADDRESS>

paulson@7998

85 
<P><A HREF="http://iakswww.ira.uka.de/iakscalmet/ballarin">Clemens Ballarin</A>. Karlsruhe, October 1999

paulson@7998

86 

paulson@7998

87 
<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>

paulson@7998

88 
</ADDRESS>

paulson@7998

89 
</BODY></HTML>
