Presheaves of modules on a spectrum with scalars restricted to the base ring

Restricting section scalars along R ≅ Γ(Spec R, ⊤) turns a presheaf of modules on Spec R into a presheaf of R-modules. This is the presheaf counterpart of AlgebraicGeometry.modulesSpecToSheaf, used in affine comparisons before sheafification. The maps from a module to the sections of its associated sheaf form a natural transformation from the constant presheaf.

@[reducible, inline]

noncomputable abbrev TauCeti.AlgebraicGeometry.specPresheafFunctor {R : CommRingCat} : CategoryTheory.Functor (PresheafOfModules (AlgebraicGeometry.Spec R).ringCatSheaf.obj) (CategoryTheory.Functor (AlgebraicGeometry.Spec R).Opensᵒᵖ (ModuleCat ↑R))

Restrict the scalars of a presheaf of modules on Spec R to R, retaining its section carriers and restriction maps. The abbreviation exposes these carriers so that sectionwise constructions use the original module instances.

noncomputable def TauCeti.AlgebraicGeometry.tildeToOpenNatTrans {R : CommRingCat} (M : ModuleCat ↑R) : (CategoryTheory.Functor.const (AlgebraicGeometry.Spec R).Opensᵒᵖ).obj M ⟶ (AlgebraicGeometry.modulesSpecToSheaf.obj (AlgebraicGeometry.tilde M)).obj

The maps from a module to the sections of its associated sheaf, natural in the open.

@[simp]

theorem TauCeti.AlgebraicGeometry.tildeToOpenNatTrans_app {R : CommRingCat} (M : ModuleCat ↑R) (U : (AlgebraicGeometry.Spec R).Opensᵒᵖ) : (tildeToOpenNatTrans M).app U = AlgebraicGeometry.tilde.toOpen M (Opposite.unop U)

Each component of the natural transformation to sections is the associated-section map.