Theorems · Definition · category theory

CategoryTheory.Limits.Cocone.pt

{J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} → CategoryTheory.Limits.Cocone F → C

An object of C

Defined in: Mathlib.CategoryTheory.Limits.Cones
Cited by: 1,354 results in Mathlib
Foundations: Depth 3 from the axioms, rests on 4 definitions · 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 and proof · cited by 16,252
CategoryTheory.Limits.Coconestatement and proof · cited by 746

Cited by1,913

Results whose statement or proof uses this declaration.

CategoryTheory.Limits.Cocone.ιstatement · cited by 605
CategoryTheory.Limits.colimitproof · cited by 453
CategoryTheory.Limits.Cofan.injstatement · cited by 170
CategoryTheory.Limits.colimit.ι_descstatement · cited by 170
CategoryTheory.Limits.Cofork.πstatement · cited by 164
CategoryTheory.Limits.IsColimit.descstatement · cited by 144
CategoryTheory.Limits.CoconeMorphism.homstatement · cited by 137
CategoryTheory.Limits.Cocone.precomposeproof · cited by 87
CategoryTheory.Limits.IsColimit.facstatement · cited by 82
CategoryTheory.Limits.IsColimit.coconePointUniqueUpToIsostatement · cited by 67
CategoryTheory.Limits.colimit.descstatement · cited by 63
CategoryTheory.Limits.IsColimit.hom_extstatement and proof · cited by 58

Showing the 200 most cited of 1,913.