# Documentation

Mathlib.CategoryTheory.Category.Preorder

# 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.

## Main definitions #

• homOfLE and leOfHom provide translations between inequalities in the preorder, and morphisms in the associated category.
• Monotone.functor is the functor associated to a monotone function.
instance Preorder.smallCategory (α : Type u) [] :

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 CategoryTheory.homOfLE and CategoryTheory.leOfHom.

instance Preorder.Preorder.subsingleton_hom {α : Type u} [] (U : α) (V : α) :
def CategoryTheory.homOfLE {X : Type u} [] {x : X} {y : X} (h : x y) :
x y

Express an inequality as a morphism in the corresponding preorder category.

Instances For
def LE.le.hom {X : Type u} [] {x : X} {y : X} (h : x y) :
x y

Alias of CategoryTheory.homOfLE.

Express an inequality as a morphism in the corresponding preorder category.

Instances For
@[simp]
theorem CategoryTheory.homOfLE_refl {X : Type u} [] {x : X} :
LE.le.hom (_ : x x) =
@[simp]
theorem CategoryTheory.homOfLE_comp {X : Type u} [] {x : X} {y : X} {z : X} (h : x y) (k : y z) :
theorem CategoryTheory.leOfHom {X : Type u} [] {x : X} {y : X} (h : x y) :
x y

Extract the underlying inequality from a morphism in a preorder category.

theorem Quiver.Hom.le {X : Type u} [] {x : X} {y : X} (h : x y) :
x y

Alias of CategoryTheory.leOfHom.

Extract the underlying inequality from a morphism in a preorder category.

theorem CategoryTheory.leOfHom_homOfLE {X : Type u} [] {x : X} {y : X} (h : x y) :
(_ : x y) = h
theorem CategoryTheory.homOfLE_leOfHom {X : Type u} [] {x : X} {y : X} (h : x y) :
LE.le.hom (_ : x y) = h
def CategoryTheory.opHomOfLE {X : Type u} [] {x : Xᵒᵖ} {y : Xᵒᵖ} (h : x.unop y.unop) :
y x

Construct a morphism in the opposite of a preorder category from an inequality.

Instances For
theorem CategoryTheory.le_of_op_hom {X : Type u} [] {x : Xᵒᵖ} {y : Xᵒᵖ} (h : x y) :
y.unop x.unop
instance CategoryTheory.uniqueToTop {X : Type u} [] [] {x : X} :
instance CategoryTheory.uniqueFromBot {X : Type u} [] [] {x : X} :
def Monotone.functor {X : Type u} {Y : Type v} [] [] {f : XY} (h : ) :

A monotone function between preorders induces a functor between the associated categories.

Instances For
@[simp]
theorem Monotone.functor_obj {X : Type u} {Y : Type v} [] [] {f : XY} (h : ) :
().toPrefunctor.obj = f
theorem CategoryTheory.Functor.monotone {X : Type u} {Y : Type v} [] [] (f : ) :
Monotone f.obj

A functor between preorder categories is monotone.

theorem CategoryTheory.Iso.to_eq {X : Type u} [] {x : X} {y : X} (f : x y) :
x = y
def CategoryTheory.Equivalence.toOrderIso {X : Type u} {Y : Type v} [] [] (e : X Y) :
X ≃o Y

A categorical equivalence between partial orders is just an order isomorphism.

Instances For
@[simp]
theorem CategoryTheory.Equivalence.toOrderIso_apply {X : Type u} {Y : Type v} [] [] (e : X Y) (x : X) :
= e.functor.obj x
@[simp]
theorem CategoryTheory.Equivalence.toOrderIso_symm_apply {X : Type u} {Y : Type v} [] [] (e : X Y) (y : Y) :
= e.inverse.obj y