Cocones associated to principal segments

If f : α <i β is a principal segment and F : β ⥤ C, there is a cocone for f.monotone.functor ⋙ F : α ⥤ C the point of which is F.obj f.top.

def PrincipalSeg.cocone {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] (F : CategoryTheory.Functor β C) : CategoryTheory.Limits.Cocone (⋯.functor.comp F)

When f : α <i β and a functor F : β ⥤ C, this is the cocone for f.monotone.functor ⋙ F : α ⥤ C whose point if F.obj f.top.

Equations

• f.cocone F = { pt := F.obj f.top, ι := { app := fun (i : α) => F.map (CategoryTheory.homOfLE ⋯), naturality := ⋯ } }

@[simp]

theorem PrincipalSeg.cocone_ι_app {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] (F : CategoryTheory.Functor β C) (i : α) : (f.cocone F).ι.app i = F.map (CategoryTheory.homOfLE ⋯)

@[simp]

theorem PrincipalSeg.cocone_pt {α : Type u_1} {β : Type u_2} [PartialOrder α] [PartialOrder β] (f : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : β) => x1 < x2) {C : Type u_3} [CategoryTheory.Category.{u_4, u_3} C] (F : CategoryTheory.Functor β C) : (f.cocone F).pt = F.obj f.top