Grothendieck's Schemes in Algebraic Geometry

Anthony Bordg 🌐, Lawrence C. Paulson 🌐 and Wenda Li 🌐

March 29, 2021


We formalize mainstream structures in algebraic geometry culminating in Grothendieck's schemes: presheaves of rings, sheaves of rings, ringed spaces, locally ringed spaces, affine schemes and schemes. We prove that the spectrum of a ring is a locally ringed space, hence an affine scheme. Finally, we prove that any affine scheme is a scheme.
BSD License


Theories of Grothendieck_Schemes