Theorems · Definition · category theory

PresheafOfModules.limitCone

{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] →
              CategoryTheory.Limits.Cone F

The (limit) cone for F : J ⥤ PresheafOfModules.{v} R that is constructed from the limit of F ⋙ evaluation R X for all X.

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategorySmall