Preorders as categories #
We install a category instance on any preorder. This is not to be confused with the category of
preorders, defined in order/category/Preorder
.
We show that monotone functions between preorders correspond to functors of the associated categories. Furthermore, galois connections correspond to adjoint functors.
Main definitions #
hom_of_le
andle_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.galois_connection.adjunction
is the adjunction associated to a galois connection.Preorder_to_Cat
is the functor embedding the category of preorders intoCat
.
The category structure coming from a preorder. There is a morphism X ⟶ Y
if and only if X ≤ Y
.
Because we don't allow morphisms to live in Prop
,
we have to define X ⟶ Y
as ulift (plift (X ≤ Y))
.
See category_theory.hom_of_le
and category_theory.le_of_hom
.
Express an inequality as a morphism in the corresponding preorder category.
Equations
- category_theory.hom_of_le h = {down := {down := h}}
Alias of category_theory.hom_of_le
.
Extract the underlying inequality from a morphism in a preorder category.
Alias of category_theory.le_of_hom
.
Construct a morphism in the opposite of a preorder category from an inequality.
Equations
Equations
- category_theory.unique_to_top = {to_inhabited := category_theory.unique_to_top._aux_1 x, uniq := _}
Equations
- category_theory.unique_from_bot = {to_inhabited := category_theory.unique_from_bot._aux_1 x, uniq := _}
A monotone function between preorders induces a functor between the associated categories.
A galois connection between preorders induces an adjunction between the associated categories.
Equations
- gc.adjunction = category_theory.adjunction.mk_of_hom_equiv {hom_equiv := λ (X_1 : X) (Y_1 : Y), {to_fun := λ (f : _.functor.obj X_1 ⟶ Y_1), _.hom, inv_fun := λ (f : X_1 ⟶ _.functor.obj Y_1), _.hom, left_inv := _, right_inv := _}, hom_equiv_naturality_left_symm' := _, hom_equiv_naturality_right' := _}
An adjunction between preorder categories induces a galois connection.
A categorical equivalence between partial orders is just an order isomorphism.