Projective Space in Synthetic Algebraic Geometry

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$.