mathlib3 documentation

algebraic_geometry.projective_spectrum.structure_sheaf

The structure sheaf on projective_spectrum π’œ. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In src/algebraic_geometry/topology.lean, we have given a topology on projective_spectrum π’œ; in this file we will construct a sheaf on projective_spectrum π’œ.

Notation #

Main definitions and results #

We define the structure sheaf as the subsheaf of all dependent function f : Ξ  x : U, homogeneous_localization π’œ x such that f is locally expressible as ratio of two elements of the same grading, i.e. βˆ€ y ∈ U, βˆƒ (V βŠ† U) (i : β„•) (a b ∈ π’œ i), βˆ€ z ∈ V, f z = a / b.

Then we establish that Proj π’œ is a LocallyRingedSpace:

References #

source
def algebraic_geometry.projective_spectrum.structure_sheaf.is_fraction {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] {U : topological_space.opens β†₯(projective_spectrum.Top π’œ)} (f : Ξ  (x : β†₯U), homogeneous_localization.at_prime π’œ x.val.as_homogeneous_ideal.to_ideal) :
Prop

The predicate saying that a dependent function on an open U is realised as a fixed fraction r / s of same grading in each of the stalks (which are localizations at various prime ideals).

Equations
source
def algebraic_geometry.projective_spectrum.structure_sheaf.is_fraction_prelocal {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
Top.prelocal_predicate (Ξ» (x : β†₯(projective_spectrum.Top π’œ)), homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal)

The predicate is_fraction is "prelocal", in the sense that if it holds on U it holds on any open subset V of U.

Equations
source
def algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
Top.local_predicate (Ξ» (x : β†₯(projective_spectrum.Top π’œ)), homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal)

We will define the structure sheaf as the subsheaf of all dependent functions in Ξ  x : U, homogeneous_localization π’œ x consisting of those functions which can locally be expressed as a ratio of A of same grading.

Equations
source
theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.zero_mem' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) :
(algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred 0
source
theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.one_mem' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) :
(algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred 1
source
theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.add_mem' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) (a b : Ξ  (x : β†₯(opposite.unop U)), homogeneous_localization.at_prime π’œ x.val.as_homogeneous_ideal.to_ideal) (ha : (algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred a) (hb : (algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred b) :
(algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred (a + b)
source
theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.neg_mem' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) (a : Ξ  (x : β†₯(opposite.unop U)), homogeneous_localization.at_prime π’œ x.val.as_homogeneous_ideal.to_ideal) (ha : (algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred a) :
(algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred (-a)
source
theorem algebraic_geometry.projective_spectrum.structure_sheaf.section_subring.mul_mem' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) (a b : Ξ  (x : β†₯(opposite.unop U)), homogeneous_localization.at_prime π’œ x.val.as_homogeneous_ideal.to_ideal) (ha : (algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred a) (hb : (algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred b) :
(algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction π’œ).to_prelocal_predicate.pred (a * b)
source
def algebraic_geometry.projective_spectrum.structure_sheaf.sections_subring {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] {π’œ : β„• β†’ submodule R A} [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) :
subring (Ξ  (x : β†₯(opposite.unop U)), homogeneous_localization.at_prime π’œ x.val.as_homogeneous_ideal.to_ideal)

The functions satisfying is_locally_fraction form a subring of all dependent functions Ξ  x : U, homogeneous_localization π’œ x.

Equations
source
def algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
Top.sheaf (Type u_2) (projective_spectrum.Top π’œ)

The structure sheaf (valued in Type, not yet CommRing) is the subsheaf consisting of functions satisfying is_locally_fraction.

Equations
source
@[protected, instance]
def algebraic_geometry.projective_spectrum.structure_sheaf.comm_ring_structure_sheaf_in_Type_obj {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) :
comm_ring ((algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type π’œ).val.obj U)
Equations
source
def algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
Top.presheaf CommRing (projective_spectrum.Top π’œ)

The structure presheaf, valued in CommRing, constructed by dressing up the Type valued structure presheaf.

Equations
source
@[simp]
theorem algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing_map_apply {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U V : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) (i : U ⟢ V) (αΎ° : (algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type π’œ).val.obj U) :
⇑((algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing π’œ).map i) αΎ° = (algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type π’œ).val.map i αΎ°
source
@[simp]
theorem algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing_obj {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U : (topological_space.opens β†₯(projective_spectrum.Top π’œ))α΅’α΅–) :
(algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing π’œ).obj U = CommRing.of ((algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type π’œ).val.obj U)
source
def algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_comp_forget {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
algebraic_geometry.projective_spectrum.structure_sheaf.structure_presheaf_in_CommRing π’œ β‹™ category_theory.forget CommRing β‰… (algebraic_geometry.projective_spectrum.structure_sheaf.structure_sheaf_in_Type π’œ).val

Some glue, verifying that that structure presheaf valued in CommRing agrees with the Type valued structure presheaf.

Equations
source
def algebraic_geometry.projective_spectrum.Proj.structure_sheaf {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
Top.sheaf CommRing (projective_spectrum.Top π’œ)

The structure sheaf on Proj π’œ, valued in CommRing.

Equations
source
@[simp]
theorem algebraic_geometry.res_apply {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U V : topological_space.opens β†₯(projective_spectrum.Top π’œ)) (i : V ⟢ U) (s : β†₯((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).val.obj (opposite.op U))) (x : β†₯V) :
(⇑((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).val.map i.op) s).val x = s.val (⇑i x)
source
def algebraic_geometry.Proj.to_SheafedSpace {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
algebraic_geometry.SheafedSpace CommRing

Proj of a graded ring as a SheafedSpace

Equations
source
def algebraic_geometry.open_to_localization {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U : topological_space.opens β†₯(projective_spectrum.Top π’œ)) (x : β†₯(projective_spectrum.Top π’œ)) (hx : x ∈ U) :
(algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).val.obj (opposite.op U) ⟢ CommRing.of (homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal)

The ring homomorphism that takes a section of the structure sheaf of Proj on the open set U, implemented as a subtype of dependent functions to localizations at homogeneous prime ideals, and evaluates the section on the point corresponding to a given homogeneous prime ideal.

Equations
source
noncomputable def algebraic_geometry.stalk_to_fiber_ring_hom {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (x : β†₯(projective_spectrum.Top π’œ)) :
(algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).presheaf.stalk x ⟢ CommRing.of (homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal)

The ring homomorphism from the stalk of the structure sheaf of Proj at a point corresponding to a homogeneous prime ideal x to the homogeneous localization at x, formed by gluing the open_to_localization maps.

Equations
source
@[simp]
theorem algebraic_geometry.germ_comp_stalk_to_fiber_ring_hom {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U : topological_space.opens β†₯(projective_spectrum.Top π’œ)) (x : β†₯U) :
(algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).presheaf.germ x ≫ algebraic_geometry.stalk_to_fiber_ring_hom π’œ ↑x = algebraic_geometry.open_to_localization π’œ U ↑x _
source
@[simp]
theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U : topological_space.opens β†₯(projective_spectrum.Top π’œ)) (x : β†₯(projective_spectrum.Top π’œ)) (hx : x ∈ U) (s : β†₯((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).val.obj (opposite.op U))) :
⇑(algebraic_geometry.stalk_to_fiber_ring_hom π’œ x) (⇑((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).presheaf.germ ⟨x, hx⟩) s) = s.val ⟨x, hx⟩
source
@[simp]
theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (U : topological_space.opens β†₯(projective_spectrum.Top π’œ)) (x : β†₯U) (s : β†₯((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).val.obj (opposite.op U))) :
⇑(algebraic_geometry.stalk_to_fiber_ring_hom π’œ ↑x) (⇑((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).presheaf.germ x) s) = s.val x
source
theorem algebraic_geometry.homogeneous_localization.mem_basic_open {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (x : β†₯(projective_spectrum.Top π’œ)) (f : homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal) :
x ∈ projective_spectrum.basic_open π’œ (homogeneous_localization.denom f)
source
noncomputable def algebraic_geometry.section_in_basic_open {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (x : β†₯(projective_spectrum.Top π’œ)) (f : homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal) :
β†₯((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).val.obj (opposite.op (projective_spectrum.basic_open π’œ (homogeneous_localization.denom f))))

Given a point x corresponding to a homogeneous prime ideal, there is a (dependent) function such that, for any f in the homogeneous localization at x, it returns the obvious section in the basic open set D(f.denom)

Equations
source
noncomputable def algebraic_geometry.homogeneous_localization_to_stalk {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (x : β†₯(projective_spectrum.Top π’œ)) :
homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal β†’ β†₯((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).presheaf.stalk x)

Given any point x and f in the homogeneous localization at x, there is an element in the stalk at x obtained by section_in_basic_open. This is the inverse of stalk_to_fiber_ring_hom.

Equations
source
noncomputable def algebraic_geometry.Proj.stalk_iso' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] (x : β†₯(projective_spectrum.Top π’œ)) :
β†₯((algebraic_geometry.projective_spectrum.Proj.structure_sheaf π’œ).presheaf.stalk x) ≃+* β†₯(CommRing.of (homogeneous_localization.at_prime π’œ x.as_homogeneous_ideal.to_ideal))

Using homogeneous_localization_to_stalk, we construct a ring isomorphism between stalk at x and homogeneous localization at x for any point x in Proj.

Equations
source
def algebraic_geometry.Proj.to_LocallyRingedSpace {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [algebra R A] (π’œ : β„• β†’ submodule R A) [graded_algebra π’œ] :
algebraic_geometry.LocallyRingedSpace

Proj of a graded ring as a LocallyRingedSpace

Equations