Theorems · Definition · category theory

ModuleCat.FilteredColimits.colimitCoconeIsColimit

{R : Type u} →
  [inst : Ring R] →
    {J : Type v} →
      [inst_1 : CategoryTheory.SmallCategory J] →
        [inst_2 : CategoryTheory.IsFiltered J] →
          (F : CategoryTheory.Functor J (ModuleCat R)) →
            CategoryTheory.Limits.IsColimit (ModuleCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in ModuleCat R.

Defined in: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Cited by: 0 results in Mathlib
Foundations: Depth 64 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Ring CategoryTheory.SmallCategory CategoryTheory.IsFiltered

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites14

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homproof · cited by 32,603
CategoryTheory.CategoryStruct.compproof · cited by 17,999
CategoryTheory.Functorstatement and proof · cited by 16,252
Ringstatement and proof · cited by 7,463
CategoryTheory.NatTrans.appproof · cited by 7,406
ModuleCatstatement and proof · cited by 1,429
CategoryTheory.Limits.Cocone.ptproof · cited by 1,354
CategoryTheory.Limits.IsColimitstatement · cited by 773
CategoryTheory.Limits.Coconeproof · cited by 746
CategoryTheory.Limits.Cocone.ιproof · cited by 605
CategoryTheory.SmallCategorystatement and proof · cited by 480
CategoryTheory.IsFilteredstatement and proof · cited by 210

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.