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)
:
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.
Instances For
@[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
@[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.
Instances For
noncomputable def
SheafOfModules.pushforwardId
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
(R : CategoryTheory.Sheaf K RingCat)
:
The pushforward functor by the identity morphism identifies to the identify functor of the category of sheaves of modules.
Instances For
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 : φ = ψ)
:
Pushforwards along equal morphisms of sheaves of rings are isomorphic.
Instances For
@[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.
Instances For
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)
:
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)
:
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)
:
A natural transformation gives a natural transformation between the pushforward functors.
Instances For
@[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)
:
@[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)
:
A natural isomorphism gives a natural isomorphism between the pushforward functors.
Instances For
@[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)
:
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)
:
If F ⊣ G, then the pushforwards along F and G are also adjoint.
Instances For
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)
:
The canonical morphism from R to the pushforward of its restriction to Over x.
Instances For
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)
:
The adjunction between restriction to Over x and pushforward along Over.star x.
Instances For
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)
:
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)
:
If e : C ≌ D, then the pushforwards along e.functor and e.inverse forms an equivalence.
Instances For
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