Theorems · Definition · category theory

ModuleCat.FilteredColimits.colimitCocone

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

The cocone over the proposed colimit module.

Defined in: Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Cited by: 2 results in Mathlib
Foundations: Depth 61 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.

Cites9

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.Functorstatement and proof · cited by 16,252
Ringstatement and proof · cited by 7,463
ModuleCatstatement and proof · cited by 1,429
CategoryTheory.Limits.Coconestatement · cited by 746
CategoryTheory.SmallCategorystatement and proof · cited by 480
CategoryTheory.IsFilteredstatement and proof · cited by 210
ModuleCat.FilteredColimits.colimitproof · cited by 1
ModuleCat.FilteredColimits.coconeMorphismproof · cited by 0

Cited by3

Results whose statement or proof uses this declaration.

ModuleCat.FilteredColimits.ι_colimitDescstatement and proof · cited by 1
ModuleCat.FilteredColimits.ι_colimitDesc_assocstatement and proof · cited by 0
ModuleCat.FilteredColimits.colimitCoconeIsColimitstatement and proof · cited by 0