uliftYonedaEquiv_presheafHom_uliftYoneda_obj

English

The Yoneda-based equivalence, when specialized to the case uliftYoneda.obj X, sends presheafHom φ to the corresponding φ-component at X, after evaluating at the image of X under F.op.

Русский

Эквивалент Ёнеда, полученный при фиксированном X и ULift, переводит presheafHom φ в соответствующий компонент φ при X после оценки по F.op.

LaTeX

$$$$ uliftYonedaEquiv.{max w v₂} (presheafHom.{w} φ (uliftYoneda.{max w v₂}.obj X)) = ((φ.app X).app (F.op.obj (Opposite.op X)) (ULift.up (\mathbb{1}))) $$$$

Lean4

theorem uliftYonedaEquiv_presheafHom_uliftYoneda_obj (X : C) :
    uliftYonedaEquiv.{max w v₂} (presheafHom.{w} φ (uliftYoneda.{max w v₂}.obj X)) =
      ((φ.app X).app (F.op.obj (Opposite.op X)) (ULift.up (𝟙 _))) :=
  by simpa using uliftYonedaEquiv_ι_presheafHom.{w} φ (uliftYoneda.obj X) (𝟙 _)

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