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 #

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

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

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