Commit 2020-08-29 13:43 17c4651c

feat(algebraic_geometry): structure sheaf on Spec R (#3907) This defines the structure sheaf on Spec R, following Hartshorne, as a sheaf in CommRing on prime_spectrum R. We still need to show at the stalk at a point is just the localization; this is another page of Hartshorne, and will come in a subsequent PR.