Sections of quasi-coherent modules over basic opens #
Let M be a quasi-coherent 𝒪_X-module on a scheme X, let U be an affine open of X and
let f ∈ Γ(X, U). Then the sections of M over the basic open X.basicOpen f are the
localization of the sections over U at the powers of f: the restriction map
Γ(M, U) ⟶ Γ(M, X.basicOpen f) is a localization of Γ(X, U)-modules. This is the module
counterpart of AlgebraicGeometry.IsAffineOpen.isLocalization_basicOpen for the structure sheaf.
This is the affine-local description of quasi-coherent modules needed to build objects over X
from their sections over affine opens. For instance, it is the condition making a quasi-coherent
sheaf of algebras coequifibered over the structure sheaf on the small affine Zariski site, which
is the input of AlgebraicGeometry.AffineZariskiSite.relativeGluingData.
Over Spec R the statement is Mathlib's AlgebraicGeometry.isIso_fromTildeΓ_iff_isLocalizing;
this module extends that affine result to arbitrary schemes.
Main declarations #
AlgebraicGeometry.Scheme.Modules.moduleBasicOpen: forf ∈ Γ(X, U), the sectionsΓ(M, X.basicOpen f)form aΓ(X, U)-module by restriction of scalars;AlgebraicGeometry.Scheme.Modules.basicOpenRestrict: the restriction mapΓ(M, U) ⟶ Γ(M, X.basicOpen f)as aΓ(X, U)-linear map;AlgebraicGeometry.Scheme.Modules.isLocalizedModule_basicOpenRestrict: for quasi-coherentMand affineU, this restriction map is the localization at the powers off.
References #
- R. Hartshorne, Algebraic Geometry, Lemma II.5.3.
- A. Grothendieck and J. Dieudonné, Éléments de géométrie algébrique I (1971), Théorème 1.4.1.
For f ∈ Γ(X, U), the sections of an 𝒪_X-module over X.basicOpen f form a
Γ(X, U)-module by restriction of scalars along Γ(X, U) ⟶ Γ(X, X.basicOpen f).
Equations
- M.moduleBasicOpen f = Module.compHom (↑(M.presheaf.obj (Opposite.op (X.basicOpen f)))) (algebraMap ↑(X.presheaf.obj (Opposite.op U)) ↑(X.presheaf.obj (Opposite.op (X.basicOpen f))))
The Γ(X, U)-module structure on Γ(M, X.basicOpen f) factors through
Γ(X, X.basicOpen f).
The restriction of sections of an 𝒪_X-module from U to X.basicOpen f, as a
Γ(X, U)-linear map.
Equations
- M.basicOpenRestrict f = { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)), map_add' := ⋯, map_smul' := ⋯ }
Instances For
For an affine open U, the sections of an 𝒪_X-module M over U are the global sections
of its restriction to the affine chart Spec Γ(X, U) ⟶ X, as Γ(X, U)-modules. Here
Γ(X, U) acts on the global sections of a module on Spec Γ(X, U) as their ring of
global functions.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The identification Γ(M, U) ≃ Γ(M.restrict hU.fromSpec, ⊤) is restriction of sections to
the image of the affine chart, which is U.
The sections of a quasi-coherent 𝒪_X-module over the basic open X.basicOpen f of an
affine open U are the localization of its sections over U at the powers of f.