Theorems · Definition · category theory

PresheafOfModules.ModuleColimit

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {cR : CategoryTheory.Limits.Cocone R} →
        {M : PresheafOfModules R} →
          {cM : CategoryTheory.Limits.Cocone M.presheaf} →
            CategoryTheory.Limits.IsColimit cR → CategoryTheory.Limits.IsColimit cM → Type w

Given a colimit cocone for a presheaf of rings R on a cofiltered category C, M a presheaf of modules over R, and a colimit cocone cM for the underlying functor Cᵒᵖ ⥤ AddCommGrpCat of M, this is the type cM.pt on which we define a module structure below.

Defined in

Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Cited by

22 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Category