Theorems · Definition · category theory

AddGrpCat.FilteredColimits.colimitCoconeIsColimit

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [inst_1 : CategoryTheory.IsFiltered J] →
      (F : CategoryTheory.Functor J AddGrpCat) →
        CategoryTheory.Limits.IsColimit (AddGrpCat.FilteredColimits.colimitCocone F)

The proposed colimit cocone is a colimit in AddGroup.

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

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites11

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
CategoryTheory.Functor.compproof · cited by 6,529
CategoryTheory.Limits.IsColimitstatement · cited by 773
CategoryTheory.SmallCategorystatement and proof · cited by 480
CategoryTheory.forget₂proof · cited by 260
CategoryTheory.IsFilteredstatement and proof · cited by 210
AddGrpCatstatement and proof · cited by 80
AddMonCatproof · cited by 71
CategoryTheory.Limits.isColimitOfReflectsproof · cited by 19
AddMonCat.FilteredColimits.colimitCoconeIsColimitproof · cited by 0
AddGrpCat.FilteredColimits.colimitCoconestatement · cited by 0

Cited by1

Results whose statement or proof uses this declaration.

AddCommGrpCat.FilteredColimits.colimitCoconeIsColimitproof · cited by 2