Grothendieck's Schemes in Algebraic Geometry

Title:	Grothendieck's Schemes in Algebraic Geometry
Authors:	Anthony Bordg, Lawrence Paulson and Wenda Li
Submission date:	2021-03-29
Abstract:	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.
BibTeX:	@article{Grothendieck_Schemes-AFP, author = {Anthony Bordg and Lawrence Paulson and Wenda Li}, title = {Grothendieck's Schemes in Algebraic Geometry}, journal = {Archive of Formal Proofs}, month = mar, year = 2021, note = {\url{https://isa-afp.org/entries/Grothendieck_Schemes.html}, Formal proof development}, ISSN = {2150-914x}, }
License:	BSD License
Depends on:	Jacobson_Basic_Algebra
Status: [ok]	This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.