  Working in an abstract, homotopy type theory based axiomatization of the
higher Zariski-topos called synthetic algebraic geometry, we show that the
Picard group of projective n-space is the integers, the automorphism group of
projective n-space is PGL(n+1) and morphisms between projective standard spaces
are given by homogenous polynomials in the usual way.
