Theorems · Theorem · category theory

PresheafOfModules.limitPresheafOfModules_map

∀ {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]
  {x Y : Cᵒᵖ} (f : x ⟶ Y),
  (PresheafOfModules.limitPresheafOfModules F).map f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.limMap (F.whiskerLeft (PresheafOfModules.restriction R f)))
      (CategoryTheory.preservesLimitIso (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))
          (F.comp (PresheafOfModules.evaluation R Y))).inv

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.Limits

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategorySmall