A Sheaf Model of the Algebraic Closure

Bassel Mannaa
Thierry Coquand

In constructive algebra one cannot in general decide the irreducibility of a polynomial over a field K. This poses some problems to showing the existence of the algebraic closure of K. We give a possible constructive interpretation of the existence of the algebraic closure of a field in characteristic 0 by building, in a constructive metatheory, a suitable site model where there is such an algebraic closure. One can then extract computational content from this model. We give examples of computation based on this model.

In Paulo Oliva: Proceedings Fifth International Workshop on Classical Logic and Computation (CL&C 2014), Vienna, Austria, July 13, 2014, Electronic Proceedings in Theoretical Computer Science 164, pp. 18–32.
Published: 9th September 2014.

ArXived at: http://dx.doi.org/10.4204/EPTCS.164.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org