Theorems · Theorem · algebraic geometry

SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat]
  [inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] {D : Type u₂}
  [inst_3 : CategoryTheory.Category.{v₂, u₂} D] {K : CategoryTheory.GrothendieckTopology D}
  {S : CategoryTheory.Sheaf K RingCat} [inst_4 : ∀ (X : D), (K.over X).WEqualsLocallyBijective AddCommGrpCat]
  [∀ (X : C), CategoryTheory.HasSheafify (J.over X) AddCommGrpCat]
  [inst_6 : ∀ (X : D), CategoryTheory.HasSheafify (K.over X) AddCommGrpCat] (G : CategoryTheory.Functor D C)
  [inst_7 : G.IsContinuous K J] [G.IsCocontinuous K J] (φ : S ⟶ (G.sheafPushforwardContinuous RingCat K J).obj R)
  (η : (SheafOfModules.pushforward φ).obj (SheafOfModules.unit R) ≅ SheafOfModules.unit S) [G.IsLeftAdjoint]
  [CategoryTheory.IsIso φ] [∀ (X : D), (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))]
  [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasPullbacks D] {M : SheafOfModules R}
  [M.IsQuasicoherent], ((SheafOfModules.pushforward φ).obj M).IsQuasicoherent

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

1 results in Mathlib

Foundations

Depth 118 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.HasWeakSheafifyCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.CategoryCategoryTheory.GrothendieckTopology.WEqualsLocallyBijectiveCategoryTheory.HasSheafifyCategoryTheory.HasSheafifyCategoryTheory.Functor.IsContinuousCategoryTheory.Functor.IsCocontinuousCategoryTheory.Functor.IsLeftAdjointCategoryTheory.IsIsoCategoryTheory.Functor.IsContinuousCategoryTheory.Limits.HasPullbacksCategoryTheory.Limits.HasPullbacksSheafOfModules.IsQuasicoherent