The structure sheaf on PrimeSpectrum R. #
We define the structure sheaf on TopCat.of (PrimeSpectrum R), for an R-module M 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 quotient of
an element of M by an element 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.)
When M = R, the structure sheaf is furthermore a sheaf of commutative rings, which we bundle as
structureSheaf : Sheaf CommRingCat (PrimeSpectrum.Top R).
We then obtain two key descriptions of the structure sheaf. We show that the stalks Mₓ is the
localization of M at the prime corresponding to x, and we show that the sections Γ(M, D(f))
is the localization of M away from f.
Note that the results of this file are packaged into schemes and sheaf of modules in later files, and one usually should not directly use the results in this file to respect the abstraction boundaries.
References #
- [Robin Hartshorne, Algebraic Geometry][Har77]
The type family over PrimeSpectrum R consisting of the localization over each point.
Equations
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
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
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 submodule.
Equations
Instances For
The functions satisfying isLocallyFraction form a subalgebra.
Equations
Instances For
The functions satisfying isLocallyFraction form a submodule.
Equations
Instances For
The structure sheaf (valued in Type, not yet CommRingCat) is the subsheaf consisting of
functions satisfying isLocallyFraction.
Equations
Instances For
Equations
Equations
Equations
Equations
The structure presheaf, valued in ModuleCat, constructed by dressing up the Type-valued
structure presheaf.
Equations
Instances For
The structure presheaf, valued in CommRingCat, constructed by dressing up the Type-valued
structure presheaf.
Equations
Instances For
Equations
The structure sheaf of a module as a presheaf of modules on Spec R.
We will later package this into a Scheme.Modules in Tilde.lean.
Equations
Instances For
Some glue, verifying that the structure presheaf valued in CommRingCat agrees
with the Type-valued structure presheaf.
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 linear map interpreting an element of M as
a section of the structure sheaf.
Equations
Instances For
The canonical ring homomorphism interpreting an element of R as an element of
the stalk of structureSheaf R at x.
Equations
Instances For
Equations
Equations
The canonical ring homomorphism interpreting an element of R as an element of
the stalk of structureSheaf R at x.
Equations
Instances For
The stalk of Spec R at x is isomorphic to the stalk of R^~ at x.
Equations
Instances For
The stalk of Spec R at x is isomorphic to Rₚ,
where p is the prime corresponding to x.
Equations
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 canonical ring homomorphism interpreting an element of R as
a section of the structure sheaf.
Equations
Instances For
Alias of AlgebraicGeometry.StructureSheaf.algebraMap_self_map.
Equations
Stalk of the structure sheaf at a prime p as localization of R
Equations
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
The map M_{f y} ⟶ N_{y} used to build maps between structure sheaves.
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
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
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.