Proj as a scheme #

This file is to prove that Proj is a scheme.

Notation #

Proj : Proj as a locally ringed space
Proj.T : the underlying topological space of Proj
Proj| U : Proj restricted to some open set U
Proj.T| U : the underlying topological space of Proj restricted to open set U
pbo f : basic open set at f in Proj
Spec : Spec as a locally ringed space
Spec.T : the underlying topological space of Spec
sbo g : basic open set at g in Spec
A⁰_x : the degree zero part of localized ring Aₓ

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 degree m, Proj.T | (pbo f) is homeomorphic to Spec.T A⁰_f:

forward direction toSpec: for any x : pbo f, i.e. a relevant homogeneous prime ideal x, send it to A⁰_f ∩ span {g / 1 | g ∈ x} (see ProjIsoSpecTopComponent.IoSpec.carrier). This ideal is prime, the proof is in ProjIsoSpecTopComponent.ToSpec.toFun. The fact that this function is continuous is found in ProjIsoSpecTopComponent.toSpec
backward direction fromSpec: for any q : 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 function Spec.T A⁰_f → Proj.T | (pbo f), this function is called ProjIsoSpecTopComponent.FromSpec.toFun. But to prove the continuity of this function, we need to prove fromSpec ∘ toSpec and toSpec ∘ fromSpec are both identities; these are achieved in ProjIsoSpecTopComponent.fromSpec_toSpec and ProjIsoSpecTopComponent.toSpec_fromSpec.

Main Definitions and Statements #

For a homogeneous element f of degree m

ProjIsoSpecTopComponent.toSpec: the continuous map between Proj.T| pbo f and Spec.T A⁰_f defined by sending x : Proj| (pbo f) to A⁰_f ∩ span {g / 1 | g ∈ x}. We also denote this map as ψ.
ProjIsoSpecTopComponent.ToSpec.preimage_eq: for any a: A, if a/f^m has degree zero, then the preimage of sbo a/f^m under to_Spec f is pbo f ∩ pbo a.

If we further assume m is positive

ProjIsoSpecTopComponent.fromSpec: the continuous map between Spec.T A⁰_f and Proj.T| pbo f defined by sending q to {a | aᵢᵐ/fⁱ ∈ q} where aᵢ is the i-th coordinate of a. We also denote this map as φ
projIsoSpecTopComponent: the homeomorphism Proj.T| pbo f ≅ Spec.T A⁰_f obtained by φ and ψ.

Reference #

[Robin Hartshorne, Algebraic Geometry][Har77]: Chapter II.2 Proposition 2.5