mathlib3 documentation

algebraic_geometry.structure_sheaf

The structure sheaf on prime_spectrum R. #

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

We define the structure sheaf on Top.of (prime_spectrum R), for a commutative ring R and prove basic properties about it. We define this as a subsheaf of the sheaf of dependent functions into the localizations, cut out by the condition that the function must be locally equal to a ratio of elements of R.

Because the condition "is equal to a fraction" passes to smaller open subsets, the subset of functions satisfying this condition is automatically a subpresheaf. Because the condition "is locally equal to a fraction" is local, it is also a subsheaf.

(It may be helpful to refer back to topology.sheaves.sheaf_of_functions, where we show that dependent functions into any type family form a sheaf, and also topology.sheaves.local_predicate, where we characterise the predicates which pick out sub-presheaves and sub-sheaves of these sheaves.)

We also set up the ring structure, obtaining structure_sheaf R : sheaf CommRing (Top.of (prime_spectrum R)).

We then construct two basic isomorphisms, relating the structure sheaf to the underlying ring R. First, structure_sheaf.stalk_iso gives an isomorphism between the stalk of the structure sheaf at a point p and the localization of R at the prime ideal p. Second, structure_sheaf.basic_open_iso gives an isomorphism between the structure sheaf on basic_open f and the localization of R at the submonoid of powers of f.

References #

The prime spectrum, just as a topological space.

Equations

The predicate saying that a dependent function on an open U is realised as a fixed fraction r / s 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, localizations R x consisting of those functions which can locally be expressed as a ratio of (the images in the localization of) elements of R.

Quoting Hartshorne:

For an open set $U ⊆ Spec A$, we define $𝒪(U)$ to be the set of functions $s : U → ⨆_{𝔭 ∈ U} A_𝔭$, such that $s(𝔭) ∈ A_𝔭$ for each $𝔭$, and such that $s$ is locally a quotient of elements of $A$: to be precise, we require that for each $𝔭 ∈ U$, there is a neighborhood $V$ of $𝔭$, contained in $U$, and elements $a, f ∈ A$, such that for each $𝔮 ∈ V, f ∉ 𝔮$, and $s(𝔮) = a/f$ in $A_𝔮$.

Now Hartshorne had the disadvantage of not knowing about dependent functions, so we replace his circumlocution about functions into a disjoint union with Π x : U, localizations x.

Equations

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

Equations

The structure sheaf on $Spec R$, valued in CommRing.

This is provided as a bundled SheafedSpace as Spec.SheafedSpace R later.

Equations

The section of structure_sheaf R on an open U sending each x ∈ U to the element f/g in the localization of R at x.

Equations

The canonical ring homomorphism interpreting an element of R as an element of the stalk of structure_sheaf R at x.

Equations

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

Equations

The ring isomorphism between the stalk of the structure sheaf of R at a point p corresponding to a prime ideal in R and the localization of R at p.

Equations

The canonical ring homomorphism interpreting s ∈ R_f as a section of the structure sheaf on the basic open defined by f ∈ R.

Equations
Instances for algebraic_geometry.structure_sheaf.to_basic_open
theorem algebraic_geometry.structure_sheaf.normalize_finite_fraction_representation (R : Type u) [comm_ring R] (U : topological_space.opens (algebraic_geometry.prime_spectrum.Top R)) (s : ((algebraic_geometry.Spec.structure_sheaf R).val.obj (opposite.op U))) {ι : Type u_1} (t : finset ι) (a h : ι R) (iDh : Π (i : ι), prime_spectrum.basic_open (h i) U) (h_cover : U (i : ι) (H : i t), prime_spectrum.basic_open (h i)) (hs : (i : ι), algebraic_geometry.structure_sheaf.const R (a i) (h i) (prime_spectrum.basic_open (h i)) _ = ((algebraic_geometry.Spec.structure_sheaf R).val.map (iDh i).op) s) :
(a' h' : ι R) (iDh' : Π (i : ι), prime_spectrum.basic_open (h' i) U), (U (i : ι) (H : i t), prime_spectrum.basic_open (h' i)) ( (i : ι), i t (j : ι), j t a' i * h' j = h' i * a' j) (i : ι), i t ((algebraic_geometry.Spec.structure_sheaf R).val.map (iDh' i).op) s = algebraic_geometry.structure_sheaf.const R (a' i) (h' i) (prime_spectrum.basic_open (h' i)) _
@[protected, instance]

Stalk of the structure sheaf at a prime p as localization of R

@[protected, instance]

Sections of the structure sheaf of Spec R on a basic open as localization of R

Given a ring homomorphism f : R →+* S, an open set U of the prime spectrum of R and an open set V of the prime spectrum of S, such that V ⊆ (comap f) ⁻¹' U, we can push a section s on U to a section on V, by composing with localization.local_ring_hom _ _ f from the left and comap f from the right. Explicitly, if s evaluates on comap f p to a / b, its image on V evaluates on p to f(a) / f(b).

At the moment, we work with arbitrary dependent functions s : Π x : U, localizations R x. Below, we prove the predicate is_locally_fraction is preserved by this map, hence it can be extended to a morphism between the structure sheaves of R and S.

Equations

For a ring homomorphism f : R →+* S and open sets U and V of the prime spectra of R and S such that V ⊆ (comap f) ⁻¹ U, the induced ring homomorphism from the structure sheaf of R at U to the structure sheaf of S at V.

Explicitly, this map is given as follows: For a point p : V, if the section s evaluates on p to the fraction a / b, its image on V evaluates on p to the fraction f(a) / f(b).

Equations

For an inclusion i : V ⟶ U between open sets of the prime spectrum of R, the comap of the identity from OO_X(U) to OO_X(V) equals as the restriction map of the structure sheaf.

This is a generalization of the fact that, for fixed U, the comap of the identity from OO_X(U) to OO_X(U) is the identity.

The comap of the identity is the identity. In this variant of the lemma, two open subsets U and V are given as arguments, together with a proof that U = V. This is be useful when U and V are not definitionally equal.