Theorems · Definition · category theory

CategoryTheory.Limits.ColimitPresentation.diag

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type w} →
      [inst_1 : CategoryTheory.Category.{t, w} J] →
        {X : C} → CategoryTheory.Limits.ColimitPresentation J X → CategoryTheory.Functor J C

The diagram {Dᵢ}.

Defined in: Mathlib.CategoryTheory.Limits.Presentation
Cited by: 62 results in Mathlib
Foundations: Depth 2 from the axioms · uses no axioms
Assumes: CategoryTheory.Category CategoryTheory.Category

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

CategoryTheory.Categorystatement and proof · cited by 32,673
CategoryTheory.Functorstatement · cited by 16,252
CategoryTheory.Limits.ColimitPresentationstatement and proof · cited by 54

Cited by86

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.ColimitPresentation.ιstatement · cited by 33
CategoryTheory.Limits.ColimitPresentation.isColimitstatement · cited by 19
CategoryTheory.ObjectProperty.ColimitOfShape.prop_diag_objstatement · cited by 17
CategoryTheory.ObjectProperty.indproof · cited by 11
CategoryTheory.Limits.ColimitPresentation.Total.Hom.homstatement · cited by 9
CategoryTheory.ObjectProperty.colimitsClosure_leproof · cited by 6
CategoryTheory.Limits.ColimitPresentation.mapproof · cited by 6
CategoryTheory.Limits.ColimitPresentation.reindexproof · cited by 6
CategoryTheory.Limits.ColimitPresentation.bindstatement and proof · cited by 5
CategoryTheory.Limits.ColimitPresentation.ofIsoproof · cited by 5
CategoryTheory.Limits.ColimitPresentation.changeDiagstatement and proof · cited by 3
CategoryTheory.Limits.ColimitPresentation.wstatement · cited by 3