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.asIdeal.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; these are achieved inProjIsoSpecTopComponent.fromSpec_toSpec
andProjIsoSpecTopComponent.toSpec_fromSpec
.
- This is in fact an ideal, the proof can be found in
- Then we construct a morphism of locally ringed spaces
α : Proj| (pbo f) ⟶ Spec.T A⁰_f
as the following: by the Gamma-Spec adjunction, it is sufficient to construct a ring mapA⁰_f → Γ(Proj, pbo f)
from the ring of homogeneous localization ofA
away fromf
to the local sections of structure sheaf of projective spectrum on the basic open set aroundf
. The mapA⁰_f → Γ(Proj, pbo f)
is constructed inawayToΓ
and is defined by sendings ∈ A⁰_f
to the sectionx ↦ s
onpbo f
.
Main Definitions and Statements #
For a homogeneous element f
of degree m
ProjIsoSpecTopComponent.toSpec
: the continuous map betweenProj.T| pbo f
andSpec.T A⁰_f
defined by sendingx : Proj| (pbo f)
toA⁰_f ∩ span {g / 1 | g ∈ x}
. We also denote this map asψ
.ProjIsoSpecTopComponent.ToSpec.preimage_eq
: for anya: A
, ifa/f^m
has degree zero, then the preimage ofsbo a/f^m
undertoSpec f
ispbo f ∩ pbo a
.
If we further assume m
is positive
ProjIsoSpecTopComponent.fromSpec
: the continuous map betweenSpec.T A⁰_f
andProj.T| pbo f
defined by sendingq
to{a | aᵢᵐ/fⁱ ∈ q}
whereaᵢ
is thei
-th coordinate ofa
. We also denote this map asφ
projIsoSpecTopComponent
: the homeomorphismProj.T| pbo f ≅ Spec.T A⁰_f
obtained byφ
andψ
.ProjectiveSpectrum.Proj.toSpec
: the morphism of locally ringed spaces betweenProj| pbo f
andSpec A⁰_f
corresponding to the ring mapA⁰_f → Γ(Proj, pbo f)
under the Gamma-Spec adjunction defined by sendings
to the sectionx ↦ s
onpbo f
.
Finally,
AlgebraicGeometry.Proj
: for anyℕ
-graded ringA
,Proj A
is locally affine, hence is a scheme.
Reference #
- [Robin Hartshorne, Algebraic Geometry][Har77]: Chapter II.2 Proposition 2.5
Proj
restrict to some open set
Equations
- AlgebraicGeometry.«termProj|_» = Lean.ParserDescr.node `AlgebraicGeometry.«termProj|_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "Proj| ") (Lean.ParserDescr.cat `term 0))
For any x
in Proj| (pbo f)
, the corresponding ideal in Spec A⁰_f
. This fact that this ideal
is prime is proven in TopComponent.Forward.toFun
.
Equations
- One or more equations did not get rendered due to their size.
The function between the basic open set D(f)
in Proj
to the corresponding basic open set in
Spec A⁰_f
. This is bundled into a continuous map in TopComponent.forward
.
Equations
- AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f x = { asIdeal := AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x, isPrime := ⋯ }
The continuous function from the basic open set D(f)
in Proj
to the corresponding basic open set in Spec A⁰_f
.
Equations
- AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f = TopCat.ofHom { toFun := AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.toFun f, continuous_toFun := ⋯ }
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The function from Spec A⁰_f
to Proj|D(f)
is defined by q ↦ {a | aᵢᵐ/fⁱ ∈ q}
, i.e. sending
q
a prime ideal in A⁰_f
to the homogeneous prime relevant ideal containing only and all the
elements a : A
such that for every i
, the degree 0 element formed by dividing the m
-th power
of the i
-th projection of a
by the i
-th power of the degree-m
homogeneous element f
,
lies in q
.
The set {a | aᵢᵐ/fⁱ ∈ q}
- is an ideal, as proved in
carrier.asIdeal
; - is homogeneous, as proved in
carrier.asHomogeneousIdeal
; - is prime, as proved in
carrier.asIdeal.prime
; - is relevant, as proved in
carrier.relevant
.
Equations
- One or more equations did not get rendered due to their size.
For a prime ideal q
in A⁰_f
, the set {a | aᵢᵐ/fⁱ ∈ q}
as an ideal.
Equations
- One or more equations did not get rendered due to their size.
For a prime ideal q
in A⁰_f
, the set {a | aᵢᵐ/fⁱ ∈ q}
as a homogeneous ideal.
Equations
- One or more equations did not get rendered due to their size.
Alias of AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem
.
The function Spec A⁰_f → Proj|D(f)
sending q
to {a | aᵢᵐ/fⁱ ∈ q}
.
Equations
- One or more equations did not get rendered due to their size.
The continuous function Spec A⁰_f → Proj|D(f)
sending q
to {a | aᵢᵐ/fⁱ ∈ q}
where
m
is the degree of f
Equations
- AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec f_deg hm = TopCat.ofHom { toFun := AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.toFun f_deg hm, continuous_toFun := ⋯ }
The homeomorphism Proj|D(f) ≅ Spec A⁰_f
defined by
φ : Proj|D(f) ⟶ Spec A⁰_f
by sendingx
toA⁰_f ∩ span {g / 1 | g ∈ x}
ψ : Spec A⁰_f ⟶ Proj|D(f)
by sendingq
to{a | aᵢᵐ/fⁱ ∈ q}
.
Equations
- One or more equations did not get rendered due to their size.
The ring map from A⁰_ f
to the local sections of the structure sheaf of the projective spectrum of
A
on the basic open set D(f)
defined by sending s ∈ A⁰_f
to the section x ↦ s
on D(f)
.
Equations
- One or more equations did not get rendered due to their size.
The ring map from A⁰_ f
to the global sections of the structure sheaf of the projective spectrum
of A
restricted to the basic open set D(f)
.
Mathematically, the map is the same as awayToSection
.
Equations
- One or more equations did not get rendered due to their size.
The morphism of locally ringed space from Proj|D(f)
to Spec A⁰_f
induced by the ring map
A⁰_ f → Γ(Proj, D(f))
under the gamma spec adjunction.
Equations
- One or more equations did not get rendered due to their size.
If x
is a point in the basic open set D(f)
where f
is a homogeneous element of positive
degree, then the homogeneously localized ring A⁰ₓ
has the universal property of the localization
of A⁰_f
at φ(x)
where φ : Proj|D(f) ⟶ Spec A⁰_f
is the morphism of locally ringed space
constructed as above.
For an element f ∈ A
with positive degree and a homogeneous ideal in D(f)
, we have that the
stalk of Spec A⁰_ f
at y
is isomorphic to A⁰ₓ
where y
is the point in Proj
corresponding
to x
.
Equations
- One or more equations did not get rendered due to their size.
If f ∈ A
is a homogeneous element of positive degree, then the projective spectrum restricted to
D(f)
as a locally ringed space is isomorphic to Spec A⁰_f
.
Equations
This is the scheme Proj(A)
for any ℕ
-graded ring A
.
Equations
- AlgebraicGeometry.Proj 𝒜 = { toLocallyRingedSpace := AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜, local_affine := ⋯ }