Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-11 23:09 0453d606

View on Github →

feat(algebraic_geometry/projective_spectrum): structure sheaf of Proj of graded ring (#13072) Construct the structure sheaf of Proj of a graded algebra.

Estimated changes

Created src/algebraic_geometry/projective_spectrum/structure_sheaf.lean

added def algebraic_geometry.projective_spectrum.Proj.structure_sheaf

added def algebraic_geometry.projective_spectrum.structure_sheaf.is_fraction

added def algebraic_geometry.projective_spectrum.structure_sheaf.is_fraction_prelocal

added def algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction

added theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.add_mem'

added theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.mul_mem'

added theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.neg_mem'

added theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.one_mem'

added theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.zero_mem'

added def algebraic_geometry.projective_spectrum.structure_sheaf.sections_subring

added def algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_comp_forget

added def algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing

added def algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type

Modified src/algebraic_geometry/projective_spectrum/topology.lean

added def projective_spectrum.Top