src/HOL/Algebra/README.html
author paulson
Thu, 01 May 2003 11:54:18 +0200
changeset 13944 9b34607cd83e
parent 7998 3d0c34795831
child 13949 0ce528cd6f19
permissions -rw-r--r--
new proofs about direct products, etc.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7998
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     1
<!-- $Id$ -->
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     2
<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     3
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     4
<H2>Algebra: Theories of Rings and Polynomials</H2>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     5
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     6
<P>This development of univariate polynomials is separated into an
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     7
abstract development of rings and the development of polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     8
itself. The formalisation is based on [Jacobson1985], and polynomials
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
     9
have a sparse, mathematical representation. These theories were
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    10
developed as a base for the integration of a computer algebra system
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    11
to Isabelle [Ballarin1999], and was designed to match implementations
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    12
of these domains in some typed computer algebra systems.  Summary:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    13
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    14
<P><EM>Rings:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    15
  Classes of rings are represented by axiomatic type classes. The
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    16
  following are available:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    17
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    18
<PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    19
  ringS:	Syntactic class
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    20
  ring:		Commutative rings with one (including a summation
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    21
		operator, which is needed for the polynomials)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    22
  domain:	Integral domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    23
  factorial:	Factorial domains (divisor chain condition is missing)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    24
  pid:		Principal ideal domains
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    25
  field:	Fields
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    26
</PRE>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    27
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    28
  Also, some facts about ring homomorphisms and ideals are mechanised.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    29
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    30
<P><EM>Polynomials:</EM>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    31
  Polynomials have a natural, mathematical representation. Facts about
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    32
  the following topics are provided:
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    33
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    34
<MENU>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    35
<LI>Degree function
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    36
<LI> Universal Property, evaluation homomorphism
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    37
<LI>Long division (existence and uniqueness)
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    38
<LI>Polynomials over a ring form a ring
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    39
<LI>Polynomials over an integral domain form an integral domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    40
</MENU>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    41
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    42
 <P>Still missing are
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    43
    Polynomials over a factorial domain form a factorial domain
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    44
    (difficult), and polynomials over a field form a pid.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    45
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    46
<P>[Jacobson1985] Nathan Jacobson, Basic Algebra I, Freeman, 1985.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    47
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    48
<P>[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving,
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    49
  Author's <A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin/publications.html">PhD thesis</A>, 1999.
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    50
13944
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    51
<H2>GroupTheory -- Group Theory using Locales, including Sylow's Theorem</H2>
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    52
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    53
<P>This directory presents proofs about group theory, by
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    54
Florian Kammüller.  (Later, Larry Paulson simplified some of the proofs.)
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    55
These theories use locales and were indeed the original motivation for
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    56
locales.  However, this treatment of groups must still be regarded as
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    57
experimental.  We can expect to see refinements in the future.
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    58
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    59
Here is an outline of the directory's contents:
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    60
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    61
<UL> <LI>Theory <A HREF="Group.html"><CODE>Group</CODE></A> defines
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    62
semigroups, groups, homomorphisms and the subgroup relation.  It also defines
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    63
the product of two groups.  It defines the factorization of a group and shows
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    64
that the factorization a normal subgroup is a group.
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    65
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    66
<LI>Theory <A HREF="Bij.html"><CODE>Bij</CODE></A>
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    67
defines bijections over sets and operations on them and shows that they
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    68
are a group.  It shows that automorphisms form a group.
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    69
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    70
<LI>Theory <A HREF="Ring.html"><CODE>Ring</CODE></A> defines rings and proves
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    71
a few basic theorems.  Ring automorphisms are shown to form a group.
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    72
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    73
<LI>Theory <A HREF="Sylow.html"><CODE>Sylow</CODE></A>
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    74
contains a proof of the first Sylow theorem.
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    75
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    76
<LI>Theory <A HREF="Summation.html"><CODE>Summation</CODE></A> Extends
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    77
abelian groups by a summation operator for finite sets (provided by
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    78
Clemens Ballarin).
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    79
</UL>
9b34607cd83e new proofs about direct products, etc.
paulson
parents: 7998
diff changeset
    80
7998
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    81
<HR>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    82
<P>Last modified on $Date$
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    83
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    84
<ADDRESS>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    85
<P><A HREF="http://iaks-www.ira.uka.de/iaks-calmet/ballarin">Clemens Ballarin</A>.  Karlsruhe, October 1999
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    86
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    87
<A NAME="ballarin@ira.uka.de" HREF="mailto:ballarin@ira.uka.de">ballarin@ira.uka.de</A>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    88
</ADDRESS>
3d0c34795831 Algebra and Polynomial theories, by Clemens Ballarin
paulson
parents:
diff changeset
    89
</BODY></HTML>