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.

@[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

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

@[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.

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.

noncomputable def SheafOfModules.pushforwardCongr {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} (e : φ = ψ) : pushforward φ ≅ pushforward ψ

Pushforwards along equal morphisms of sheaves of rings are isomorphic.

@[simp]

theorem SheafOfModules.pushforwardCongr_symm {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} (e : φ = ψ) : (pushforwardCongr e).symm = pushforwardCongr ⋯

@[simp]

theorem SheafOfModules.pushforwardCongr_hom_app_val_app {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} (e : φ = ψ) (M : SheafOfModules R) (U : Cᵒᵖ) (x : ↑(((pushforward φ).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardCongr e).hom.app M).val.app U)) x = x

@[simp]

theorem SheafOfModules.pushforwardCongr_inv_app_val_app {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} (e : φ = ψ) (M : SheafOfModules R) (U : Cᵒᵖ) (x : ↑(((pushforward ψ).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardCongr e).inv.app M).val.app U)) x = x

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.

theorem SheafOfModules.pushforwardComp_hom_app_val_app {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') (M : SheafOfModules R') (U : Cᵒᵖ) (x : ↑((((pushforward ψ).comp (pushforward φ)).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardComp φ ψ).hom.app M).val.app U)) x = x

theorem SheafOfModules.pushforwardComp_inv_app_val_app {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') (M : SheafOfModules R') (U : Cᵒᵖ) (x : ↑(((pushforward (CategoryTheory.CategoryStruct.comp φ ((F.sheafPushforwardContinuous RingCat J K).map ψ))).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardComp φ ψ).inv.app M).val.app U)) x = x

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

noncomputable def SheafOfModules.pushforwardNatTrans {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 G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous J K] [G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) (α : F ⟶ G) : pushforward φ ⟶ pushforward (CategoryTheory.CategoryStruct.comp φ ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans α RingCat J K).app S))

A natural transformation gives a natural transformation between the pushforward functors.

@[simp]

theorem SheafOfModules.pushforwardNatTrans_app_val_app {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 G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous J K] [G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) (α : F ⟶ G) (M : SheafOfModules S) (U : Cᵒᵖ) (x : ↑(((pushforward φ).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardNatTrans φ α).app M).val.app U)) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (α.app (Opposite.unop U)).op)) x

@[simp]

theorem SheafOfModules.pushforwardNatTrans_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} {G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [G.IsContinuous J K] [G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) : pushforwardNatTrans φ (CategoryTheory.CategoryStruct.id G) = (pushforwardCongr ⋯).hom

@[simp]

theorem SheafOfModules.pushforwardNatTrans_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 G H : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous J K] [G.IsContinuous J K] [H.IsContinuous J K] [H.IsContinuous J K] (α : F ⟶ G) (β : G ⟶ H) (φ : T ⟶ (H.sheafPushforwardContinuous RingCat J K).obj S) : pushforwardNatTrans φ (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (pushforwardNatTrans φ β) (CategoryTheory.CategoryStruct.comp (pushforwardNatTrans (CategoryTheory.CategoryStruct.comp φ ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans β RingCat J K).app S)) α) (pushforwardCongr ⋯).hom)

@[simp]

theorem SheafOfModules.pushforwardNatTrans_app_val_app_apply {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 G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous J K] [G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) (α : F ⟶ G) (X : SheafOfModules S) (U : Cᵒᵖ) (x : ↑(((pushforward φ).obj X).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardNatTrans φ α).app X).val.app U)) x = (CategoryTheory.ConcreteCategory.hom (X.val.map (α.app (Opposite.unop U)).op)) x

noncomputable def SheafOfModules.pushforwardNatIso {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 G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous J K] [G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) (α : F ≅ G) : pushforward φ ≅ pushforward (CategoryTheory.CategoryStruct.comp φ ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S))

A natural isomorphism gives a natural isomorphism between the pushforward functors.

@[simp]

theorem SheafOfModules.pushforwardNatIso_hom {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 G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous J K] [G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) (α : F ≅ G) : (pushforwardNatIso φ α).hom = pushforwardNatTrans φ α.hom

@[simp]

theorem SheafOfModules.pushforwardNatIso_inv {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 G : CategoryTheory.Functor C D} {T : CategoryTheory.Sheaf J RingCat} {S : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous J K] [G.IsContinuous J K] (φ : T ⟶ (G.sheafPushforwardContinuous RingCat J K).obj S) (α : F ≅ G) : (pushforwardNatIso φ α).inv = CategoryTheory.CategoryStruct.comp (pushforwardNatTrans (CategoryTheory.CategoryStruct.comp φ ((CategoryTheory.Functor.sheafPushforwardContinuousNatTrans α.hom RingCat J K).app S)) α.inv) (pushforwardCongr ⋯).hom

noncomputable def SheafOfModules.pushforwardPushforwardAdj {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} {G : CategoryTheory.Functor D C} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous K J] [G.IsContinuous K J] (adj : F ⊣ G) (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S) (H₁ : CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) R.val = CategoryTheory.CategoryStruct.comp ψ.val (G.op.whiskerLeft φ.val)) (H₂ : CategoryTheory.CategoryStruct.comp φ.val (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.val) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.val)) = CategoryTheory.CategoryStruct.id S.val) : pushforward φ ⊣ pushforward ψ

If F ⊣ G, then the pushforwards along F and G are also adjoint.

theorem SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app {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} {G : CategoryTheory.Functor D C} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous K J] [G.IsContinuous K J] (adj : F ⊣ G) (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S) (H₁ : CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) R.val = CategoryTheory.CategoryStruct.comp ψ.val (G.op.whiskerLeft φ.val)) (H₂ : CategoryTheory.CategoryStruct.comp φ.val (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.val) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.val)) = CategoryTheory.CategoryStruct.id S.val) (M : SheafOfModules R) (U : Dᵒᵖ) (x : ↑(((CategoryTheory.Functor.id (SheafOfModules R)).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardPushforwardAdj adj φ ψ H₁ H₂).unit.app M).val.app U)) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (adj.counit.app (Opposite.unop U)).op)) x

theorem SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app {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} {G : CategoryTheory.Functor D C} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [F.IsContinuous J K] [F.IsContinuous J K] [G.IsContinuous K J] [G.IsContinuous K J] (adj : F ⊣ G) (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K J).obj S) (H₁ : CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.counit) R.val = CategoryTheory.CategoryStruct.comp ψ.val (G.op.whiskerLeft φ.val)) (H₂ : CategoryTheory.CategoryStruct.comp φ.val (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.val) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.val)) = CategoryTheory.CategoryStruct.id S.val) (M : SheafOfModules S) (U : Cᵒᵖ) (x : ↑((((pushforward ψ).comp (pushforward φ)).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardPushforwardAdj adj φ ψ H₁ H₂).counit.app M).val.app U)) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (adj.unit.app (Opposite.unop U)).op)) x

def SheafOfModules.pushforwardOver {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C) : R ⟶ ((CategoryTheory.Over.star x).sheafPushforwardContinuous RingCat J (J.over x)).obj (R.over x)

The canonical morphism from R to the pushforward of its restriction to Over x.

def SheafOfModules.overPushforwardOverAdj {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C) : pushforward (CategoryTheory.CategoryStruct.id (R.over x)) ⊣ pushforward (pushforwardOver x)

The adjunction between restriction to Over x and pushforward along Over.star x.

instance SheafOfModules.instIsLeftAdjointOverOverRingCatPushforwardIdSheafOver {C : Type u'} [CategoryTheory.Category.{v', u'} C] [CategoryTheory.Limits.HasBinaryProducts C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} (x : C) : (pushforward (CategoryTheory.CategoryStruct.id (R.over x))).IsLeftAdjoint

noncomputable def SheafOfModules.pushforwardPushforwardEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} (eqv : C ≌ D) {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [eqv.functor.IsContinuous J K] [eqv.functor.IsContinuous J K] [eqv.inverse.IsContinuous K J] [eqv.inverse.IsContinuous K J] (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S) (H₁ : CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.counit) R.val = CategoryTheory.CategoryStruct.comp ψ.val (eqv.inverse.op.whiskerLeft φ.val)) (H₂ : CategoryTheory.CategoryStruct.comp φ.val (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.val) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.val)) = CategoryTheory.CategoryStruct.id S.val) : SheafOfModules R ≌ SheafOfModules S

If e : C ≌ D, then the pushforwards along e.functor and e.inverse forms an equivalence.

theorem SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} (eqv : C ≌ D) {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [eqv.functor.IsContinuous J K] [eqv.functor.IsContinuous J K] [eqv.inverse.IsContinuous K J] [eqv.inverse.IsContinuous K J] (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S) (H₁ : CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.counit) R.val = CategoryTheory.CategoryStruct.comp ψ.val (eqv.inverse.op.whiskerLeft φ.val)) (H₂ : CategoryTheory.CategoryStruct.comp φ.val (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.val) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.val)) = CategoryTheory.CategoryStruct.id S.val) (M : SheafOfModules R) (U : Dᵒᵖ) (x : ↑(((CategoryTheory.Functor.id (SheafOfModules R)).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).unit.app M).val.app U)) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (eqv.counit.app (Opposite.unop U)).op)) x

theorem SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D} (eqv : C ≌ D) {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat} [eqv.functor.IsContinuous J K] [eqv.functor.IsContinuous J K] [eqv.inverse.IsContinuous K J] [eqv.inverse.IsContinuous K J] (φ : S ⟶ (eqv.functor.sheafPushforwardContinuous RingCat J K).obj R) (ψ : R ⟶ (eqv.inverse.sheafPushforwardContinuous RingCat K J).obj S) (H₁ : CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.counit) R.val = CategoryTheory.CategoryStruct.comp ψ.val (eqv.inverse.op.whiskerLeft φ.val)) (H₂ : CategoryTheory.CategoryStruct.comp φ.val (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.val) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.val)) = CategoryTheory.CategoryStruct.id S.val) (M : SheafOfModules S) (U : Cᵒᵖ) (x : ↑((((pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).inverse.comp (pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).functor).obj M).val.obj U)) : (CategoryTheory.ConcreteCategory.hom (((pushforwardPushforwardEquivalence eqv φ ψ H₁ H₂).counit.app M).val.app U)) x = (CategoryTheory.ConcreteCategory.hom (M.val.map (eqv.unit.app (Opposite.unop U)).op)) x