Theorems · Definition · category theory

PresheafOfModules.limitPresheafOfModules

{C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {J : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
          (F : CategoryTheory.Functor J (PresheafOfModules R)) →
            [∀ (X : Cᵒᵖ),
                  Small.{v, max u₂ v}
                    ↑((F.comp (PresheafOfModules.evaluation R X)).comp
                          (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections] →
              PresheafOfModules R

Given F : J ⥤ PresheafOfModules.{v} R, this is the presheaf of modules obtained by taking a limit in the category of modules over R.obj X for all X.

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Cited by

4 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategorySmall