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.
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)
:
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.
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]
[F.IsContinuous J K]
(φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R)
{X✝ Y✝ : SheafOfModules R}
(f : X✝ ⟶ Y✝)
:
((SheafOfModules.pushforward φ).map f).val = (PresheafOfModules.pushforward φ.val).map f.val
@[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)
:
((SheafOfModules.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.
Equations
- M.over X = (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat (K.over X) K).obj R))).obj M