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 src/algebraic_geometry/projective_spectrum/structure_sheaf.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
f : A
,Proj.T | (pbo f)
is homeomorphic toSpec.T A⁰_f
:
- forward direction :
for any
x : pbo f
, i.e. a relevant homogeneous prime idealx
, send it tox ∩ span {g / 1 | g ∈ A}
(seeTop_component.forward.carrier
). This ideal is prime, the proof is inTop_component.forward.to_fun
. The fact that this function is continuous is found inTop_component.forward
- backward direction : TBC
Main Definitions and Statements #
degree_zero_part
: 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
-
Top_component.forward
:forward f
is the continuous map betweenProj.T| pbo f
andSpec.T A⁰_f
-
Top_component.forward.preimage_eq
: for anya: A
, ifa/f^m
has degree zero, then the preimage ofsbo a/f^m
underforward f
ispbo f ∩ pbo a
. -
Robin Hartshorne, Algebraic Geometry: Chapter II.2 Proposition 2.5
The degree zero part of the localized ring Aₓ
is the subring of elements of the form a/x^n
such
that a
and x^n
have the same degree.
Equations
Instances for ↥algebraic_geometry.degree_zero_part
Equations
Every element in the degree zero part of Aₓ
can be written as a/x^n
for some a
and n : ℕ
,
degree_zero_part.deg
picks this natural number n
Equations
Every element in the degree zero part of Aₓ
can be written as a/x^n
for some a
and n : ℕ
,
degree_zero_part.deg
picks the numerator a
Equations
- algebraic_geometry.degree_zero_part.num f_deg x = (Exists.some _).val