Theorems · Definition · category theory

AddCommGrpCat.FilteredColimits.colimitCocone

{J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    [CategoryTheory.IsFiltered J] → (F : CategoryTheory.Functor J AddCommGrpCat) → CategoryTheory.Limits.Cocone F

The cocone over the proposed colimit additive commutative group.

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

Cites14

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.NatTrans.appproof · cited by 7,406
CategoryTheory.Functor.compproof · cited by 6,529
CategoryTheory.Limits.Coconestatement · cited by 746
CategoryTheory.Limits.Cocone.ιproof · cited by 605
CategoryTheory.SmallCategorystatement and proof · cited by 480
AddCommGrpCatstatement and proof · cited by 462
CategoryTheory.forget₂proof · cited by 260
CategoryTheory.IsFilteredstatement and proof · cited by 210
AddGrpCatproof · cited by 80
AddCommGrpCat.ofHomproof · cited by 72
AddGrpCat.Hom.homproof · cited by 20

Cited by4

Results whose statement or proof uses this declaration.

AddCommGrpCat.FilteredColimits.colimitCoconeIsColimitstatement · cited by 2
ModuleCat.FilteredColimits.colimitDescproof · cited by 2
CategoryTheory.Limits.IsColimit.ι_smulproof · cited by 2
ModuleCat.FilteredColimits.coconeMorphismproof · cited by 0