compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id

English

The Yoneda embedding has a Left Kan extension property for representables.

Русский

Функтор Янеда обладает свойством левое Kan-расширение для представимых объектов.

LaTeX

$$$((\yoneda.obj X) IsLeftKanExtension (yonedaMap F X))$$$

Lean4

@[simp]
theorem compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id (X : C) :
    ((compULiftYonedaIsoULiftYonedaCompLan.{w} F).inv.app X).app (op (F.obj X))
        ((F.op.lanUnit.app ((uliftYoneda.{max w v₂}).obj X)).app (op X) (ULift.up (𝟙 X))) =
      ULift.up (𝟙 (F.obj X)) :=
  (congr_fun
        (Functor.descOfIsLeftKanExtension_fac_app _ (F.op.lanUnit.app ((uliftYoneda.{max w v₂}).obj X)) _
          (uliftYonedaMap.{w} F X) (op X))
        (ULift.up (𝟙 X))).trans
    (by simp [uliftYonedaMap])

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