mathlib documentation

algebraic_geometry.projective_spectrum.structure_sheaf

The structure sheaf on projective_spectrum π’œ. #

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 #

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

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

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

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

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

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

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
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 π’œ] :

Proj of a graded ring as a LocallyRingedSpace

Equations