Local sections as modules over global functions #
Restricting global functions to an open equips its sections with a common scalar ring.
Restriction maps are linear over that ring, so differences of restrictions and their
cokernels can be formed as modules, even when the opens have different coordinate rings.
For a scheme over a commutative ring, this action is compatible with that of the base ring
(AlgebraicGeometry.Scheme.Modules.isScalarTower_sections). Along a morphism over the base,
pushforwardSectionsBaseLinearEquiv identifies sections of a pushforward with those on the
preimage as modules over the base ring.
The sections of a sheaf of modules on a scheme over R are thus R-modules, and the restriction
maps are R-linear: this is the presheaf of R-modules
(Scheme.Modules.sectionsBasePresheafFunctor R).obj M. Its underlying presheaf of abelian groups
is the presheaf of sections (Scheme.Modules.sectionsBasePresheafCompForget₂Iso), and
multiplication by r : R on it is induced by multiplication by the global function r
(Scheme.Modules.sectionsBasePresheafFunctor_map_globalSectionsSmul).
For a family of opens V i covering W, restriction to the cover
(Scheme.Modules.sectionsRestrictPiBaseLinear) and the differences of restrictions to opens
containing the pairwise intersections (Scheme.Modules.sectionsDiffPiBaseLinear) are R-linear.
By the sheaf condition the first is injective and its image is the kernel of the second
(Scheme.Modules.sectionsRestrictPiBaseLinear_injective,
Scheme.Modules.exact_sectionsRestrictPiBaseLinear). In particular, sections are determined by
their restrictions to affine opens (Scheme.Modules.sections_ext_of_isAffineOpen).
Compatible families of sections of M are its global sections (Scheme.Modules.sectionsEquivTop),
and so are the morphisms 𝒪_X ⟶ M out of the structure sheaf (Scheme.Modules.unitHomEquivTop).
Sections over any open are a module over global functions, by restriction of scalars.
A global function acts on local sections by its restriction to the open.
Restriction of local sections is linear over global functions.
Instances For
For a scheme over a commutative ring R, global functions act on local sections compatibly
with R, where R acts on functions and on sections over U through
Scheme.baseRingToStructurePresheaf.
The action of R on the sections over W of a sheaf of modules on a scheme over R, through
Scheme.baseRingToStructurePresheaf, as in Scheme.Modules.isScalarTower_sections.
Instances For
Restriction of sections commutes with the action of the base ring through
Scheme.baseRingToStructurePresheaf.
The presheaf of sections of a sheaf of modules on a scheme over R, as a presheaf of
R-modules: the sections over W keep their carrier and restriction maps, and R acts through
Scheme.baseRingToStructurePresheaf (Scheme.Modules.sectionsBaseModule). The body is exposed
because the carrier of each object is Γ(M, W) by definition, which already the statements of
the application lemmas below rely on.
Instances For
The restriction maps of the presheaf of R-modules of sections are those of M.
A morphism of sheaves of modules acts on the presheaves of R-modules of sections by its
action on sections.
The identification sectionsBasePresheafCompForget₂Iso is natural in the sheaf of modules.
The identification sectionsBasePresheafCompForget₂Iso is natural in the sheaf of modules.
Multiplication by s : R on the presheaf of R-modules of sections is induced by the
multiplication by the global function s on the sheaf of modules.
The restrictions of the sections over W to a family of opens V i ≤ W, linear over the
base ring R, for any action of R on the sections over W through functions and for the action
through functions on the sections over each V i.
Instances For
The components of sectionsRestrictPiBaseLinear are the restriction maps.
A section over W is determined by its restrictions to a family of opens covering W.
The differences s (a p)|_{W' p} - s (b p)|_{W' p} of the restrictions of a family of sections
over the V i to opens W' p ≤ V (a p) ⊓ V (b p), linear over the base ring R acting through
functions.
Instances For
The components of sectionsDiffPiBaseLinear are differences of restrictions.
Families of sections over the V i whose restrictions agree on the opens W' p are exactly the
restrictions of the sections over W, when the V i cover W and every pairwise intersection
V i ⊓ V j lies in some W' p with a p = i and b p = j.
The base ring acts on sections of a pushforward over U as it acts on sections over the
preimage of U: pushforward restricts scalars along f.app U, which carries the image of the
base ring in Γ(Y, U) to its image in Γ(X, f ⁻¹ᵁ U).
The sections of a pushforward over an open have the same base-ring module structure as the sections on its preimage.
Instances For
Sections of an 𝒪_X-module over V agree if their restrictions to all affine opens contained
in V agree.
Compatible families of sections of M are its global sections: a family goes to its section
over X, and a global section to the family of its restrictions.
Instances For
Applying p : M ⟶ N to a compatible family of sections applies p to its global section.
Morphisms 𝒪_X ⟶ M out of the structure sheaf are the global sections of M: a morphism
goes to the image of 1 over X. This is Mathlib's SheafOfModules.unitHomEquiv, followed by
the evaluation of a compatible family of sections at the terminal open X
(Scheme.Modules.sectionsEquivTop).
Instances For
Composing a morphism 𝒪_X ⟶ M with p : M ⟶ N applies p to the corresponding global
section.