Projective Space in Synthetic 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$.