Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Grothendieck's Schemes in Alge...

view this post on Zulip Email Gateway (Apr 09 2021 at 13:39):

From: "Thiemann, René" <>
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 for more details.


Last updated: Dec 08 2021 at 10:22 UTC