Grothendieck's Schemes in Algebraic Geometry

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

March 29, 2021

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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


Session Grothendieck_Schemes