Sections of a quasi-coherent sheaf over affine opens #
For a quasi-coherent sheaf of modules F on a scheme X (Mathlib's X.Modules with
IsQuasicoherent):
- over a basic open
D(r)of an affine openV, the restrictionΓ(F, V) → Γ(F, D(r))is the localization at the powers ofr[TSPA, Tags 01I9 and 01IA] (AlgebraicGeometry.Scheme.Modules.isLocalizedModule_resₗ_basicOpen). This is Mathlib'sisIso_fromTildeΓ_of_isQuasicoherent(a quasi-coherent sheaf onSpec RisM^~) for the restriction ofFalongSpec Γ(X, V) ≅ V, read onX: the sections of the restriction are the sections ofF(Scheme.Modules.restrict_obj), and theΓ(X, V)-action on them is the restriction of functions (fromSpec_appIso_inv); - for affine opens
U ≤ V,Γ(F, U)is the base changeΓ(X, U) ⊗_{Γ(X, V)} Γ(F, V)[TSPA, Tags 01I9 and 01IA] (isBaseChange_resₗ): both sides localize toΓ(F, D(r))at the basic opensD(r) ⊆ UofV, which coverU. Consequently the image ofΓ(F, V)spansΓ(F, U)(span_range_restrictionMap_eq_top), and every semilinear map out ofΓ(F, V)extends to aΓ(X, U)-linear map out ofΓ(F, U)(exists_extend_restrictionMap): the hypotheses of the base change of the projective bundle of a module (affineProjectiveBundle.isPullback_map).
The ring identity behind the restriction to an affine open: the Γ(X, V)-action on the
sections of F.restrict hV.fromSpec over W is the restriction.
The restriction Γ(F, V) → Γ(F, U) as a Γ(X, V)-linear map, Γ(F, U) a Γ(X, V)-module
through the restriction of functions.
Equations
- F.resₗ h = { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE h).op)), map_add' := ⋯, map_smul' := ⋯ }
Instances For
The sections of F over an affine open V are the global sections of the restriction of F
to Spec Γ(X, V) ≅ V, as Γ(X, V)-modules.
Equations
- F.topSectionsEquiv hV = LinearEquiv.ofBijective { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE ⋯).op)), map_add' := ⋯, map_smul' := ⋯ } ⋯
Instances For
The restriction to a basic open D(r) of an affine open V is a localization on X if and
only if it is one for the restriction of F to Spec Γ(X, V) ≅ V, the condition of Mathlib's
isIso_fromTildeΓ_iff_isLocalizing: the two restriction maps are identified by the restrictions
of F along Spec Γ(X, V) ≅ V, and the actions of Γ(X, V) by fromSpec_appIso_inv.
Sections of a quasi-coherent module over a basic open are a localization: for an affine
open V and r ∈ Γ(X, V), the restriction Γ(F, V) → Γ(F, D(r)) is the localization at the
powers of r [TSPA, Tags 01I9 and 01IA]. This is Mathlib's isIso_fromTildeΓ_of_isQuasicoherent
for the restriction of F to Spec Γ(X, V) ≅ V, read on X.
isLocalizedModule_resₗ_basicOpen for an open given as equal to the basic open.
IsAffineOpen.isLocalization_basicOpen for an open given as equal to the basic open.
The sections of a quasi-coherent module over nested affine opens U ≤ V: Γ(F, U) is the
base change Γ(X, U) ⊗_{Γ(X, V)} Γ(F, V) [TSPA, Tags 01I9 and 01IA]. Both sides are localizations of
Γ(F, V) at the basic opens D(r) ⊆ U of V (isLocalizedModule_resₗ_basicOpen, applied to V
and to U, where D(r) is the basic open of the restriction of r), and these cover U; a map of
modules that is bijective after localizing at a family generating the unit ideal is bijective
(Mathlib's bijective_of_isLocalized_span).
For affine opens U ≤ V of X, the restrictions of the sections of a quasi-coherent sheaf
over V span its sections over U (isBaseChange_resₗ).
For affine opens U ≤ V of X, every map out of the sections of a quasi-coherent sheaf over
V, semilinear along the restriction Γ(X, V) → Γ(X, U), extends along the restriction to a
Γ(X, U)-linear map out of the sections over U (isBaseChange_resₗ).