Pushforward of sheaves of modules

Assume that categories C and D are equipped with Grothendieck topologies, and that F : C ⥤ D is a continuous functor. Then, if φ : S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R is a morphism of sheaves of rings, we construct the pushforward functor pushforward φ : SheafOfModules.{v} R ⥤ SheafOfModules.{v} S, and we show that they interact with the composition of morphisms similarly as pseudofunctors.

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

The pushforward of sheaves of modules that is induced by a continuous functor F and a morphism of sheaves of rings φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R.

Equations

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

@[simp]

theorem SheafOfModules.pushforward_obj_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (M : SheafOfModules R) : ((pushforward φ).obj M).val = (PresheafOfModules.pushforward φ.val).obj M.val

@[simp]

theorem SheafOfModules.pushforward_map_val {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {X✝ Y✝ : SheafOfModules R} (f : X✝ ⟶ Y✝) : ((pushforward φ).map f).val = (PresheafOfModules.pushforward φ.val).map f.val

@[reducible, inline]

noncomputable abbrev SheafOfModules.over {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {R : CategoryTheory.Sheaf K RingCat} (M : SheafOfModules R) (X : D) : SheafOfModules (R.over X)

Given M : SheafOfModules R and X : D, this is the restriction of M over the sheaf of rings R.over X on the category Over X.

Equations

• M.over X = (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).obj R))).obj M

noncomputable def SheafOfModules.pushforwardId {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (R : CategoryTheory.Sheaf K RingCat) : pushforward (CategoryTheory.CategoryStruct.id R) ≅ CategoryTheory.Functor.id (SheafOfModules R)

The pushforward functor by the identity morphism identifies to the identify functor of the category of sheaves of modules.

Equations

• SheafOfModules.pushforwardId R = CategoryTheory.Iso.refl (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id R))

noncomputable def SheafOfModules.pushforwardComp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {D' : Type u₃} [CategoryTheory.Category.{v₃, u₃} D'] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {K' : CategoryTheory.GrothendieckTopology D'} {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [G.IsContinuous K K'] [G.IsContinuous K K'] [(F.comp G).IsContinuous J K'] [(F.comp G).IsContinuous J K'] (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') : (pushforward ψ).comp (pushforward φ) ≅ pushforward (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))

The composition of two pushforward functors on categories of sheaves of modules identify to the pushforward for the composition.

Equations

• SheafOfModules.pushforwardComp φ ψ = CategoryTheory.Iso.refl ((SheafOfModules.pushforward ψ).comp (SheafOfModules.pushforward φ))

theorem SheafOfModules.pushforward_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {D' : Type u₃} [CategoryTheory.Category.{v₃, u₃} D'] {D'' : Type u₄} [CategoryTheory.Category.{v₄, u₄} D''] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {K' : CategoryTheory.GrothendieckTopology D'} {K'' : CategoryTheory.GrothendieckTopology D''} {G : CategoryTheory.Functor D D'} {R' : CategoryTheory.Sheaf K' RingCat} [G.IsContinuous K K'] [G.IsContinuous K K'] [(F.comp G).IsContinuous J K'] [(F.comp G).IsContinuous J K'] (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') {G' : CategoryTheory.Functor D' D''} {R'' : CategoryTheory.Sheaf K'' RingCat} [G'.IsContinuous K' K''] [G'.IsContinuous K' K''] [(G.comp G').IsContinuous K K''] [(G.comp G').IsContinuous K K''] [((F.comp G).comp G').IsContinuous J K''] [((F.comp G).comp G').IsContinuous J K''] [(F.comp (G.comp G')).IsContinuous J K''] [(F.comp (G.comp G')).IsContinuous J K''] (ψ' : R' ⟶ (G'.sheafPushforwardContinuous RingCat K' K'').obj R'') : (pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ)) ψ' = ((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫ pushforwardComp φ (CategoryTheory.CategoryStruct.comp ψ ((G.sheafPushforwardContinuous RingCat K K').map ψ'))

theorem SheafOfModules.pushforward_comp_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) : pushforwardComp (CategoryTheory.CategoryStruct.id S) φ = (pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor

theorem SheafOfModules.pushforward_id_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) : pushforwardComp φ (CategoryTheory.CategoryStruct.id R) = CategoryTheory.Functor.isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor