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

source
@[instance 100]
instance Preorder.smallCategory (α : Type u) [Preorder α] :
CategoryTheory.SmallCategory α

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

Equations

- One or more equations did not get rendered due to their size.

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

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

Equations

- CategoryTheory.homOfLE h = { down := { down := h } }

Instances For

source
@[reducible, inline]
abbrev LE.le.hom {X : Type u_1} [Preorder X] {x y : X} (h : x ≤ y) :
x ⟶ y

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

Equations

- @LE.le.hom = @CategoryTheory.homOfLE

Instances For

source
@[simp]
theorem CategoryTheory.homOfLE_refl {X : Type u} [Preorder X] {x : X} (h : x ≤ x) :
h.hom = CategoryStruct.id x
source
@[simp]
theorem CategoryTheory.homOfLE_comp {X : Type u} [Preorder X] {x y z : X} (h : x ≤ y) (k : y ≤ z) :
CategoryStruct.comp (homOfLE h) (homOfLE k) = homOfLE ⋯
source
theorem CategoryTheory.leOfHom {X : Type u} [Preorder X] {x y : X} (h : x ⟶ y) :
x ≤ y

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

source
@[reducible, inline]
abbrev Quiver.Hom.le {X : Type u_1} [Preorder X] {x y : X} (h : x ⟶ y) :
x ≤ y

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

Equations

- @Quiver.Hom.le = @CategoryTheory.leOfHom

Instances For

source
@[simp]
theorem CategoryTheory.homOfLE_leOfHom {X : Type u} [Preorder X] {x y : X} (h : x ⟶ y) :
⋯.hom = h
source
theorem CategoryTheory.homOfLE_isIso_of_eq {X : Type u} [Preorder X] {x y : X} (h : x ≤ y) (heq : x = y) :
IsIso (homOfLE h)
source
@[simp]
theorem CategoryTheory.homOfLE_comp_eqToHom {X : Type u} [Preorder X] {a b c : X} (hab : a ≤ b) (hbc : b = c) :
CategoryStruct.comp (homOfLE hab) (eqToHom hbc) = homOfLE ⋯
source
theorem CategoryTheory.homOfLE_comp_eqToHom_assoc {X : Type u} [Preorder X] {a b c : X} (hab : a ≤ b) (hbc : b = c) {Z : X} (h : c ⟶ Z) :
CategoryStruct.comp (homOfLE hab) (CategoryStruct.comp (eqToHom hbc) h) = CategoryStruct.comp (homOfLE ⋯) h
source
@[simp]
theorem CategoryTheory.eqToHom_comp_homOfLE {X : Type u} [Preorder X] {a b c : X} (hab : a = b) (hbc : b ≤ c) :
CategoryStruct.comp (eqToHom hab) (homOfLE hbc) = homOfLE ⋯
source
theorem CategoryTheory.eqToHom_comp_homOfLE_assoc {X : Type u} [Preorder X] {a b c : X} (hab : a = b) (hbc : b ≤ c) {Z : X} (h : c ⟶ Z) :
CategoryStruct.comp (eqToHom hab) (CategoryStruct.comp (homOfLE hbc) h) = CategoryStruct.comp (homOfLE ⋯) h
source
@[simp]
theorem CategoryTheory.homOfLE_op_comp_eqToHom {X : Type u} [Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c) :
CategoryStruct.comp (homOfLE hab).op (eqToHom hbc) = (homOfLE ⋯).op
source
theorem CategoryTheory.homOfLE_op_comp_eqToHom_assoc {X : Type u} [Preorder X] {a b c : X} (hab : b ≤ a) (hbc : Opposite.op b = Opposite.op c) {Z : X ᵒᵖ} (h : Opposite.op c ⟶ Z) :
CategoryStruct.comp (homOfLE hab).op (CategoryStruct.comp (eqToHom hbc) h) = CategoryStruct.comp (homOfLE ⋯).op h
source
@[simp]
theorem CategoryTheory.eqToHom_comp_homOfLE_op {X : Type u} [Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b) :
CategoryStruct.comp (eqToHom hab) (homOfLE hbc).op = (homOfLE ⋯).op
source
theorem CategoryTheory.eqToHom_comp_homOfLE_op_assoc {X : Type u} [Preorder X] {a b c : X} (hab : Opposite.op a = Opposite.op b) (hbc : c ≤ b) {Z : X ᵒᵖ} (h : Opposite.op c ⟶ Z) :
CategoryStruct.comp (eqToHom hab) (CategoryStruct.comp (homOfLE hbc).op h) = CategoryStruct.comp (homOfLE ⋯).op h
source
def CategoryTheory.opHomOfLE {X : Type u} [Preorder X] {x y : X ᵒᵖ} (h : Opposite.unop x ≤ Opposite.unop y) :
y ⟶ x

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

Equations

- CategoryTheory.opHomOfLE h = (CategoryTheory.homOfLE h).op

Instances For

source
theorem CategoryTheory.le_of_op_hom {X : Type u} [Preorder X] {x y : X ᵒᵖ} (h : x ⟶ y) :
Opposite.unop y ≤ Opposite.unop x
source
instance CategoryTheory.uniqueToTop {X : Type u} [Preorder X] [OrderTop X] {x : X} :
Unique (x ⟶ ⊤)
Equations

- CategoryTheory.uniqueToTop = { default := CategoryTheory.homOfLE ⋯, uniq := ⋯ }

source
instance CategoryTheory.uniqueFromBot {X : Type u} [Preorder X] [OrderBot X] {x : X} :
Unique (⊥ ⟶ x)
Equations

- CategoryTheory.uniqueFromBot = { default := CategoryTheory.homOfLE ⋯, uniq := ⋯ }

source
def CategoryTheory.orderDualEquivalence (X : Type u) [Preorder X] :
X ᵒᵈ ≌ X ᵒᵖ

The equivalence of categories from the order dual of a preordered type `X` to the opposite category of the preorder `X`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.orderDualEquivalence_functor_map (X : Type u) [Preorder X] {X✝ Y✝ : X ᵒᵈ} (f : X✝ ⟶ Y✝) :
(orderDualEquivalence X).functor.map f = (homOfLE ⋯).op
source
@[simp]
theorem CategoryTheory.orderDualEquivalence_counitIso (X : Type u) [Preorder X] :
(orderDualEquivalence X).counitIso = Iso.refl ({ obj := fun (x : X ᵒᵖ) => OrderDual.toDual (Opposite.unop x), map := fun {X_1 Y : X ᵒᵖ} (f : X_1 ⟶ Y) => homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }.comp { obj := fun (x : X ᵒᵈ) => Opposite.op (OrderDual.ofDual x), map := fun {X_1 Y : X ᵒᵈ} (f : X_1 ⟶ Y) => (homOfLE ⋯).op, map_id := ⋯, map_comp := ⋯ })
source
@[simp]
theorem CategoryTheory.orderDualEquivalence_inverse_map (X : Type u) [Preorder X] {X✝ Y✝ : X ᵒᵖ} (f : X✝ ⟶ Y✝) :
(orderDualEquivalence X).inverse.map f = homOfLE ⋯
source
@[simp]
theorem CategoryTheory.orderDualEquivalence_functor_obj (X : Type u) [Preorder X] (x : X ᵒᵈ) :
(orderDualEquivalence X).functor.obj x = Opposite.op (OrderDual.ofDual x)
source
@[simp]
theorem CategoryTheory.orderDualEquivalence_unitIso (X : Type u) [Preorder X] :
(orderDualEquivalence X).unitIso = Iso.refl (Functor.id X ᵒᵈ)
source
@[simp]
theorem CategoryTheory.orderDualEquivalence_inverse_obj (X : Type u) [Preorder X] (x : X ᵒᵖ) :
(orderDualEquivalence X).inverse.obj x = OrderDual.toDual (Opposite.unop x)
source
def Monotone.functor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {f : X → Y} (h : Monotone f) :
CategoryTheory.Functor X Y

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

Equations

- h.functor = { obj := f, map := fun {X_1 Y_1 : X} (g : X_1 ⟶ Y_1) => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }

Instances For

source
@[simp]
theorem Monotone.functor_obj {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {f : X → Y} (h : Monotone f) :
h.functor.obj = f
source
instance instFullFunctor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X ↪o Y) :
⋯.functor.Full
source
def OrderIso.equivalence {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
X ≌ Y

The equivalence of categories `X ≌ Y` induced by `e : X ≃o Y`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem OrderIso.equivalence_inverse {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
e.equivalence.inverse = ⋯.functor
source
@[simp]
theorem OrderIso.equivalence_unitIso {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
e.equivalence.unitIso = CategoryTheory.NatIso.ofComponents (fun (x : X) => CategoryTheory.eqToIso ⋯) ⋯
source
@[simp]
theorem OrderIso.equivalence_counitIso {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
e.equivalence.counitIso = CategoryTheory.NatIso.ofComponents (fun (x : Y) => CategoryTheory.eqToIso ⋯) ⋯
source
@[simp]
theorem OrderIso.equivalence_functor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
e.equivalence.functor = ⋯.functor
source
theorem CategoryTheory.Functor.monotone {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : Functor X Y) :
Monotone f.obj

A functor between preorder categories is monotone.

source
def CategoryTheory.Functor.toOrderHom {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (F : Functor X Y) :
X →o Y

A functor `X ⥤ Y` between preorder categories as an `OrderHom`.

Equations

- F.toOrderHom = { toFun := F.obj, monotone' := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Functor.toOrderHom_coe {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (F : Functor X Y) (a✝ : X) :
F.toOrderHom a✝ = F.obj a✝
source
@[reducible, inline]
abbrev OrderHom.toFunctor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X →o Y) :
CategoryTheory.Functor X Y

An `OrderHom` as a functor `X ⥤ Y` between preorder categories.

Equations

- f.toFunctor = ⋯.functor

Instances For

source
def OrderHom.equivFunctor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] :
(X →o Y) ≃ CategoryTheory.Functor X Y

The equivalence between `X →o Y` and the type of functors `X ⥤ Y` between preorder categories `X` and `Y`.

Equations

- OrderHom.equivFunctor = { toFun := OrderHom.toFunctor, invFun := fun (F : CategoryTheory.Functor X Y) => F.toOrderHom, left_inv := ⋯, right_inv := ⋯ }

Instances For

source
@[simp]
theorem OrderHom.equivFunctor_apply {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X →o Y) :
equivFunctor f = f.toFunctor
source
@[simp]
theorem OrderHom.equivFunctor_symm_apply {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (F : CategoryTheory.Functor X Y) :
equivFunctor.symm F = F.toOrderHom
source
def OrderHom.equivalenceFunctor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] :
X →o Y ≌ CategoryTheory.Functor X Y

The categorical equivalence between the category of monotone functions `X →o Y` and the category of functors `X ⥤ Y`, where `X` and `Y` are preorder categories.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem OrderHom.equivalenceFunctor_inverse_obj {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (F : CategoryTheory.Functor X Y) :
equivalenceFunctor.inverse.obj F = F.toOrderHom
source
@[simp]
theorem OrderHom.equivalenceFunctor_unitIso_inv_app {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (X✝ : X →o Y) :
equivalenceFunctor.unitIso.inv.app X✝ = CategoryTheory.CategoryStruct.id X✝
source
@[simp]
theorem OrderHom.equivalenceFunctor_counitIso_hom_app_app {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (X✝ : CategoryTheory.Functor X Y) (X✝¹ : X) :
(equivalenceFunctor.counitIso.hom.app X✝).app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.obj X✝¹)
source
@[simp]
theorem OrderHom.equivalenceFunctor_functor_obj_obj {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X →o Y) (a : X) :
(equivalenceFunctor.functor.obj f).obj a = f a
source
@[simp]
theorem OrderHom.equivalenceFunctor_unitIso_hom_app {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (X✝ : X →o Y) :
equivalenceFunctor.unitIso.hom.app X✝ = CategoryTheory.CategoryStruct.id X✝
source
@[simp]
theorem OrderHom.equivalenceFunctor_counitIso_inv_app_app {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (X✝ : CategoryTheory.Functor X Y) (X✝¹ : X) :
(equivalenceFunctor.counitIso.inv.app X✝).app X✝¹ = CategoryTheory.CategoryStruct.id (X✝.obj X✝¹)
source
theorem CategoryTheory.Iso.to_eq {X : Type u} [PartialOrder X] {x y : X} (f : x ≅ y) :
x = y
source
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.

Equations

- e.toOrderIso = { toFun := e.functor.obj, invFun := e.inverse.obj, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

Instances For

source
@[simp]
theorem CategoryTheory.Equivalence.toOrderIso_apply {X : Type u} {Y : Type v} [PartialOrder X] [PartialOrder Y] (e : X ≌ Y) (x : X) :
e.toOrderIso x = e.functor.obj x
source
@[simp]
theorem CategoryTheory.Equivalence.toOrderIso_symm_apply {X : Type u} {Y : Type v} [PartialOrder X] [PartialOrder Y] (e : X ≌ Y) (y : Y) :
e.toOrderIso.symm y = e.inverse.obj y
source
theorem PartialOrder.isIso_iff_eq {X : Type u} [PartialOrder X] {a b : X} (f : a ⟶ b) :
CategoryTheory.IsIso f ↔ a = b