Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-12 08:46 6bc2bd6e

View on Github →

feat(algebraic_geometry/projective_spectrum): Proj as a locally ringed space (#12773) This pr is about proving that Proj with its structure sheaf is a locally ringed space

Estimated changes

Modified src/algebraic_geometry/projective_spectrum/structure_sheaf.lean

added def algebraic_geometry.Proj.stalk_iso'

added def algebraic_geometry.Proj.to_LocallyRingedSpace

added def algebraic_geometry.Proj.to_SheafedSpace

added theorem algebraic_geometry.germ_comp_stalk_to_fiber_ring_hom

added theorem algebraic_geometry.homogeneous_localization.mem_basic_open

added def algebraic_geometry.homogeneous_localization_to_stalk

added def algebraic_geometry.open_to_localization

added theorem algebraic_geometry.res_apply

added def algebraic_geometry.section_in_basic_open

added def algebraic_geometry.stalk_to_fiber_ring_hom

added theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ'

added theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ