Commit 2021-10-01 08:55 f7d7a91c

View on Github →

feat(algebraic_geometry/ringed_space): Define basic opens for ringed spaces. (#9358) Defines the category of ringed spaces, as an alias for SheafedSpace CommRing. We provide basic lemmas about sections being units in the stalk and define basic opens in this context.

Estimated changes

Modified src/algebraic_geometry/locally_ringed_space.lean

added def algebraic_geometry.LocallyRingedSpace.to_RingedSpace

Created src/algebraic_geometry/ringed_space.lean

added def algebraic_geometry.RingedSpace.basic_open

added theorem algebraic_geometry.RingedSpace.is_unit_of_is_unit_germ

added theorem algebraic_geometry.RingedSpace.is_unit_res_basic_open

added theorem algebraic_geometry.RingedSpace.is_unit_res_of_is_unit_germ

added theorem algebraic_geometry.RingedSpace.mem_basic_open

added def algebraic_geometry.RingedSpace