Theorems · Definition · algebraic geometry

SheafOfModules.QuasicoherentData.pushforward

{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) →
                                    [inst_9 :
                                        ∀ (X : D),
                                          (CategoryTheory.Over.post G).IsContinuous (K.over X) (J.over (G.obj X))] →
                                      (∀ (X : D) (Y : C) (f : G.obj X ⟶ Y),
                                          CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max (max u u₁) v₁,
                                              max (max u u₂) v₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂}
                                            (SheafOfModules.pushforward
                                              (((CategoryTheory.Over.forget X).sheafPushforwardContinuous RingCat
                                                    (K.over X) K).map
                                                φ))) →
                                        {M : SheafOfModules R} →
                                          M.QuasicoherentData → ((SheafOfModules.pushforward φ).obj M).QuasicoherentData

The pushforward of SheafOfModules.QuasicoherentData along a continuous and cocontinuous functor.

Defined in

Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent

Cited by

3 results in Mathlib

Foundations

Depth 116 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.IsContinuous