Proj as a scheme #
This file is to prove that Proj
is a scheme.
Notation #
Proj
:Proj
as a locally ringed spaceProj.T
: the underlying topological space ofProj
Proj U
:Proj
restricted to some open setU
Proj.T U
: the underlying topological space ofProj
restricted to open setU
pbo f
: basic open set atf
inProj
Spec
:Spec
as a locally ringed spaceSpec.T
: the underlying topological space ofSpec
sbo g
: basic open set atg
inSpec
A⁰_x
: the degree zero part of localized ringAₓ
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:
 We prove that
Proj
can be covered by basic open sets at homogeneous element of positive degree.  We prove that for any homogeneous element
f : A
of positive degreem
,Proj.T  (pbo f)
is homeomorphic toSpec.T A⁰_f
:
 forward direction
toSpec
: for anyx : pbo f
, i.e. a relevant homogeneous prime idealx
, send it toA⁰_f ∩ span {g / 1  g ∈ x}
(seeProjIsoSpecTopComponent.IoSpec.carrier
). This ideal is prime, the proof is inProjIsoSpecTopcomponent.ToSpec.toFun
. The fact that this function is continuous is found inProjIsoSpecTopComponent.toSpec
 backward direction
fromSpec
: for anyq : Spec A⁰_f
, we send it to{a  ∀ i, aᵢᵐ/fⁱ ∈ q}
; we need this to be a homogeneous prime ideal that is relevant. This is in fact an ideal, the proof can be found in
ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal
;  This ideal is also homogeneous, the proof can be found in
ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.homogeneous
;  This ideal is relevant, the proof can be found in
ProjIsoSpecTopComponent.FromSpec.carrier.relevant
;  This ideal is prime, the proof can be found in
ProjIsoSpecTopComponent.FromSpec.carrier.prime
. Hence we have a well defined functionSpec.T A⁰_f → Proj.T  (pbo f)
, this function is calledProjIsoSpecTopComponent.FromSpec.toFun
. But to prove the continuity of this function, we need to provefromSpec ∘ toSpec
andtoSpec ∘ fromSpec
are both identities (TBC).
 This is in fact an ideal, the proof can be found in
Main Definitions and Statements #
degreeZeroPart
: the degree zero part of the localized ringAₓ
wherex
is a homogeneous element of degreen
is the subring of elements of the forma/f^m
wherea
has degreemn
.
For a homogeneous element f
of degree n

ProjIsoSpecTopComponent.toSpec
:forward f
is the continuous map betweenProj.T pbo f
andSpec.T A⁰_f

ProjIsoSpecTopComponent.ToSpec.preimage_eq
: for anya: A
, ifa/f^m
has degree zero, then the preimage ofsbo a/f^m
underto_Spec f
ispbo f ∩ pbo a
. 
[Robin Hartshorne, Algebraic Geometry][Har77]: Chapter II.2 Proposition 2.5