natTrans_app_uliftYoneda_obj — Mathlib

English

For each object X, the X-component of the natural transformation natTrans φ is given by composing the inverse of a canonical map with φ.app X.

Русский

Для каждого объекта X компонент инференции natTrans φ задаётся как композиция обратного канонического отображения и φ.app X.

LaTeX

$$$$ (natTrans.{w} φ).app (uliftYoneda.{max w v₂}.obj X) = (compULiftYonedaIsoULiftYonedaCompLan.{w} F).inv.app X \;\gg\; φ.app X $$$$

Lean4

theorem natTrans_app_uliftYoneda_obj (X : C) :
    (natTrans.{w} φ).app (uliftYoneda.{max w v₂}.obj X) =
      (compULiftYonedaIsoULiftYonedaCompLan.{w} F).inv.app X ≫ φ.app X :=
  by
  dsimp [natTrans]
  apply (F.op.lan.obj (uliftYoneda.obj X)).hom_ext_of_isLeftKanExtension (F.op.lanUnit.app _)
  rw [Functor.descOfIsLeftKanExtension_fac]
  apply uliftYonedaEquiv.injective
  rw [uliftYonedaEquiv_presheafHom_uliftYoneda_obj]
  exact congr_arg _ (compULiftYonedaIsoULiftYonedaCompLan_inv_app_app_apply_eq_id F X).symm

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