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.

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.

License

BSD License

Topics

Session Grothendieck_Schemes

Depends on

Cite

× 
@article{Grothendieck_Schemes-AFP,
  author  = {Anthony Bordg and Lawrence C. Paulson and Wenda Li},
  title   = {Grothendieck's Schemes in Algebraic Geometry},
  journal = {Archive of Formal Proofs},
  month   = {March},
  year    = {2021},
  note    = {\url{https://isa-afp.org/entries/Grothendieck_Schemes.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: