instIsRightKanExtensionObjRanAppRanCounit

English

For every F : C → H, the object L.ran.obj F carries a universal right Kan extension structure with the counit map L.ranCounit.app F.

Русский

Для каждого F : C → H объект L.ran.obj F обладает свойством справаKan расширения с аппроксимацией counit через L.ranCounit.app F.

LaTeX

$$$ \\forall F:\\, C \\to H,\\; (L.\\mathrm{ran.obj} F).IsRightKanExtension (L.\\mathrm{ranCounit}.app F). $$$

Lean4

instance (F : C ⥤ H) : (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F) :=
  by
  dsimp [ran, ranCounit]
  infer_instance

Похожие утверждения