A Foundation for Synthetic Algebraic Geometry
Felix Cherubini, Thierry Coquand, Matthias Hutzler
TL;DR
This work develops a synthetic foundation for algebraic geometry inside the Zariski topos, leveraging homotopy type theory with three core axioms (Loc, SQC, Z-choice) to internalize affine schemes, schemes, and cohomology. It provides two complementary constructions of projective space, a robust theory of bundles and quasi-coherence, and a version of Čech cohomology that aligns with sheaf-theoretic expectations, all within a constructive, type-theoretic framework. Central contributions include proving a contravariant equivalence between finitely presented algebras and affine schemes, establishing vanishing results for cohomology on affine schemes, and detailing a comprehensive type-theoretic justification of the axioms via internal presheaf and sheaf models, including global sections and Zariski global choice. The framework enables internal manipulation of schemes, open/closed subtypes, descent data, and glueing, while maintaining a precise correspondence with classical algebraic geometry, and it lays groundwork for internal cohomology, projective geometry, and line bundle theory in synthetic settings.
Abstract
This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt. The Zariski topos consists of sheaves on the site opposite to the category of finitely presented algebras over a fixed ring, with the Zariski topology, i.e. generating covers are given by localization maps $A\to A_{f_1}$ for finitely many elements $f_1,\dots,f_n$ that generate the ideal $(1)=A\subseteq A$. We use homotopy type theory together with three axioms as the internal language of a (higher) Zariski topos. One of our main contributions is the use of higher types -- in the homotopical sense -- to define and reason about cohomology. Actually computing cohomology groups, seems to need a principle along the lines of our ``Zariski local choice'' axiom, which we justify as well as the other axioms using a cubical model of homotopy type theory.