# Constructive Algebra

## Goals of the course

This course is an introduction to constructive algebra. We recall first
what is Hilbert's program, and the distinction between constructive and classical
reasoning. We explain how
to classify the complexity of mathematical notions and proofs in mathematics
using basic notions of logic. A typical example of reduction of logical complexity
can be seen in the use of point-free representation of the Zariski spectrum of
a commutative ring. We explain also how to make sense effectively of the algebraic closure
of a field.

## Courses

**Course 1** Introduction to constructive algebra

**Course 2** Zariski lattice and Prufer domain
and Structure sheaf

**Course 3** Separable algebraic closure of a perfect field

## Interesting links

Besides the book by Mines, Richman and Ruitenburg, the
book of Yengui
on constructive commutative algebra and the book by Lombardi and Quitte below
(each of them with a lot of exercises) are recommended

The home page of Henri Lombardi contains many
relevant papers. See also the book
about finitely generated projective modules

The home page of Harold
Edwards contains interesting talks. As a typical example
see this talk on
Abel's Theorem. His
book on constructive
mathematics is recommended

The home page
of Mohamed Barakat, with elegant implementations of abstract algorithms

The PhD thesis of
Ingo Blechschmidt on internal language of toposes in algebraic geometry

The PhD thesis of Claire Tete (in french)
on constructive homological algebra

A master thesis
on using homological algebra for computation of gcd in polynomial rings

A master thesis on coherent rings

An historical introduction
to Dedekind's theory of ideals

A paper on
proof theory (coherent logic) and algebra

Some remarks about
two notes of Stone or abstract functional analysis

A logical approach to commutative algebra

The home page of Fred Richman contains also
relevant papers. In particular, see the paper on "Intuitionism as generalization".

The following paper provides a nice introduction
to constructive mathematics and to type theory