A Sheaf Model of the Algebraic Closure
arXiv:1404.4549 · doi:10.4204/EPTCS.164.2
Abstract
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 Proceedings CL&C 2014, arXiv:1409.2593