Tensor descent for invertible module sheaves on a ringed site

Tensoring a module-presheaf morphism with a locally free rank-one module sheaf preserves the local equivalences inverted by sheafification. The proof works on an arbitrary Grothendieck site: local surjectivity is preserved by tensoring, while local injectivity is checked on a covering family where the rank-one factor is identified with the unit.

The stalkwise strengthening available on topological spaces, which removes the rank-one hypothesis, lives in DerivedAlgGeo.Topology.Sheaves.ModuleTensor.

@[implicit_reducible]

noncomputable def SheafOfModules.instMonoidalCategoryPresheafOfModulesCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrier_derivedAlgGeo {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} : CategoryTheory.MonoidalCategory (PresheafOfModules (S.comp (CategoryTheory.forget₂ CommRingCat RingCat)))

Equations

• SheafOfModules.instMonoidalCategoryPresheafOfModulesCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrier_derivedAlgGeo = PresheafOfModules.monoidalCategory

theorem SheafOfModules.isLocallySurjective_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (F : PresheafOfModules (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))) {G₁ G₂ : PresheafOfModules (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (g : G₁ ⟶ G₂) [CategoryTheory.Presheaf.IsLocallySurjective J ((PresheafOfModules.toPresheaf (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map g)] : CategoryTheory.Presheaf.IsLocallySurjective J ((PresheafOfModules.toPresheaf (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F g))

Tensoring on the left preserves local surjectivity on an arbitrary site.

theorem SheafOfModules.isLocallyInjective_whiskerLeft_of_isoUnit {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} (F : PresheafOfModules (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))) (e : CategoryTheory.MonoidalCategoryStruct.tensorUnit (PresheafOfModules (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))) ≅ F) {G₁ G₂ : PresheafOfModules (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))} (g : G₁ ⟶ G₂) [CategoryTheory.Presheaf.IsLocallyInjective J ((PresheafOfModules.toPresheaf (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map g)] : CategoryTheory.Presheaf.IsLocallyInjective J ((PresheafOfModules.toPresheaf (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F g))

Tensoring on the left by an object isomorphic to the unit preserves local injectivity.

@[implicit_reducible]

noncomputable def SheafOfModules.instMonoidalCategoryPresheafOfModulesObjFunctorOppositeRingCatIsSheafRingSheaf {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} : CategoryTheory.MonoidalCategory (PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj)

Equations

• SheafOfModules.instMonoidalCategoryPresheafOfModulesObjFunctorOppositeRingCatIsSheafRingSheaf = PresheafOfModules.monoidalCategory

@[implicit_reducible]

noncomputable def SheafOfModules.instSymmetricCategoryPresheafOfModulesObjFunctorOppositeRingCatIsSheafRingSheaf {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} : CategoryTheory.SymmetricCategory (PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj)

Equations

• SheafOfModules.instSymmetricCategoryPresheafOfModulesObjFunctorOppositeRingCatIsSheafRingSheaf = PresheafOfModules.symmetricCategory

theorem SheafOfModules.isLocallyInjective_whiskerLeft_of_rankOneData {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} [∀ (X : D), CategoryTheory.HasWeakSheafify (K.over X) AddCommGrpCat] [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules (SheafOfModules.ringSheaf✝ S)} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) {G₁ G₂ : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj} (g : G₁ ⟶ G₂) [CategoryTheory.Presheaf.IsLocallyInjective K ((PresheafOfModules.toPresheaf (SheafOfModules.ringSheaf✝ S).obj).map g)] : CategoryTheory.Presheaf.IsLocallyInjective K ((PresheafOfModules.toPresheaf (SheafOfModules.ringSheaf✝ S).obj).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.val g))

Tensoring by a locally free rank-one module sheaf preserves local injectivity.

theorem SheafOfModules.W_whiskerLeft_of_rankOneData {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} [K.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), CategoryTheory.HasWeakSheafify (K.over X) AddCommGrpCat] [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules (SheafOfModules.ringSheaf✝ S)} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) {G₁ G₂ : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj} (g : G₁ ⟶ G₂) (hg : K.W ((PresheafOfModules.toPresheaf (SheafOfModules.ringSheaf✝ S).obj).map g)) : K.W ((PresheafOfModules.toPresheaf (SheafOfModules.ringSheaf✝ S).obj).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.val g))

Tensoring by a locally free rank-one module sheaf preserves sheafification equivalences.

theorem SheafOfModules.isIso_sheafification_map_whiskerLeft_of_rankOneData {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), CategoryTheory.HasWeakSheafify (K.over X) AddCommGrpCat] [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules (SheafOfModules.ringSheaf✝ S)} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) {G₁ G₂ : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj} (g : G₁ ⟶ G₂) (hg : K.W ((PresheafOfModules.toPresheaf (SheafOfModules.ringSheaf✝ S).obj).map g)) : CategoryTheory.IsIso ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.val g))

Sheafification sends the left-whiskered local equivalence to an isomorphism.

theorem SheafOfModules.isIso_sheafification_map_whiskerRight_of_whiskerLeft {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] (M : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj) {G₁ G₂ : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj} (g : G₁ ⟶ G₂) (h : CategoryTheory.IsIso ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g))) : CategoryTheory.IsIso ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight g M))

The two whiskerings are interchangeable.

Symmetry of the objectwise tensor product of module presheaves conjugates g ▷ M into M ◁ g, and sheafification is a functor, so it inverts one exactly when it inverts the other. Nothing here depends on the site, on M being a sheaf, or on any rank, flatness, or finiteness hypothesis on M: every such hypothesis a caller carries is spent proving the left-hand input, never this transfer. That is why the scheme consumer, whose stalkwise proof of the left-hand input needs no rank-one restriction, reuses this lemma rather than restating the conjugation.

theorem SheafOfModules.isIso_sheafification_map_whiskerRight_of_rankOneData {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), CategoryTheory.HasWeakSheafify (K.over X) AddCommGrpCat] [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules (SheafOfModules.ringSheaf✝ S)} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) {G₁ G₂ : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj} (g : G₁ ⟶ G₂) (hg : K.W ((PresheafOfModules.toPresheaf (SheafOfModules.ringSheaf✝ S).obj).map g)) : CategoryTheory.IsIso ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight g M.val))

Sheafification sends the right-whiskered local equivalence to an isomorphism.

theorem SheafOfModules.isIso_sheafification_map_whiskerLeft_unit_of_rankOneData {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), CategoryTheory.HasWeakSheafify (K.over X) AddCommGrpCat] [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules (SheafOfModules.ringSheaf✝ S)} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) (P : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj) : CategoryTheory.IsIso ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M.val ((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).unit.app P)))

Sheafification inverts left whiskering of its unit by a rank-one module sheaf.

theorem SheafOfModules.isIso_sheafification_map_whiskerRight_unit_of_rankOneData {D : Type u} [CategoryTheory.Category.{u, u} D] {K : CategoryTheory.GrothendieckTopology D} {S : CategoryTheory.Sheaf K CommRingCat} [CategoryTheory.HasWeakSheafify K AddCommGrpCat] [K.WEqualsLocallyBijective AddCommGrpCat] [∀ (X : D), CategoryTheory.HasWeakSheafify (K.over X) AddCommGrpCat] [∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules (SheafOfModules.ringSheaf✝ S)} (q : M.LocalGeneratorsData) [q.IsLocallyFreeData] (hq : q.IsRankOne) (P : PresheafOfModules (SheafOfModules.ringSheaf✝ S).obj) : CategoryTheory.IsIso ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).map (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (SheafOfModules.ringSheaf✝ S).obj)).unit.app P) M.val))

Sheafification inverts right whiskering of its unit by a rank-one module sheaf.