Projective Space in Synthetic Algebraic Geometry

TL;DR

This paper develops the theory of projective space within synthetic algebraic geometry, establishing fundamental properties like automorphism and Picard groups using homotopy type theory and higher topos theory.

Contribution

It introduces a synthetic approach to projective space, proving key properties and providing new proofs that connect algebraic geometry with homotopy type theory.

Findings

Automorphism group of $ ext{P}^n$ is $ ext{PGL}_{n+1}(R)$

Picard group of $ ext{P}^n$ is $ ext{Z}$

Type of line bundles on $ ext{P}^n$ is $ ext{Z} imes K(R^ imes,1)$

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