restrictedULiftYoneda — Mathlib

Lean4

/-- Given a functor `A : C ⥤ ℰ` (with `Category.{v₂} ℰ`) and a auxiliary universe `w`,
this is the functor `ℰ ⥤ Cᵒᵖ ⥤ Type (max w v₂)` which sends `(E : ℰ) (c : Cᵒᵖ)`
to the homset `A.obj C ⟶ E` (considered in the higher universe `max w v₂`).
Under the existence of a suitable pointwise left Kan extension, it is shown in
`uliftYonedaAdjunction` that this functor has a left adjoint.

Defined as in [MM92], Chapter I, Section 5, Theorem 2.
-/
@[simps! obj_map map_app]
def restrictedULiftYoneda : ℰ ⥤ Cᵒᵖ ⥤ Type (max w v₂) :=
  uliftYoneda.{w} ⋙ (Functor.whiskeringLeft _ _ _).obj A.op

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