mathlib3

b79fc037 - feature(algebraic_geometry/Scheme): the category of schemes (#3961)

feature(algebraic_geometry/Scheme): the category of schemes (#3961) The definition of a `Scheme`, and the category of schemes as the full subcategory of locally ringed spaces. Co-authored-by: Johan Commelin <johan@commelin.net> 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>