Local isomorphisms of presheaves of modules are stable under tensor products

Let R be a presheaf of commutative rings on a small site (C, J). A morphism f of presheaves of R-modules is a local isomorphism when its underlying morphism of presheaves of abelian groups lies in J.W, i.e. becomes an isomorphism after sheafification. This file proves that the sectionwise tensor product of presheaves of modules preserves local isomorphisms in each variable: the morphism property J.W.inverseImage (PresheafOfModules.toPresheaf _) is monoidal.

This is the input needed to compare iterated sheafified tensor products of sheaves of modules: sheafifying M ⊗ N before tensoring with P does not change the sheafification of the result.

Main declarations

• PresheafOfModules.isLocallySurjective_whiskerLeft: tensoring with any presheaf of modules preserves local surjectivity;
• PresheafOfModules.isLocallyInjective_free_whiskerLeft: tensoring with a free presheaf of modules preserves local injectivity;
• PresheafOfModules.inverseImage_W_toPresheaf_whiskerLeft and PresheafOfModules.inverseImage_W_toPresheaf_whiskerRight: tensoring with any presheaf of modules preserves local isomorphisms;
• PresheafOfModules.isMonoidal_inverseImage_W_toPresheaf: the resulting IsMonoidal instance.

theorem PresheafOfModules.isLocallySurjective_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (P : PresheafOfModulesOfCommRing R) {N N' : PresheafOfModulesOfCommRing R} (f : N ⟶ N') [CategoryTheory.Presheaf.IsLocallySurjective J ((toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map f)] : CategoryTheory.Presheaf.IsLocallySurjective J ((toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P f))

Tensoring with a presheaf of modules P preserves local surjectivity: a section of P ⊗ N' is locally a sum of elementary tensors whose second factors lift along f.

theorem PresheafOfModules.isLocallyInjective_free_whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} (F : CategoryTheory.Functor Cᵒᵖ (Type u)) {N N' : PresheafOfModulesOfCommRing R} (f : N ⟶ N') [CategoryTheory.Presheaf.IsLocallyInjective J ((toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map f)] : CategoryTheory.Presheaf.IsLocallyInjective J ((toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((free (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))).obj F) f))

Tensoring with the free presheaf of modules on a presheaf of types F preserves local injectivity. A section of free F ⊗ N killed by free F ◁ f has all its coefficients killed by f, and these finitely many coefficients vanish together on a covering sieve.

theorem PresheafOfModules.inverseImage_W_toPresheaf_whiskerLeft {C : Type u} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] (P : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) {N N' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {f : N ⟶ N'} (hf : J.W.inverseImage (toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) f) : J.W.inverseImage (toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P f)

Tensoring with a presheaf of modules on the left preserves local isomorphisms.

theorem PresheafOfModules.inverseImage_W_toPresheaf_whiskerRight {C : Type u} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {N N' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} {f : N ⟶ N'} (hf : J.W.inverseImage (toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) f) (P : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) : J.W.inverseImage (toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (CategoryTheory.MonoidalCategoryStruct.whiskerRight f P)

Tensoring with a presheaf of modules on the right preserves local isomorphisms.

instance PresheafOfModules.isMonoidal_inverseImage_W_toPresheaf {C : Type u} [CategoryTheory.SmallCategory C] (J : CategoryTheory.GrothendieckTopology C) {R : CategoryTheory.Functor Cᵒᵖ CommRingCat} [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] : (J.W.inverseImage (toPresheaf (R.comp (CategoryTheory.forget₂ CommRingCat RingCat)))).IsMonoidal

Local isomorphisms of presheaves of modules form a monoidal morphism property.