mathlib documentation

category_theory.limits.over

@[simp]
theorem category_theory.functor.to_cocone_ι_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J category_theory.over X) (j : J) :
F.to_cocone.ι.app j = (F.obj j).hom

We can interpret a functor F into the category of arrows with codomain X as a cocone over the diagram given by the domains of the arrows in the image of F such that the apex of the cocone is X.

Equations

We can interpret a functor F into the category of arrows with domain X as a cone over the diagram given by the codomains of the arrows in the image of F such that the apex of the cone is X.

Equations
@[simp]
theorem category_theory.functor.to_cone_π_app {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] {X : C} (F : J category_theory.under X) (j : J) :
F.to_cone.π.app j = (F.obj j).hom

@[simp]

A colimit of F ⋙ over.forget induces a cocone over F. This is an implementation detail, use the has_colimit instance provided below.

Equations

A limit of F ⋙ under.forget induces a cone over F. This is an implementation detail, use the has_limit instance provided below.

Equations