To play this document inside your browser use ALT-N and ALT-P. You can save your edits inside your browser and load them back (edits are also saved when you close the window). Finally you can download the file for offline editing.

The algebra library

  • This is a central part of the mathematical components library.
  • This library register a various range of (mathematical) structures.
    • types with decidable equality: eqType
    • types with a finite number of elements: finType
    • finite groups: finGroupType
    • abelian (not possibly finite) groups: zmodType
    • rings: ringType
    • rings with invertible elements: unitRingType
    • commutative rings: comRingType
    • integral domains: idomainType
    • fields: fieldType
    • left modules: lmodType
    • left algebra: lalgType
    • algebra: algType
    • finite dimensional vector spaces: vectType
    • ...

  • These structures share operators: e.g. the operator (_ + _), introduced for abelian groups (zmodType), is also available for all the structures that inherit it (rings, domains, fields, etc...)

  • All of these structures are discrete: they all have decidable equality: the operator (_ == _) is available on all of them.

  • Here is a picture of the begining of the hierarchy

    Extensive documentation in the header of:

  • In addition there are structures for maps (additive morphisms, ring morphisms, etc...), and substructures (subgroup, subsemiring, subring, subfield, etc...)

  • From math-comp 2.0 alpha, structures are generated by the external tool Hierarchy Builder

Roadmap for the lesson:

  • introduction to HB
  • instantiation of a structure in the library
  • exploration of the theory provided by this structure and naming conventions
  • creation of a algebraic substructure and predicate and their use

Inhabiting the mathematical structures hierarchy.

  • We now show on the example of integers how to instantiate the mathematical structures that integers satisfy.

  • In order to minimize the work of the user, the library lets you inhabit structures by instanciating mixins and factory, one at a time. Each time we want to build structures, we only declare the mixin/factory as an HB.instance. One or several structures will be automatically instantiated.

  • We catagorize five different ways to build structures. Th three first will be shown here.

    • using a partially isomorphic structure (and providing the witness).
    • by instanciating just the required mixin from scratch,
    • by instanciating a factory to create one or several structures,
    • by subtyping
    • by quotienting (out of scope of the tutorial).


Let's open an module and redefine int

Equality, countable and choice types, by injection

We provide an injection with explicit partial inverse, from int to nat + nat, this will be enough to provide the mixins for equality, countable and choice types.

We create the mixins for equality, countable and choice types from this injection, and gradually inhabit the hierarchy.


Abelian group structure, from scratch

We now create the abelian group structure of integers (here called Z-module), from scratch, introducing the operators and proving exactly the required properties.

Remark: we may develop here a piece of abelian group theory which is specific to the theory of integers. E.g.


Ring and Commutative ring structure, the stronger the better

This time, we will build directly a rich commutative ring factory first and use it to instanciate both the ring structure and the commutative ring struture at the same time. This is not only an economy of space, but an economy of proofs, since the commutativity property reduces the number of ring axioms to prove.


Other structures and instances

About other algebraic structures:

  • read the documentation of ssralg and ssrnum (algebraic structures with order and absolute value)

  • Canonical instances in the library are:
    • integers (int) (forms an integral domain)
    • rationals (rat) (forms an archimedian field)
    • algebraic numbers (algC) (forms an algebraically closed field)
    • polynomials {poly R} (forms an integral domain under sufficient hypothesis on the base ring)
    • matrices 'M[R]_(m, n) (forms a module / a finite dimension vector space)
    • square matrices 'M[R]_n (forms an algebra, if n := m.+1)

Group theory (not in this course):

  • see fingroup, perm, action, ...

Structures for morphisms:

** Structure preserving predicates:

**


Reasoning modulo p.

Instead of reasonning using (_ %| _) and (_ %% _), we switch to 'Z_p


More about structure preserving predicates.

There is a notion of subobject for a few algebraic concepts.

See the [hierarchy.dot], use [HB.about], [HB.howto] or read documentation headers to discover other substructure preserving predicates.

Application to building the field of Gauss integers

  • First we define a predicate for the algebraic numbers which are Gaussian integers.


We prove that Gaussian integers form a subring

  • Finally, we define the type of Gaussian Integer, as a sigma type of algebraic numbers. We soon prove that this is in fact a sub type.

  • We provide the subtype property, this makes it possible to use the generic operator val to get an algC from a Gaussian Integer.
  • Moreover provide a commutative ring structure to the type GI, using the subring canonical property for the predicate gaussInteger