English
An explicit equivalence between the category of monotone maps and the category of functors is given by sending a monotone map to its induced functor and vice versa.
Русский
Существует явная эквиваленция между категорией монотонных отображений и категорией функторов: монотонное отображение сопоставляется функтору, и наоборот.
LaTeX
$$$\text{equivalenceFunctor}: (X \too Y) \simeq (X ⥤ Y)$$$
Lean4
/-- The categorical equivalence between the category of monotone functions `X →o Y` and the category
of functors `X ⥤ Y`, where `X` and `Y` are preorder categories. -/
@[simps! functor_obj_obj inverse_obj unitIso_hom_app unitIso_inv_app counitIso_inv_app_app counitIso_hom_app_app]
def equivalenceFunctor : (X →o Y) ≌ (X ⥤ Y)
where
functor :=
{ obj f := f.toFunctor
map f := { app x := homOfLE <| leOfHom f x } }
inverse :=
{ obj F := F.toOrderHom
map f := homOfLE fun x ↦ leOfHom <| f.app x }
unitIso := Iso.refl _
counitIso := Iso.refl _
