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:

Note

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.

People

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).