mathlib
17c4651c - feat(algebraic_geometry): structure sheaf on Spec R (#3907)

Commit
5 years ago
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. Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Ashvni <ashvni.n@gmail.com>
Author
Parents
Loading