English
There is a bijection between morphisms (coyoneda.obj X ⋙ uliftFunctor ⟶ F) and objects F.obj X.unop, natural in F and X. The toFun sends φ to φ.app X.unop (ULift.up (id_X)); the inverse sends f to the natural transformation app := (fun _ x => F.map (ULift.down x) f).
Русский
Существует биекция между отображениями (coyoneda.obj X ⋙ uliftFunctor ⟶ F) и элементами F.obj X.unop; отображение осуществляется через φ ↦ φ.app X.unop (ULift.up 𝟙); обратное отображение задаётся какapp := ...
LaTeX
$$$$ (coyonedaCompUliftFunctorEquiv (F) (X)) : (coyoneda.obj X \circ uliftFunctor \rightarrow F) \simeq F(X^{unop}) $$$$
Lean4
/-- A bijection `(coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj (unop X)` which is a variant
of `coyonedaEquiv` with heterogeneous universes. -/
def coyonedaCompUliftFunctorEquiv (F : C ⥤ Type max v₁ w) (X : Cᵒᵖ) : (coyoneda.obj X ⋙ uliftFunctor ⟶ F) ≃ F.obj X.unop
where
toFun φ := φ.app X.unop (ULift.up (𝟙 _))
invFun f := { app := fun _ x => F.map (ULift.down x) f }
left_inv
φ := by
ext Y f
dsimp
rw [← FunctorToTypes.naturality]
dsimp
rw [Category.id_comp]
rfl
right_inv f := by simp
