yonedaULiftEquiv — Mathlib

English

Compute the YonedaULift application: yonedaULiftEquiv_apply expresses the evaluation at identity morphism.

Русский

Вычисление применения yonedaULift: yonedaULiftEquiv_apply описывает возможность оценки по тождественному лему.

LaTeX

$$$yonedaULiftEquiv\_apply\ {X} {F} (f) = f.\val.app\ (op\ X) \ ⟨𝟙 X⟩$$$

Lean4

/-- A version of `yonedaEquiv` for `yonedaULift`. -/
def yonedaULiftEquiv {X : C} {F : Sheaf J (Type (max v v'))} : ((yonedaULift.{v'} J).obj X ⟶ F) ≃ F.val.obj (op X) :=
  (fullyFaithfulSheafToPresheaf _ _).homEquiv.trans uliftYonedaEquiv

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