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
andleOfHom
provide translations between inequalities in the preorder, and morphisms in the associated category.Monotone.functor
is the functor associated to a monotone function.
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}
[Preorder α]
(U : α)
(V : α)
:
Subsingleton (U ⟶ V)
@[simp]
theorem
CategoryTheory.homOfLE_refl
{X : Type u}
[Preorder X]
{x : X}
:
LE.le.hom (_ : x ≤ x) = CategoryTheory.CategoryStruct.id x
@[simp]
theorem
CategoryTheory.homOfLE_comp
{X : Type u}
[Preorder X]
{x : X}
{y : X}
{z : X}
(h : x ≤ y)
(k : y ≤ z)
:
@[simp]
theorem
Monotone.functor_obj
{X : Type u}
{Y : Type v}
[Preorder X]
[Preorder Y]
{f : X → Y}
(h : Monotone f)
:
(Monotone.functor h).toPrefunctor.obj = f
theorem
CategoryTheory.Functor.monotone
{X : Type u}
{Y : Type v}
[Preorder X]
[Preorder Y]
(f : CategoryTheory.Functor X Y)
:
Monotone f.obj
A functor between preorder categories is monotone.
def
CategoryTheory.Equivalence.toOrderIso
{X : Type u}
{Y : Type v}
[PartialOrder X]
[PartialOrder Y]
(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}
[PartialOrder X]
[PartialOrder Y]
(e : X ≌ Y)
(x : X)
:
↑(CategoryTheory.Equivalence.toOrderIso e) x = e.functor.obj x
@[simp]
theorem
CategoryTheory.Equivalence.toOrderIso_symm_apply
{X : Type u}
{Y : Type v}
[PartialOrder X]
[PartialOrder Y]
(e : X ≌ Y)
(y : Y)
:
↑(OrderIso.symm (CategoryTheory.Equivalence.toOrderIso e)) y = e.inverse.obj y