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] (φ : 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_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] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {X✝ Y✝ : SheafOfModules R} (f : X✝ ⟶ Y✝) : ((pushforward φ).map f).val = (PresheafOfModules.pushforward φ.hom).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] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (M : SheafOfModules R) : ((pushforward φ).obj M).val = (PresheafOfModules.pushforward φ.hom).obj M.val

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

The restriction functor from sheaves of R-modules to sheaves of R.over X-modules for some X : D.

Equations

• SheafOfModules.overFunctor R X = SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (R.over X))

@[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.overFunctor R X).obj M

@[reducible, inline]

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

Given a map f : M ⟶ N between sheaves of modules over R, this is the restriction to the map M.over X ⟶ N.over X between sheaves of modules over R.over X.

Equations

• SheafOfModules.Hom.over f X = (SheafOfModules.overFunctor R X).map f

noncomputable def SheafOfModules.overMap {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (R : CategoryTheory.Sheaf K RingCat) {X Y : D} (f : X ⟶ Y) : CategoryTheory.Functor (SheafOfModules (R.over Y)) (SheafOfModules (R.over X))

If f : X ⟶ Y, this is the pushforward of sheaves of modules along Over.map f.

Equations

• SheafOfModules.overMap R f = SheafOfModules.pushforward (R.pushforwardOverMapIso f).inv

noncomputable def SheafOfModules.overFunctorMap {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (R : CategoryTheory.Sheaf K RingCat) {X Y : D} (f : X ⟶ Y) : (overFunctor R Y).comp (overMap R f) ≅ overFunctor R X

First restricting to Over Y and then extending to Over X is the same as restricting to Over X.

Equations

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

noncomputable def SheafOfModules.overMapUnitIso {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {R : CategoryTheory.Sheaf K RingCat} {X Y : D} [(K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [(K.over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (f : X ⟶ Y) : (overMap R f).obj (unit (R.over Y)) ≅ unit (R.over X)

The pushforward of R.over Y along Over.map f is isomorphic to R.over X.

Equations

• SheafOfModules.overMapUnitIso f = CategoryTheory.Iso.refl ((SheafOfModules.overMap R f).obj (SheafOfModules.unit (R.over Y)))

@[simp]

theorem SheafOfModules.overMapUnitIso_hom_val_app_hom_apply {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {R : CategoryTheory.Sheaf K RingCat} {X Y : D} [(K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [(K.over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (f : X ⟶ Y) (x✝ : (CategoryTheory.Over X)ᵒᵖ) (x : ↑(((overMap R f).obj (unit (R.over Y))).val.obj x✝)) : (ModuleCat.Hom.hom ((overMapUnitIso f).hom.val.app x✝)) x = x

@[simp]

theorem SheafOfModules.overMapUnitIso_inv_val_app_hom_apply {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} {R : CategoryTheory.Sheaf K RingCat} {X Y : D} [(K.over X).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] [(K.over Y).HasSheafCompose (CategoryTheory.forget₂ RingCat AddCommGrpCat)] (f : X ⟶ Y) (x✝ : (CategoryTheory.Over X)ᵒᵖ) (x : ↑(((overMap R f).obj (unit (R.over Y))).val.obj x✝)) : (ModuleCat.Hom.hom ((overMapUnitIso f).inv.val.app x✝)) x = x

noncomputable def SheafOfModules.overPullback {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.Limits.HasPullbacks D] {X Y : D} (f : X ⟶ Y) : CategoryTheory.Functor (SheafOfModules (R.over X)) (SheafOfModules (R.over Y))

If f : X ⟶ Y, this is the pushforward of sheaves of modules along Over.pullback f.

Equations

• SheafOfModules.overPullback R f = SheafOfModules.pushforward (R.toPushforwardOverPullback f)

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.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] {φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R} (e : φ = ψ) : pushforward φ ≅ pushforward ψ

Pushforwards along equal morphisms of sheaves of rings are isomorphic.

Equations

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

@[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] {φ ψ : 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] {φ ψ : 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] {φ ψ : 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] (φ : 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'] [(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.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] (φ : 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'] [(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] (φ : 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'] [(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] (φ : 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'] [(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.comp G').IsContinuous K 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] (φ : 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] (φ : 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] [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.

Equations

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

@[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] [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] (φ : 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] [G.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] [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] [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.

Equations

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

@[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] [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] [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] [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.obj = CategoryTheory.CategoryStruct.comp ψ.hom (G.op.whiskerLeft φ.hom)) (H₂ : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.hom) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.obj)) = CategoryTheory.CategoryStruct.id S.obj) : pushforward φ ⊣ pushforward ψ

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

Equations

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

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] [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.obj = CategoryTheory.CategoryStruct.comp ψ.hom (G.op.whiskerLeft φ.hom)) (H₂ : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.hom) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.obj)) = CategoryTheory.CategoryStruct.id S.obj) (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] [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.obj = CategoryTheory.CategoryStruct.comp ψ.hom (G.op.whiskerLeft φ.hom)) (H₂ : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (F.op.whiskerLeft ψ.hom) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op adj.unit) S.obj)) = CategoryTheory.CategoryStruct.id S.obj) (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

noncomputable 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.

Equations

• SheafOfModules.pushforwardOver x = { hom := { app := fun (U : Cᵒᵖ) => R.obj.map CategoryTheory.Limits.prod.snd.op, naturality := ⋯ } }

noncomputable 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.

Equations

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

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.overMapPushforwardAdj {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : overMap R f ⊣ overPullback R f

The adjunction between pushforward along Over.map and pushforward along Over.pullback.

Equations

• SheafOfModules.overMapPushforwardAdj R f = SheafOfModules.pushforwardPushforwardAdj (CategoryTheory.Over.mapPullbackAdj f) (R.pushforwardOverMapIso f).inv (R.toPushforwardOverPullback f) ⋯ ⋯

instance SheafOfModules.instIsLeftAdjointOverOverRingCatOverMapOfHasPullbacks {C : Type u'} [CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.Limits.HasPullbacks C] {X Y : C} (f : X ⟶ Y) : (overMap R f).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.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.obj = CategoryTheory.CategoryStruct.comp ψ.hom (eqv.inverse.op.whiskerLeft φ.hom)) (H₂ : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.hom) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.obj)) = CategoryTheory.CategoryStruct.id S.obj) : SheafOfModules R ≌ SheafOfModules S

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

Equations

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

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.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.obj = CategoryTheory.CategoryStruct.comp ψ.hom (eqv.inverse.op.whiskerLeft φ.hom)) (H₂ : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.hom) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.obj)) = CategoryTheory.CategoryStruct.id S.obj) (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.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.obj = CategoryTheory.CategoryStruct.comp ψ.hom (eqv.inverse.op.whiskerLeft φ.hom)) (H₂ : CategoryTheory.CategoryStruct.comp φ.hom (CategoryTheory.CategoryStruct.comp (eqv.functor.op.whiskerLeft ψ.hom) (CategoryTheory.Functor.whiskerRight (CategoryTheory.NatTrans.op eqv.unit) S.obj)) = CategoryTheory.CategoryStruct.id S.obj) (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

noncomputable def SheafOfModules.pushforwardCompForgetToSheafModuleCat {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] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) (X : Cᵒᵖ) (hX : CategoryTheory.Limits.IsInitial X) (hX' : CategoryTheory.Limits.IsInitial (F.op.obj X)) : (pushforward φ).comp (forgetToSheafModuleCat S X hX) ≅ (forgetToSheafModuleCat R (F.op.obj X) hX').comp ((CategoryTheory.sheafCompose K (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.hom.app X)))).comp (F.sheafPushforwardContinuous (ModuleCat ↑(S.obj.obj X)) J K))

Pushforward commutes with SheafOfModules.forgetToSheafModuleCat

Equations

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