Projective Space in Synthetic Algebraic Geometry
Felix Cherubini, Thierry Coquand, Matthias Ritter, David Wärn
TL;DR
The paper develops projective space in synthetic algebraic geometry using homotopy type theory internal to the Zariski topos, leveraging the locality, duality, and Zariski-local choice axioms. It proves that Aut$(\mathbb{P}^n)=\mathrm{PGL}_{n+1}(R)$ and that $ ext{Pic}(\mathbb{P}^n)=\mathbb{Z}$, with stronger characterizations of line bundles as $ ext{Line}\times\mathbb{Z}$-data and all maps to $\mathbb{P}^m$ given by homogeneous polynomials of fixed degree. The approach combines Veronese embeddings, Horrocks' theorem, and Quillen patching in a synthetic, non-set-theoretic context to obtain both algebraic and geometric proofs, including alternative and geometric routes to the Picard group. These results generalize classical facts to the synthetic setting and illuminate the structure of line bundles, automorphisms, and morphisms of projective space internally to a higher topos. The methodology highlights the power of internal cohomology, higher-type line bundles, and topos-theoretic reasoning for foundational results in algebraic geometry.
Abstract
Synthetic algebraic geometry is a new approach to algebraic geometry. It consists in using homotopy type theory extended with three axioms, together with the interpretation of these in a higher version of the Zariski topos, in order to do algebraic geometry internally to this topos. In this article, we will show basic properties of projective n-space $\mathbb{P}^n$ in synthetic algebraic geometry. In particular, we show that the automorphism group of $\mathbb{P}^n$ is $\mathrm{PGL}_{n+1}(R)$ and that the picard group is $\mathbb{Z}$. We will provide different proofs of the latter statement, where the most synthetic approach naturally leads to the refined statement that the type of line bundles on $\mathbb{P}^n$ is the higher type $\mathbb{Z}\times K(R^\times,1)$, where $K(R^\times,1)$ is a delooping of the group of units of the internal base ring $R$.