Theorems · Definition · category theory

ModuleCat.FilteredColimits.colimit

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

The bundled R-module giving the filtered colimit of a diagram.

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

Cites8

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

CategoryTheory.Functorstatement and proof · cited by 16,252
Ringstatement and proof · cited by 7,463
ModuleCatstatement and proof · cited by 1,429
ModuleCat.ofproof · cited by 594
CategoryTheory.SmallCategorystatement and proof · cited by 480
AddCommGrpCat.carrierproof · cited by 407
CategoryTheory.IsFilteredstatement and proof · cited by 210
ModuleCat.FilteredColimits.Mproof · cited by 8

Cited by4

Results whose statement or proof uses this declaration.

ModuleCat.FilteredColimits.colimitCoconeproof · cited by 2
ModuleCat.FilteredColimits.colimitDescstatement and proof · cited by 2
ModuleCat.FilteredColimits.coconeMorphismstatement · cited by 0
ModuleCat.FilteredColimits.colimit.congr_simpstatement and proof · cited by 0