Max Zeuner: What is synthetic algebraic geometry?

Abstract

Synthetic algebraic geometry (SAG) is generally speaking the study of algebro-geometric objects in the internal logic of the so-called big Zariski topos. Complicated sheaf-theoretic constructions often become fundamental algebraic constructions from the internal point of view and this can be used to simplify and shorten proofs. A central role is taken by the affine line \(\mathbb{A}^1\), which internally looks like a ring with very surprising, anti-classical properties. In fact, it is possible to develop SAG axiomatically in a constructive meta-theory by stipulating a ring sharing some key properties with the internal affine line. An ongoing project at Chalmers university develops this axiomatic approach to SAG, using homotopy type theory (HoTT) as the constructive meta-theory. The purpose of this talk is to give the necessary background on the big Zariski topos and a basic introduction to axiomatic SAG. If time permits, I would also like to discuss the benefits of working in HoTT (namely being able to define cohomology) and sketch a purported model construction using "cubical Zariski sheaves".