Algebraic Geometry in Coq
Welcome to the homepage of the Coq algebraic geometry project. Small algebraic geometric developments have been
done in Coq many times, but as far as we know there has been no bottom-up development of modern (Grothendieck-style)
algebraic geometry in Coq. This project is intended to fill this gap, and also to demonstrate that Coq and SSReflect/MathComp
are capable of handling high-level, abstract mathematics, in addition to low-level, concrete mathematics which it is well-known
to be able to handle well.
This project is in many ways inspired by the Stacks Project, in that we
also start with few preliminaries and build up the tools necessary to develop algebraic geometry step-by-step; it is
also motivated in part by Lean's Mathlib. We take as
granted Coq's expressive Gallina specification language, the SSReflect proof language and the Coq
Mathematical Components library, and formalize the required stepping stones towards algebraic geometry. We do not
necessarily follow the Stacks Project in our formalization, but like the Stacks Project, we aim to build a coherent library of
related mathematics along our way. Eventually, however, this project would not necessarily be limited to algebraic geometry:
we are also interested in expanding in other related directions, such as homological algebra and topos theory.
Current & planned developments
Currently, our main goal is to define the notion of an affine scheme, i.e. a locally ringed space
isomorphic to the spectrum of a commutative ring with unit. This requires a bit of category theory and commutative algebra, as well
as some sheaf theory.
Our current formaliation roadmap is:
We intend to do a formalization of "textbook" algebraic geometry (as in Grothendieck's EGA
or the Stacks Project), which relies heavily on non-constructive reasoning principles
(especially the Axiom of Choice). Therefore, we always assume functional and proof extensionality, decidability of every proposition,
and the (type-theoretic) Axiom of Choice in our development.
Currently, Xuanrui Qi is the only person working on this project.
We would love to have some collaborators, especially those who are experienced in using SSReflect/MathComp to formalize
mathematics, and those who have some expertise in algebraic geometry.
Many people have given their valuable advice and support:
- Reynald Affeldt (National Institute of Advanced Industrial Science and Technology, Japan)
- Takafumi Saikawa (Nagoya University, Japan)
- David Nowak (CNRS & University of Lille, France)
- Jacques Garrigue (Nagoya University, Japan).