# mathlib3documentation

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 #

• R is a commutative semiring;
• A is a commutative ring and an R-algebra;
• π : β β submodule R A is the grading of A;
• U is opposite object of some open subset of projective_spectrum.Top.

## 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.

• algebraic_geometry.projective_spectrum.structure_sheaf.is_locally_fraction: the predicate that a dependent function is locally expressible as a ratio of two elements of the same grading.
• algebraic_geometry.projective_spectrum.structure_sheaf.sections_subring: the dependent functions satisfying the above local property forms a subring of all dependent functions Ξ  x : U, homogeneous_localization π x.
• algebraic_geometry.Proj.structure_sheaf: the sheaf with U β¦ sections_subring U and natural restriction map.

Then we establish that Proj π is a LocallyRingedSpace:

• algebraic_geometry.Proj.stalk_iso': for any x : projective_spectrum π, the stalk of Proj.structure_sheaf at x is isomorphic to homogeneous_localization π x.
• algebraic_geometry.Proj.to_LocallyRingedSpace: Proj as a locally ringed space.

## References #

def algebraic_geometry.projective_spectrum.structure_sheaf.is_fraction {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] {π : β β A} [graded_algebra π] (f : Ξ  (x : β₯U), ) :
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

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

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

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

Equations

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

Equations
@[protected, instance]
Equations

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

Equations

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

Equations
def algebraic_geometry.projective_spectrum.Proj.structure_sheaf {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] :

The structure sheaf on Proj π, valued in CommRing.

Equations
@[simp]
theorem algebraic_geometry.res_apply {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (U V : topological_space.opens β₯(projective_spectrum.Top π)) (i : V βΆ U) (s : β₯) (x : β₯V) :
.val x = s.val (βi x)
def algebraic_geometry.Proj.to_SheafedSpace {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] :

Proj of a graded ring as a SheafedSpace

Equations
def algebraic_geometry.open_to_localization {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯(projective_spectrum.Top π)) (hx : x β U) :

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
noncomputable def algebraic_geometry.stalk_to_fiber_ring_hom {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯(projective_spectrum.Top π)) :

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
@[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] [ A] (π : β β A) [graded_algebra π] (x : β₯U) :
@[simp]
theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯(projective_spectrum.Top π)) (hx : x β U) (s : β₯) :
@[simp]
theorem algebraic_geometry.stalk_to_fiber_ring_hom_germ {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯U) (s : β₯) :
theorem algebraic_geometry.homogeneous_localization.mem_basic_open {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯(projective_spectrum.Top π))  :
noncomputable def algebraic_geometry.section_in_basic_open {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯(projective_spectrum.Top π))  :

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
noncomputable def algebraic_geometry.homogeneous_localization_to_stalk {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯(projective_spectrum.Top π)) :

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
• = Ξ» (f : , f)
noncomputable def algebraic_geometry.Proj.stalk_iso' {R : Type u_1} {A : Type u_2} [comm_ring R] [comm_ring A] [ A] (π : β β A) [graded_algebra π] (x : β₯(projective_spectrum.Top π)) :

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

Proj of a graded ring as a LocallyRingedSpace

Equations