Restriction maps of a sheaf of modules #
For a sheaf of 𝒪_X-modules F (Mathlib's X.Modules) and opens U ≤ V, the restriction
Γ(F, V) → Γ(F, U) is semilinear along the restriction of functions Γ(X, V) → Γ(X, U):
AlgebraicGeometry.Scheme.Modules.restrictionMap. These are the transition maps of the modules
of sections over the affine opens from which the projective bundle P(F) of a quasi-coherent
sheaf is glued [TSPA, Tag 01OB].
noncomputable def
AlgebraicGeometry.Scheme.Modules.restrictionMap
{X : Scheme}
(F : X.Modules)
{U V : X.Opens}
(h : U ≤ V)
:
↑(F.presheaf.obj (Opposite.op V)) →ₛₗ[CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)] ↑(F.presheaf.obj (Opposite.op U))
The restriction map Γ(F, V) → Γ(F, U) of a sheaf of modules, for opens U ≤ V, as a map
semilinear along the restriction of functions Γ(X, V) → Γ(X, U).
Equations
- F.restrictionMap h = { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (F.presheaf.map (CategoryTheory.homOfLE h).op)), map_add' := ⋯, map_smul' := ⋯ }