coyonedaEquiv_apply — Mathlib

English

There exists a natural isomorphism coyonedaEquiv between natural transformations from coyoneda to F and the elements F.obj X; i.e., coyonedaEquiv: (coyoneda.obj (op X) ⟶ F) ≃ F.obj X.

Русский

Существует естественный изоморфизм coyonedaEquiv между естественными преобразованиями от coyoneda к F и элементами F.obj X.

LaTeX

$$$\text{coyonedaEquiv}: (coyoneda.obj (op X) ⟶ F) \simeq F.obj X$$$

Lean4

theorem coyonedaEquiv_apply {X : C} {F : C ⥤ Type v₁} (f : coyoneda.obj (op X) ⟶ F) : coyonedaEquiv f = f.app X (𝟙 X) :=
  rfl

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