equivFunctor — Mathlib

English

There is an equivalence between the type of order-homs X →o Y and the type of functors X ⥤ Y.

Русский

Существует эквиваленция между множеством отображений порядка X →o Y и множеством функторов X ⥤ Y.

LaTeX

$$$(X \too Y) \simeq (X ⥤ Y)$$$

Lean4

/-- The equivalence between `X →o Y` and the type of functors `X ⥤ Y` between preorder categories
`X` and `Y`. -/
@[simps]
def equivFunctor : (X →o Y) ≃ (X ⥤ Y) where
  toFun := toFunctor
  invFun F := F.toOrderHom

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