Sheafifying a sectionwise pushforward comparison #
Let F : C ⥤ D be a continuous functor between sites, S and R sheaves of commutative
rings on C and D, and φ : S ⟶ F_* R a morphism of the underlying sheaves of rings. Many
endofunctors T of sheaves of modules, such as exterior and symmetric powers, are the
sheafification of a sectionwise endofunctor P of presheaves of modules. Given such
presentations T_S of P_S over S and T_R of P_R over R, a sectionwise comparison
c : φ_* ⋙ P_S ⟶ P_R ⋙ φ_* induces a natural comparison T_S ∘ φ_* ⟶ φ_* ∘ T_R: the transpose
along sheafification of c followed by the pushforward of the sheafification unit of P_R M.
The presentations are passed as identifications T.obj M ≅ (P M)^# together with the induced
formula for T.map, which is how SheafOfModules.exteriorPower and
SheafOfModules.symmetricPower are presented (SheafOfModules.exteriorPowerIso,
SheafOfModules.exteriorPower_map, and their symmetric-power counterparts).
Main declarations #
TauCeti.SheafOfModules.sheafifyPushforwardComparison: the comparisonT_S ∘ φ_* ⟶ φ_* ∘ T_R, determined on underlying presheaves byunit_comp_forget_map_sheafifyPushforwardComparison_app;TauCeti.SheafOfModules.sheafifyPushforwardComparison_app_comp_pushforward_map: the comparison is compatible with sheafified maps out ofT_SandT_Rwhose sectionwise maps are compatible withc, as for the identifications of first exterior and symmetric powers with the module;TauCeti.SheafOfModules.isIso_sheafifyPushforwardComparison: the comparison is invertible when the sectionwise comparison is invertible and the functor of sites is cocontinuous.
noncomputable def
TauCeti.SheafOfModules.sheafifyPushforwardComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
{TS : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf S))}
{PS : CategoryTheory.Functor (PresheafOfModulesOfCommRing S.obj) (PresheafOfModulesOfCommRing S.obj)}
(eS :
(M : SheafOfModules (ringCatSheaf S)) →
TS.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).obj (PS.obj M.val))
(hS :
∀ {M N : SheafOfModules (ringCatSheaf S)} (f : M ⟶ N),
TS.map f = CategoryTheory.CategoryStruct.comp (eS M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).map
(PS.map f.val))
(eS N).inv))
{TR : CategoryTheory.Functor (SheafOfModules (ringCatSheaf R)) (SheafOfModules (ringCatSheaf R))}
{PR : CategoryTheory.Functor (PresheafOfModulesOfCommRing R.obj) (PresheafOfModulesOfCommRing R.obj)}
(eR :
(M : SheafOfModules (ringCatSheaf R)) →
TR.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (PR.obj M.val))
(hR :
∀ {M N : SheafOfModules (ringCatSheaf R)} (f : M ⟶ N),
TR.map f = CategoryTheory.CategoryStruct.comp (eR M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map
(PR.map f.val))
(eR N).inv))
(c :
(PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)).comp PS ⟶ PR.comp (PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)))
:
The natural comparison T_S (φ_* M) ⟶ φ_* (T_R M) induced by a sectionwise comparison
c : φ_* ⋙ P_S ⟶ P_R ⋙ φ_*, for sheafified presentations eS of T_S and eR of T_R: the
transpose along sheafification of c followed by the pushforward of the sheafification unit.
Instances For
theorem
TauCeti.SheafOfModules.unit_comp_forget_map_sheafifyPushforwardComparison_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
{TS : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf S))}
{PS : CategoryTheory.Functor (PresheafOfModulesOfCommRing S.obj) (PresheafOfModulesOfCommRing S.obj)}
(eS :
(M : SheafOfModules (ringCatSheaf S)) →
TS.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).obj (PS.obj M.val))
(hS :
∀ {M N : SheafOfModules (ringCatSheaf S)} (f : M ⟶ N),
TS.map f = CategoryTheory.CategoryStruct.comp (eS M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).map
(PS.map f.val))
(eS N).inv))
{TR : CategoryTheory.Functor (SheafOfModules (ringCatSheaf R)) (SheafOfModules (ringCatSheaf R))}
{PR : CategoryTheory.Functor (PresheafOfModulesOfCommRing R.obj) (PresheafOfModulesOfCommRing R.obj)}
(eR :
(M : SheafOfModules (ringCatSheaf R)) →
TR.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (PR.obj M.val))
(hR :
∀ {M N : SheafOfModules (ringCatSheaf R)} (f : M ⟶ N),
TR.map f = CategoryTheory.CategoryStruct.comp (eR M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map
(PR.map f.val))
(eR N).inv))
(c :
(PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)).comp PS ⟶ PR.comp (PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)))
(M : SheafOfModules (ringCatSheaf R))
:
CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
(PS.obj ((SheafOfModules.pushforward φ).obj M).val))
((SheafOfModules.forget (ringCatSheaf S)).map
(CategoryTheory.CategoryStruct.comp (eS ((SheafOfModules.pushforward φ).obj M)).inv
((sheafifyPushforwardComparison φ eS ⋯ eR ⋯ c).app M))) = CategoryTheory.CategoryStruct.comp (c.app M.val)
((presheafPushforward φ).map
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
(PR.obj M.val))
((SheafOfModules.forget (ringCatSheaf R)).map (eR M).inv)))
On underlying presheaves, the sheafified comparison restricted along the sheafification unit
is the sectionwise comparison followed by the pushforward of the sheafification unit of P_R M.
This determines the comparison, by the universal property of sheafification.
theorem
TauCeti.SheafOfModules.unit_comp_forget_map_sheafifyPushforwardComparison_app_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
{TS : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf S))}
{PS : CategoryTheory.Functor (PresheafOfModulesOfCommRing S.obj) (PresheafOfModulesOfCommRing S.obj)}
(eS :
(M : SheafOfModules (ringCatSheaf S)) →
TS.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).obj (PS.obj M.val))
(hS :
∀ {M N : SheafOfModules (ringCatSheaf S)} (f : M ⟶ N),
TS.map f = CategoryTheory.CategoryStruct.comp (eS M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).map
(PS.map f.val))
(eS N).inv))
{TR : CategoryTheory.Functor (SheafOfModules (ringCatSheaf R)) (SheafOfModules (ringCatSheaf R))}
{PR : CategoryTheory.Functor (PresheafOfModulesOfCommRing R.obj) (PresheafOfModulesOfCommRing R.obj)}
(eR :
(M : SheafOfModules (ringCatSheaf R)) →
TR.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (PR.obj M.val))
(hR :
∀ {M N : SheafOfModules (ringCatSheaf R)} (f : M ⟶ N),
TR.map f = CategoryTheory.CategoryStruct.comp (eR M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map
(PR.map f.val))
(eR N).inv))
(c :
(PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)).comp PS ⟶ PR.comp (PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)))
(M : SheafOfModules (ringCatSheaf R))
{Z : PresheafOfModules (ringCatSheaf S).obj}
(h : (SheafOfModules.forget (ringCatSheaf S)).obj ((SheafOfModules.pushforward φ).obj (TR.obj M)) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).unit.app
(PS.obj ((SheafOfModules.pushforward φ).obj M).val))
((SheafOfModules.forget (ringCatSheaf S)).map
(CategoryTheory.CategoryStruct.comp (eS ((SheafOfModules.pushforward φ).obj M)).inv
((sheafifyPushforwardComparison φ eS ⋯ eR ⋯ c).app M))))
h = CategoryTheory.CategoryStruct.comp
(CategoryTheory.CategoryStruct.comp (c.app M.val)
((presheafPushforward φ).map
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app
(PR.obj M.val))
((SheafOfModules.forget (ringCatSheaf R)).map (eR M).inv))))
h
On underlying presheaves, the sheafified comparison restricted along the sheafification unit
is the sectionwise comparison followed by the pushforward of the sheafification unit of P_R M.
This determines the comparison, by the universal property of sheafification.
theorem
TauCeti.SheafOfModules.sheafifyPushforwardComparison_app_comp_pushforward_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
{TS : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf S))}
{PS : CategoryTheory.Functor (PresheafOfModulesOfCommRing S.obj) (PresheafOfModulesOfCommRing S.obj)}
(eS :
(M : SheafOfModules (ringCatSheaf S)) →
TS.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).obj (PS.obj M.val))
(hS :
∀ {M N : SheafOfModules (ringCatSheaf S)} (f : M ⟶ N),
TS.map f = CategoryTheory.CategoryStruct.comp (eS M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).map
(PS.map f.val))
(eS N).inv))
{TR : CategoryTheory.Functor (SheafOfModules (ringCatSheaf R)) (SheafOfModules (ringCatSheaf R))}
{PR : CategoryTheory.Functor (PresheafOfModulesOfCommRing R.obj) (PresheafOfModulesOfCommRing R.obj)}
(eR :
(M : SheafOfModules (ringCatSheaf R)) →
TR.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (PR.obj M.val))
(hR :
∀ {M N : SheafOfModules (ringCatSheaf R)} (f : M ⟶ N),
TR.map f = CategoryTheory.CategoryStruct.comp (eR M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map
(PR.map f.val))
(eR N).inv))
(c :
(PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)).comp PS ⟶ PR.comp (PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)))
(M : SheafOfModules (ringCatSheaf R))
{fS : TS.obj ((SheafOfModules.pushforward φ).obj M) ⟶ (SheafOfModules.pushforward φ).obj M}
{fR : TR.obj M ⟶ M}
{oS : PS.obj ((SheafOfModules.pushforward φ).obj M).val ⟶ ((SheafOfModules.pushforward φ).obj M).val}
{oR : PR.obj M.val ⟶ M.val}
(hfS :
CategoryTheory.CategoryStruct.comp (eS ((SheafOfModules.pushforward φ).obj M)).inv fS = CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).map oS)
(sheafificationIso (ringCatSheaf S) ((SheafOfModules.pushforward φ).obj M)).hom)
(hfR :
CategoryTheory.CategoryStruct.comp (eR M).inv fR = CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map oR)
(sheafificationIso (ringCatSheaf R) M).hom)
(h :
CategoryTheory.CategoryStruct.comp (c.app M.val)
((PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)).map oR) = oS)
:
CategoryTheory.CategoryStruct.comp ((sheafifyPushforwardComparison φ eS ⋯ eR ⋯ c).app M)
((SheafOfModules.pushforward φ).map fR) = fS
The sheafified comparison is compatible with maps fS : T_S (φ_* M) ⟶ φ_* M and
fR : T_R M ⟶ M that are sheafifications of sectionwise maps oS and oR compatible with the
sectionwise comparison c. For instance, this identifies the comparison in degree one with the
identity, through the identifications of first exterior or symmetric powers with the module.
instance
TauCeti.SheafOfModules.isIso_sheafifyPushforwardComparison
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : CategoryTheory.GrothendieckTopology C}
[J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify J AddCommGrpCat]
[J.WEqualsLocallyBijective AddCommGrpCat]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{K : CategoryTheory.GrothendieckTopology D}
[K.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)]
[CategoryTheory.HasWeakSheafify K AddCommGrpCat]
[K.WEqualsLocallyBijective AddCommGrpCat]
{F : CategoryTheory.Functor C D}
[F.IsContinuous J K]
{S : CategoryTheory.Sheaf J CommRingCat}
{R : CategoryTheory.Sheaf K CommRingCat}
(φ : ringCatSheaf S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj (ringCatSheaf R))
{TS : CategoryTheory.Functor (SheafOfModules (ringCatSheaf S)) (SheafOfModules (ringCatSheaf S))}
{PS : CategoryTheory.Functor (PresheafOfModulesOfCommRing S.obj) (PresheafOfModulesOfCommRing S.obj)}
(eS :
(M : SheafOfModules (ringCatSheaf S)) →
TS.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).obj (PS.obj M.val))
(hS :
∀ {M N : SheafOfModules (ringCatSheaf S)} (f : M ⟶ N),
TS.map f = CategoryTheory.CategoryStruct.comp (eS M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf S).obj)).map
(PS.map f.val))
(eS N).inv))
{TR : CategoryTheory.Functor (SheafOfModules (ringCatSheaf R)) (SheafOfModules (ringCatSheaf R))}
{PR : CategoryTheory.Functor (PresheafOfModulesOfCommRing R.obj) (PresheafOfModulesOfCommRing R.obj)}
(eR :
(M : SheafOfModules (ringCatSheaf R)) →
TR.obj M ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).obj (PR.obj M.val))
(hR :
∀ {M N : SheafOfModules (ringCatSheaf R)} (f : M ⟶ N),
TR.map f = CategoryTheory.CategoryStruct.comp (eR M).hom
(CategoryTheory.CategoryStruct.comp
((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map
(PR.map f.val))
(eR N).inv))
(c :
(PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)).comp PS ⟶ PR.comp (PresheafOfModulesOfCommRing.pushforward (commRingCatHom φ)))
[F.IsCocontinuous J K]
[CategoryTheory.IsIso c]
:
CategoryTheory.IsIso (sheafifyPushforwardComparison φ eS ⋯ eR ⋯ c)
Along a continuous and cocontinuous functor, sheafification carries an invertible sectionwise pushforward comparison to an invertible comparison of sheaves of modules.