Email Gateway (Apr 09 2021 at 13:39): Email Gateway (Apr 09 2021 at 13:39):From: "Thiemann, René" <Rene.Thiemann@uibk.ac.at>
Dear all,
there is a new AFP-entry by Anthony Bordg, Lawrence Paulson and Wenda Li:
Grothendieck's Schemes in Algebraic Geometry
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.
See https://www.isa-afp.org/entries/Grothendieck_Schemes.html for more details.
Enjoy,
René
Last updated: Jan 04 2025 at 20:18 UTC