The structure sheaf on PrimeSpectrum R. #
We define the structure sheaf on TopCat.of (PrimeSpectrum 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 Mathlib/Topology/Sheaves/SheafOfFunctions.lean,
where we show that dependent functions into any type family form a sheaf,
and also Mathlib/Topology/Sheaves/LocalPredicate.lean, where we characterise the predicates
which pick out sub-presheaves and sub-sheaves of these sheaves.)
We also set up the ring structure, obtaining
structureSheaf : Sheaf CommRingCat (PrimeSpectrum.Top R).
We then construct two basic isomorphisms, relating the structure sheaf to the underlying ring R.
First, StructureSheaf.stalkIso 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,
StructureSheaf.basicOpenIso gives an isomorphism between the structure sheaf on basicOpen f
and the localization of R at the submonoid of powers of f.
References #
- [Robin Hartshorne, Algebraic Geometry][Har77]
The prime spectrum, just as a topological space.
Instances For
The type family over PrimeSpectrum R consisting of the localization over each point.
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
The predicate IsFraction is "prelocal",
in the sense that if it holds on U it holds on any open subset V of U.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
The functions satisfying isLocallyFraction form a subring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The structure sheaf (valued in Type, not yet CommRingCat) is the subsheaf consisting of
functions satisfying isLocallyFraction.
Equations
Instances For
The structure presheaf, valued in CommRingCat, constructed by dressing up the Type valued
structure presheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Some glue, verifying that the structure presheaf valued in CommRingCat agrees
with the Type valued structure presheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The structure sheaf on $Spec R$, valued in CommRingCat.
This is provided as a bundled SheafedSpace as Spec.SheafedSpace R later.
Equations
Instances For
The section of structureSheaf R on an open U sending each x ∈ U to the element
f/g in the localization of R at x.
Equations
Instances For
The canonical ring homomorphism interpreting an element of R as
a section of the structure sheaf.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical ring homomorphism interpreting an element of R as an element of
the stalk of structureSheaf R at x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The canonical ring homomorphism from the localization of R at p to the stalk
of the structure sheaf at the point p.
Equations
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
The ring homomorphism from the stalk of the structure sheaf of R at a point corresponding to
a prime ideal p to the localization of R at p,
formed by gluing the openToLocalization maps.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
The canonical ring homomorphism interpreting s ∈ R_f as a section of the structure sheaf
on the basic open defined by f ∈ R.
Instances For
The ring isomorphism between the structure sheaf on basicOpen f and the localization of R
at the submonoid of powers of f.
Equations
Instances For
Stalk of the structure sheaf at a prime p as localization of R
Sections of the structure sheaf of Spec R on a basic open as localization of R
The ring isomorphism between the ring R and the global sections Γ(X, 𝒪ₓ).
Equations
Instances For
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.localRingHom _ _ 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 isLocallyFraction is preserved by this map, hence it can be extended to
a morphism between the structure sheaves of R and S.
Equations
Instances For
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
- One or more equations did not get rendered due to their size.
Instances For
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 useful when U and V
are not definitionally equal.