Commit 2021-05-08 05:52 583ad823

View on Github →

feat(algebraic_geometry/structure_sheaf): Structure sheaf on basic opens (#7405) Proves that to_basic_open is an isomorphism of commutative rings. Also adds Hartshorne as a reference.

Estimated changes

Modified docs/references.bib

Modified src/algebraic_geometry/structure_sheaf.lean

added def algebraic_geometry.basic_open_iso

added theorem algebraic_geometry.locally_const_basic_open

added theorem algebraic_geometry.normalize_finite_fraction_representation

added theorem algebraic_geometry.to_basic_open_injective

added theorem algebraic_geometry.to_basic_open_surjective