Proj as a scheme #

This file is to prove that Proj is a scheme.

Notation #

Implementation #

In AlgebraicGeometry/ProjectiveSpectrum/StructureSheaf.lean, we have given Proj a structure sheaf so that Proj is a locally ringed space. In this file we will prove that Proj equipped with this structure sheaf is a scheme. We achieve this by using an affine cover by basic open sets in Proj, more specifically:

  1. We prove that Proj can be covered by basic open sets at homogeneous element of positive degree.
  2. We prove that for any homogeneous element f : A of positive degree m, Proj.T | (pbo f) is homeomorphic to Spec.T A⁰_f:

Main Definitions and Statements #

For a homogeneous element f of degree n