A module sheaf viewed over a fixed base ring

Given R → Γ(Y, 𝒪_Y), every section module of an 𝒪_Y-module is an R-module, compatibly with restriction. This keeps the sheaf condition in ModuleCat R, so its two-open pullback cone can subsequently be localized.

This is an underived change of scalars. It supplies neither a comparison with sections after scheme base change nor a derived global-sections theorem.

noncomputable def AlgebraicGeometry.modulesToFixedBaseSheaf {R : CommRingCat} (Y : Scheme) (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) : CategoryTheory.Functor Y.Modules (TopCat.Sheaf (ModuleCat ↑R) ↑Y.toPresheafedSpace)

View an 𝒪_Y-module sheaf as a sheaf of modules over a fixed ring R, using R → Γ(Y, 𝒪_Y). The sheaf and all its restriction maps are retained.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.modulesToFixedBaseSheaf_smul {R : CommRingCat} (Y : Scheme) (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (M : Y.Modules) (U : Y.Opens) (r : ↑R) (x : ↑(((modulesToFixedBaseSheaf Y φ).obj M).presheaf.obj (Opposite.op U))) : r • x = (AddCommGrpCat.Hom.hom (Scheme.Modules.smul ((CategoryTheory.ConcreteCategory.hom (Y.presheaf.map (TopologicalSpace.Opens.leTop U).op)) ((CommRingCat.Hom.hom φ) r)))) x

The fixed R-action is the original 𝒪_Y(U)-action after restricting φ(r) from the whole scheme to U.

noncomputable def AlgebraicGeometry.fixedBaseSectionsFunctor {R : CommRingCat} (Y : Scheme) (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (U : Y.Opens) : CategoryTheory.Functor Y.Modules (ModuleCat ↑R)

Sections on an open as R-modules, obtained by evaluating the fixed-base sheaf.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.fixedBaseSectionsTwoOpenLimit {R : CommRingCat} (Y : Scheme) (φ : R ⟶ Y.presheaf.obj (Opposite.op ⊤)) (M : Y.Modules) (U V : Y.Opens) : CategoryTheory.Limits.IsLimit (((modulesToFixedBaseSheaf Y φ).obj M).interUnionPullbackCone U V)

The sheaf condition for two opens, in ModuleCat R. This is the exact pullback cone to which flat localization can later be applied.

Equations

• AlgebraicGeometry.fixedBaseSectionsTwoOpenLimit Y φ M U V = ((AlgebraicGeometry.modulesToFixedBaseSheaf Y φ).obj M).isLimitPullbackCone U V