Preorders as categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
We install a category instance on any preorder. This is not to be confused with the category of
preorders, defined in
We show that monotone functions between preorders correspond to functors of the associated
Main definitions #
le_of_hom provide translations between inequalities in the preorder, and
morphisms in the associated category.
monotone.functor is the functor associated to a monotone function.
Express an inequality as a morphism in the corresponding preorder category.
Extract the underlying inequality from a morphism in a preorder category.
Construct a morphism in the opposite of a preorder category from an inequality.
A monotone function between preorders induces a functor between the associated categories.
A functor between preorder categories is monotone.
A categorical equivalence between partial orders is just an order isomorphism.