Documentation

Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme

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:
  1. 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 map A⁰_f → Γ(Proj, pbo f) from the ring of homogeneous localization of A away from f to the local sections of structure sheaf of projective spectrum on the basic open set around f. The map A⁰_f → Γ(Proj, pbo f) is constructed in awayToΓ and is defined by sending s ∈ A⁰_f to the section x ↦ s on pbo f.

Main Definitions and Statements #

For a homogeneous element f of degree m

If we further assume m is positive

Finally,

Reference #

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

The continuous function from the basic open set D(f) in Proj to the corresponding basic open set in Spec A⁰_f.

Equations
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}

Equations
  • One or more equations did not get rendered due to their size.
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) :
a carrier f_deg q ∀ (i : ), HomogeneousLocalization.mk { deg := m * i, num := (GradedAlgebra.proj 𝒜 i) a ^ m, , den := f ^ i, , den_mem := } q.asIdeal
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) {n : } (hn : a 𝒜 n) :
a carrier f_deg q HomogeneousLocalization.mk { deg := m * n, num := a ^ m, , den := f ^ n, , den_mem := } q.asIdeal
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.mem_carrier_iff_of_mem_mul {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (a : A) {n : } (hn : a 𝒜 (n * m)) :
a carrier f_deg q HomogeneousLocalization.mk { deg := m * n, num := a, , den := f ^ n, , den_mem := } q.asIdeal
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.add_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) {a b : A} (ha : a carrier f_deg q) (hb : b carrier f_deg q) :
a + b carrier f_deg q
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.zero_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :
0 carrier f_deg q
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.smul_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) (c x : A) (hx : x carrier f_deg q) :
c x carrier f_deg q
def AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :

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.
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :
fasIdeal f_deg hm q
@[deprecated AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem (since := "2025-05-23")]
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_not_mem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :
fasIdeal f_deg hm q

Alias of AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.denom_notMem.

theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.ne_top {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :
asIdeal f_deg hm q
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.FromSpec.carrier.asIdeal.prime {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (q : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :
(asIdeal f_deg hm q).IsPrime

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.
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_fromSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (x : (Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))).toPresheafedSpace) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.fromSpec_toSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (x : ((Proj.toLocallyRingedSpace 𝒜).restrict ).toPresheafedSpace) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_injective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_surjective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_bijective {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
theorem AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec.image_basicOpen_eq_basicOpen {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {𝒜 : Submodule R A} [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) (a : A) (i : ) :
(CategoryTheory.ConcreteCategory.hom (toSpec 𝒜 f)) '' (Subtype.val ⁻¹' (ProjectiveSpectrum.basicOpen 𝒜 (((DirectSum.decompose 𝒜) a) i))) = (PrimeSpectrum.basicOpen (HomogeneousLocalization.mk { deg := m * i, num := (((DirectSum.decompose 𝒜) a) i) ^ m, , den := f ^ i, , den_mem := })).carrier

The continuous function Spec A⁰_f → Proj|D(f) sending q to {a | aᵢᵐ/fⁱ ∈ q} where m is the degree of f

Equations

The homeomorphism Proj|D(f) ≅ Spec A⁰_f defined by

  • φ : Proj|D(f) ⟶ Spec A⁰_f by sending x to A⁰_f ∩ span {g / 1 | g ∈ x}
  • ψ : Spec A⁰_f ⟶ Proj|D(f) by sending q 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.
theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec_base_isIso {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] {f : A} {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :

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.
theorem AlgebraicGeometry.ProjectiveSpectrum.Proj.isIso_toSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :
def AlgebraicGeometry.projIsoSpec {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] (f : A) {m : } (f_deg : f 𝒜 m) (hm : 0 < m) :

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
def AlgebraicGeometry.Proj {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] (𝒜 : Submodule R A) [GradedAlgebra 𝒜] :

This is the scheme Proj(A) for any -graded ring A.

Equations