A foundation for synthetic algebraic geometry

Abstract

This is a foundation for algebraic geometry, developed internal to the Zariski topos, building on the work of Kock and Blechschmidt (Kock (2006) [I.12], Blechschmidt (2017)). 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, that is, generating covers are given by localization maps for finitely many elements f1, . . ., fn that generate the ideal (1)=A⊂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.