Theorems · Theorem · category theory

PresheafOfModules.limitCone_pt

∀ {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))
  [inst_2 :
    ∀ (X : Cᵒᵖ),
      Small.{v, max u₂ v}
        ↑((F.comp (PresheafOfModules.evaluation R X)).comp (CategoryTheory.forget (ModuleCat ↑(R.obj X)))).sections],
  (PresheafOfModules.limitCone F).pt = PresheafOfModules.limitPresheafOfModules F

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategorySmall