Pushforward of sheaves of modules on underlying presheaves

Let F : C ⥤ D be a continuous functor between sites, R and S sheaves of commutative rings on D and C, and φ : S ⟶ F_* R a morphism of the underlying sheaves of rings. This file records the data underlying the pushforward SheafOfModules.pushforward φ of sheaves of modules that sectionwise constructions transfer along: the morphism of presheaves of commutative rings underlying φ, and the pushforward of the underlying presheaves of modules.

Main declarations

• SheafOfModules.commRingCatHom: the morphism of presheaves of commutative rings underlying φ, computed on sections by SheafOfModules.commRingCatHom_app;
• SheafOfModules.presheafPushforward: the pushforward of presheaves of modules underlying the pushforward of sheaves of modules;
• SheafOfModules.forget_map_pushforward_map: on underlying presheaves, the pushforward of a morphism of sheaves of modules is the pushforward of the underlying morphism.

def TauCeti.SheafOfModules.commRingCatHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {F : CategoryTheory.Functor C D} [F.IsContinuous J K] {S : CategoryTheory.Sheaf J CommRingCat} {R : CategoryTheory.Sheaf K CommRingCat} (φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)) : S.obj ⟶ F.op.comp R.obj

The morphism of presheaves of commutative rings underlying φ. Its body is exposed so that sectionwise constructions over presheaves of commutative rings, pushed forward along it, are pushforwards along φ.hom.

@[simp]

theorem TauCeti.SheafOfModules.commRingCatHom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {F : CategoryTheory.Functor C D} [F.IsContinuous J K] {S : CategoryTheory.Sheaf J CommRingCat} {R : CategoryTheory.Sheaf K CommRingCat} (φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)) (U : Cᵒᵖ) : (commRingCatHom φ).app U = CommRingCat.ofHom (RingCat.Hom.hom (φ.hom.app U))

On sections over U, the morphism of presheaves of commutative rings underlying φ is the ring map φ.hom.app U.

noncomputable def TauCeti.SheafOfModules.presheafPushforward {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {F : CategoryTheory.Functor C D} [F.IsContinuous J K] {S : CategoryTheory.Sheaf J CommRingCat} {R : CategoryTheory.Sheaf K CommRingCat} (φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)) : CategoryTheory.Functor (PresheafOfModules (ringCatSheaf R).obj) (PresheafOfModules (ringCatSheaf S).obj)

The pushforward of presheaves of modules underlying SheafOfModules.pushforward φ. It is Mathlib's PresheafOfModules.pushforward φ.hom, with source and target written as presheaves of modules over the presheaves of rings (ringCatSheaf R).obj and (ringCatSheaf S).obj, so that it composes with SheafOfModules.forget and with sheafification.

theorem TauCeti.SheafOfModules.forget_map_pushforward_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} [K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] {F : CategoryTheory.Functor C D} [F.IsContinuous J K] {S : CategoryTheory.Sheaf J CommRingCat} {R : CategoryTheory.Sheaf K CommRingCat} (φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R)) {M N : SheafOfModules (ringCatSheaf R)} (f : M ⟶ N) : (SheafOfModules.forget (ringCatSheaf S)).map ((SheafOfModules.pushforward φ).map f) = (presheafPushforward φ).map ((SheafOfModules.forget (ringCatSheaf R)).map f)

On underlying presheaves of modules, the pushforward of a morphism of sheaves of modules is the pushforward of the underlying morphism of presheaves.