[isabelle] New in the AFP: Grothendieck's Schemes in Algebraic Geometry
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] New in the AFP: Grothendieck's Schemes in Algebraic Geometry
- From: Thiemann, René <Rene.Thiemann at uibk.ac.at>
- Date: Fri, 9 Apr 2021 13:38:15 +0000
- Accept-language: de-DE, de-AT, en-US
- Thread-index: AQHXLUWXLxGEN+zmTEuJ4S9kfx0O+A==
- Thread-topic: New in the AFP: Grothendieck's Schemes in Algebraic Geometry
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and