Restriction and sheafification for sheaves of modules

For a continuous and cocontinuous functor between sites, this file identifies pushforward of the sheafification of a presheaf of modules with sheafification after pushforward. Restriction to a slice site is the special case given by Over.forget X.

Pushforward of sheaves of modules is additive, as is its specialization to restriction to a slice site.

The comparison is obtained from the unit of Mathlib's sheafification adjunction. Its underlying morphism of presheaves of abelian groups is the sheafification map whiskered by the functor between sites. Cocontinuity preserves its local injectivity and surjectivity, so Mathlib's localization theorem makes the comparison an isomorphism after sheafification. No formalization is vendored for that comparison: the ingredients are Mathlib's PresheafOfModules.sheafificationAdjunction, PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms, and Presheaf.isLocallyInjective_whisker/Presheaf.isLocallySurjective_whisker.

The iterated-slice comparison Sheaf.iteratedSliceEquivalence identifies two successive restrictions with restriction to the underlying object; its unit-sheaf and restricted-object isomorphisms make that identification usable for transporting local bases. The construction is adapted from Brian Nugent's implementation.

Main declarations

• SheafOfModules.pushforwardSheafificationIso is the sheafification-pushforward comparison for a continuous and cocontinuous functor;
• SheafOfModules.pushforwardSheafificationIso_inv_comp_map_counit and SheafOfModules.sheafification_map_pushforward_map_comp_counit describe the comparison through the counits of the sheafification adjunctions;
• SheafOfModules.overSheafificationIso is its specialization to a slice site;
• Sheaf.iteratedSliceEquivalence identifies restriction to an iterated slice with restriction to the underlying object, with Sheaf.iteratedSliceEquivalenceUnitSheafIso and Sheaf.iteratedSliceEquivalenceInverseObjIso as the two comparisons it provides on unit sheaves and on restrictions of a sheaf of modules;
• SheafOfModules.pushforward and SheafOfModules.overFunctor are additive.

This advances TauCetiRoadmap/JacobianChallenge/README.md, Layer A, item "Invertible sheaves on a scheme; the Picard group Pic X under ⊗", by providing the restriction compatibility needed to compare local trivializations on refinements.

noncomputable def Sheaf.iteratedSliceEquivalence {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) : SheafOfModules (R.over Y.left) ≌ SheafOfModules ((R.over Z).over Y)

Restriction along Over.iteratedSliceEquiv Y, as an equivalence between sheaves of modules on the slice over Y.left and sheaves of modules on the iterated slice over Y.

Equations

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

@[simp]

theorem Sheaf.iteratedSliceEquivalence_functor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) : (iteratedSliceEquivalence R Y).functor = SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((Y.iteratedSliceEquiv.functor.sheafPushforwardContinuous RingCat ((J.over Z).over Y) (J.over Y.left)).obj (R.over Y.left)))

The forward direction of iteratedSliceEquivalence is restriction along (Over.iteratedSliceEquiv Y).functor.

@[simp]

theorem Sheaf.iteratedSliceEquivalence_inverse {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) : (iteratedSliceEquivalence R Y).inverse = SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((Y.iteratedSliceEquiv.inverse.sheafPushforwardContinuous RingCat (J.over Y.left) ((J.over Z).over Y)).obj ((R.over Z).over Y)))

The backward direction of iteratedSliceEquivalence is restriction along (Over.iteratedSliceEquiv Y).inverse.

noncomputable def Sheaf.iteratedSliceEquivalenceUnitSheafIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) : SheafOfModules.unit (R.over Y.left) ≅ (iteratedSliceEquivalence R Y).inverse.obj (SheafOfModules.unit ((R.over Z).over Y))

The comparison of unit sheaves (each structure sheaf as a module over itself) used when transporting generating sections off an iterated slice: the unit sheaf on the slice over Y.left and the restriction along (Sheaf.iteratedSliceEquivalence R Y).inverse of the unit sheaf on the iterated slice over Y are definitionally equal.

Equations

• Sheaf.iteratedSliceEquivalenceUnitSheafIso R Y = CategoryTheory.eqToIso ⋯

@[simp]

theorem Sheaf.iteratedSliceEquivalenceUnitSheafIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) : (iteratedSliceEquivalenceUnitSheafIso R Y).hom = CategoryTheory.eqToHom ⋯

The unit-sheaf comparison is the identity.

@[simp]

theorem Sheaf.iteratedSliceEquivalenceUnitSheafIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) : (iteratedSliceEquivalenceUnitSheafIso R Y).inv = CategoryTheory.eqToHom ⋯

The inverse of the unit-sheaf comparison is the reverse equality morphism.

noncomputable def Sheaf.iteratedSliceEquivalenceInverseObjIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) (M : SheafOfModules R) : (iteratedSliceEquivalence R Y).inverse.obj ((M.over Z).over Y) ≅ M.over Y.left

The inverse of the unit isomorphism of Sheaf.iteratedSliceEquivalence at M.over Y.left, composed with the equality isomorphism that identifies (Sheaf.iteratedSliceEquivalence R Y).functor.obj (M.over Y.left) with (M.over Z).over Y.

Equations

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

theorem Sheaf.iteratedSliceEquivalenceInverseObjIso_def {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) {Z : C} (Y : CategoryTheory.Over Z) (M : SheafOfModules R) : iteratedSliceEquivalenceInverseObjIso R Y M = (iteratedSliceEquivalence R Y).inverse.mapIso (CategoryTheory.eqToIso ⋯) ≪≫ (iteratedSliceEquivalence R Y).unitIso.symm.app (M.over Y.left)

Sheaf.iteratedSliceEquivalenceInverseObjIso is the inverse unit isomorphism composed with the equality isomorphism supplied by Sheaf.iteratedSliceEquivalence_functor.

instance TauCeti.SheafOfModules.instAdditiveSheafOfModulesPushforward_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {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) : (SheafOfModules.pushforward φ).Additive

The pushforward of sheaves of modules is additive.

instance TauCeti.SheafOfModules.instAdditiveSheafOfModulesOverOverRingCatOverFunctor_tauCeti {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} (R : CategoryTheory.Sheaf J RingCat) (X : C) : (SheafOfModules.overFunctor R X).Additive

Restriction to a slice site is additive.

@[reducible, inline]

abbrev TauCeti.SheafOfModules.pushforwardRingIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) : F.op.comp R.obj ≅ ((F.sheafPushforwardContinuous RingCat J K).obj R).obj

The underlying presheaf of the continuous pushforward is precomposition by the functor between sites.

Equations

• TauCeti.SheafOfModules.pushforwardRingIso F R = CategoryTheory.Iso.refl (F.op.comp R.obj)

noncomputable def TauCeti.SheafOfModules.pushforwardToSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] (P : PresheafOfModules R.obj) : (PresheafOfModules.pushforward (pushforwardRingIso F R).inv).obj P ⟶ ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj P)).val

The pushforward of a sheafification unit, as a map of presheaves of modules. This is the canonical comparison whose sheafification is inverted by pushforwardSheafificationIso.

Equations

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

theorem TauCeti.SheafOfModules.pushforwardToSheafify_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] {P Q : PresheafOfModules R.obj} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.pushforward (pushforwardRingIso F R).inv).map f) (pushforwardToSheafify F R Q) = CategoryTheory.CategoryStruct.comp (pushforwardToSheafify F R P) ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).map ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f)).val

The comparison from pushforward to the underlying presheaf of the pushed-forward sheafification is natural in the presheaf.

theorem TauCeti.SheafOfModules.pushforwardToSheafify_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] {P Q : PresheafOfModules R.obj} (f : P ⟶ Q) {Z : PresheafOfModules ((F.sheafPushforwardContinuous RingCat J K).obj R).obj} (h : ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj Q)).val ⟶ Z) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.pushforward (pushforwardRingIso F R).inv).map f) (CategoryTheory.CategoryStruct.comp (pushforwardToSheafify F R Q) h) = CategoryTheory.CategoryStruct.comp (pushforwardToSheafify F R P) (CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).map ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f)).val h)

The comparison from pushforward to the underlying presheaf of the pushed-forward sheafification is natural in the presheaf.

theorem TauCeti.SheafOfModules.toPresheaf_map_pushforwardToSheafify {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] (P : PresheafOfModules R.obj) : (PresheafOfModules.toPresheaf ((F.sheafPushforwardContinuous RingCat J K).obj R).obj).map (pushforwardToSheafify F R P) = F.op.whiskerLeft (CategoryTheory.toSheafify K P.presheaf)

On underlying presheaves of abelian groups, pushforwardToSheafify is the canonical sheafification map whiskered by the functor between sites.

noncomputable def TauCeti.SheafOfModules.pushforwardSheafificationIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [F.IsCocontinuous J K] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (P : PresheafOfModules R.obj) : (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj P) ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).obj ((PresheafOfModules.pushforward (pushforwardRingIso F R).inv).obj P)

For each presheaf of modules, pushforward along a continuous and cocontinuous functor of its sheafification is isomorphic to sheafification after pushforward.

Equations

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

@[simp]

theorem TauCeti.SheafOfModules.pushforwardSheafificationIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [F.IsCocontinuous J K] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (P : PresheafOfModules R.obj) : (pushforwardSheafificationIso F R P).inv = CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).map (pushforwardToSheafify F R P)) (sheafificationIso ((F.sheafPushforwardContinuous RingCat J K).obj R) ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj P))).hom

The inverse of pushforwardSheafificationIso is the canonical comparison obtained from the sheafification unit and counit.

theorem TauCeti.SheafOfModules.pushforwardSheafificationIso_inv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [F.IsCocontinuous J K] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P Q : PresheafOfModules R.obj} (f : P ⟶ Q) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).map ((PresheafOfModules.pushforward (pushforwardRingIso F R).inv).map f)) (pushforwardSheafificationIso F R Q).inv = CategoryTheory.CategoryStruct.comp (pushforwardSheafificationIso F R P).inv ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).map ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f))

The inverse sheafification--pushforward comparison is natural in the presheaf.

theorem TauCeti.SheafOfModules.pushforwardSheafificationIso_inv_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [F.IsCocontinuous J K] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P Q : PresheafOfModules R.obj} (f : P ⟶ Q) {Z : SheafOfModules ((F.sheafPushforwardContinuous RingCat J K).obj R)} (h : (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj Q) ⟶ Z) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).map ((PresheafOfModules.pushforward (pushforwardRingIso F R).inv).map f)) (CategoryTheory.CategoryStruct.comp (pushforwardSheafificationIso F R Q).inv h) = CategoryTheory.CategoryStruct.comp (pushforwardSheafificationIso F R P).inv (CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).map ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f)) h)

The inverse sheafification--pushforward comparison is natural in the presheaf.

theorem TauCeti.SheafOfModules.pushforwardSheafificationIso_inv_comp_map_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [F.IsCocontinuous J K] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (M : SheafOfModules R) : CategoryTheory.CategoryStruct.comp (pushforwardSheafificationIso F R (((SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars (CategoryTheory.CategoryStruct.id R.obj))).obj M)).inv ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).map ((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id R.obj)).counit.app M)) = (PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).counit.app ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj M)

On the underlying presheaf of a sheaf of modules M, the inverse sheafification--pushforward comparison followed by the pushforward of the counit of the sheafification adjunction at M is the counit at the pushforward of M.

theorem TauCeti.SheafOfModules.pushforwardSheafificationIso_inv_comp_map_counit_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [F.IsCocontinuous J K] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (M : SheafOfModules R) {Z : SheafOfModules ((F.sheafPushforwardContinuous RingCat J K).obj R)} (h : (SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (pushforwardSheafificationIso F R ((PresheafOfModules.restrictScalars (CategoryTheory.CategoryStruct.id R.obj)).obj ((SheafOfModules.forget R).obj M))).inv (CategoryTheory.CategoryStruct.comp ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).map ((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id R.obj)).counit.app M)) h) = CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).counit.app ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj M)) h

On the underlying presheaf of a sheaf of modules M, the inverse sheafification--pushforward comparison followed by the pushforward of the counit of the sheafification adjunction at M is the counit at the pushforward of M.

theorem TauCeti.SheafOfModules.sheafification_map_pushforward_map_comp_counit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D} (F : CategoryTheory.Functor C D) [F.IsContinuous J K] (R : CategoryTheory.Sheaf K RingCat) [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [F.IsCocontinuous J K] [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] {P : PresheafOfModules R.obj} {M : SheafOfModules R} (f : P ⟶ ((SheafOfModules.forget R).comp (PresheafOfModules.restrictScalars (CategoryTheory.CategoryStruct.id R.obj))).obj M) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).map ((PresheafOfModules.pushforward (pushforwardRingIso F R).inv).map f)) ((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R).obj)).counit.app ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).obj M)) = CategoryTheory.CategoryStruct.comp (pushforwardSheafificationIso F R P).inv ((SheafOfModules.pushforward (CategoryTheory.CategoryStruct.id ((F.sheafPushforwardContinuous RingCat J K).obj R))).map (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id R.obj)).homEquiv P M).symm f))

The sheafification of the pushforward of a morphism f : P ⟶ M from a presheaf of modules into (the underlying presheaf of) a sheaf of modules, followed by the counit for the pushforward of M, is the inverse sheafification--pushforward comparison followed by the pushforward of the adjoint morphism P^# ⟶ M.

noncomputable def TauCeti.SheafOfModules.overSheafificationIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) (P : PresheafOfModules R.obj) (X : C) [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] : ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj P).over X ≅ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (R.over X).obj)).obj ((PresheafOfModules.pushforward (pushforwardRingIso (CategoryTheory.Over.forget X) R).inv).obj P)

For each presheaf of modules and object of the site, restriction of its sheafification is isomorphic to the sheafification of its restriction.

Equations

• TauCeti.SheafOfModules.overSheafificationIso R P X = TauCeti.SheafOfModules.pushforwardSheafificationIso (CategoryTheory.Over.forget X) R P

@[simp]

theorem TauCeti.SheafOfModules.overSheafificationIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) (P : PresheafOfModules R.obj) (X : C) [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] : (overSheafificationIso R P X).inv = CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (R.over X).obj)).map (pushforwardToSheafify (CategoryTheory.Over.forget X) R P)) (sheafificationIso (R.over X) (((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj P).over X)).hom

The inverse of overSheafificationIso is the canonical comparison obtained from the sheafification unit and counit, as in pushforwardSheafificationIso_inv.

theorem TauCeti.SheafOfModules.overSheafificationIso_inv_naturality {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) {P Q : PresheafOfModules R.obj} (f : P ⟶ Q) (X : C) [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (R.over X).obj)).map ((PresheafOfModules.pushforward (pushforwardRingIso (CategoryTheory.Over.forget X) R).inv).map f)) (overSheafificationIso R Q X).inv = CategoryTheory.CategoryStruct.comp (overSheafificationIso R P X).inv ((SheafOfModules.overFunctor R X).map ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f))

The inverse restriction--sheafification comparison is natural in the presheaf.

theorem TauCeti.SheafOfModules.overSheafificationIso_inv_naturality_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) {P Q : PresheafOfModules R.obj} (f : P ⟶ Q) (X : C) [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] {Z : SheafOfModules (R.over X)} (h : ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).obj Q).over X ⟶ Z) : CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (R.over X).obj)).map ((PresheafOfModules.pushforward (pushforwardRingIso (CategoryTheory.Over.forget X) R).inv).map f)) (CategoryTheory.CategoryStruct.comp (overSheafificationIso R Q X).inv h) = CategoryTheory.CategoryStruct.comp (overSheafificationIso R P X).inv (CategoryTheory.CategoryStruct.comp ((SheafOfModules.overFunctor R X).map ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map f)) h)

The inverse restriction--sheafification comparison is natural in the presheaf.

noncomputable def TauCeti.SheafOfModules.overSheafificationNatIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) (X : C) [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] : (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).comp (SheafOfModules.overFunctor R X) ≅ (PresheafOfModules.pushforward (pushforwardRingIso (CategoryTheory.Over.forget X) R).inv).comp (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (R.over X).obj))

Restriction after sheafification is naturally isomorphic to sheafification after restriction of presheaves.

Equations

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

@[simp]

theorem TauCeti.SheafOfModules.overSheafificationNatIso_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) (X : C) [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] (P : PresheafOfModules R.obj) : (overSheafificationNatIso R X).hom.app P = (pushforwardSheafificationIso (CategoryTheory.Over.forget X) R P).hom

The forward component of overSheafificationNatIso is the generic pushforward--sheafification comparison.

@[simp]

theorem TauCeti.SheafOfModules.overSheafificationNatIso_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (R : CategoryTheory.Sheaf J RingCat) (X : C) [CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] [(J.over X).WEqualsLocallyBijective AddCommGrpCat] (P : PresheafOfModules R.obj) : (overSheafificationNatIso R X).inv.app P = (pushforwardSheafificationIso (CategoryTheory.Over.forget X) R P).inv

The inverse component of overSheafificationNatIso is the inverse generic pushforward--sheafification comparison.