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.

@[implicit_reducible, 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.

instance Preorder.subsingleton_hom {α : Type u} [Preorder α] (U V : α) : Subsingleton (U ⟶ V)

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.

@[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.

@[simp]

theorem CategoryTheory.homOfLE_refl {X : Type u} [Preorder X] {x : X} (h : x ≤ x) : h.hom = CategoryStruct.id x

@[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 ⋯

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.

@[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.

@[simp]

theorem CategoryTheory.homOfLE_leOfHom {X : Type u} [Preorder X] {x y : X} (h : x ⟶ y) : ⋯.hom = h

theorem CategoryTheory.homOfLE_isIso_of_eq {X : Type u} [Preorder X] {x y : X} (h : x ≤ y) (heq : x = y) : IsIso (homOfLE h)

theorem CategoryTheory.isIso_homOfLE {X : Type u} [Preorder X] {x y : X} (h : x = y) : IsIso (homOfLE ⋯)

@[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 ⋯

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

@[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 ⋯

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

@[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

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

@[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

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

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.

theorem CategoryTheory.le_of_op_hom {X : Type u} [Preorder X] {x y : Xᵒᵖ} (h : x ⟶ y) : Opposite.unop y ≤ Opposite.unop x

@[implicit_reducible]

instance CategoryTheory.uniqueToTop {X : Type u} [Preorder X] [OrderTop X] {x : X} : Unique (x ⟶ ⊤)

@[implicit_reducible]

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

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.

@[simp]

theorem CategoryTheory.orderDualEquivalence_functor_map (X : Type u) [Preorder X] {X✝ Y✝ : Xᵒᵈ} (f : X✝ ⟶ Y✝) : (orderDualEquivalence X).functor.map f = (homOfLE ⋯).op

@[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 := ⋯ })

@[simp]

theorem CategoryTheory.orderDualEquivalence_unitIso (X : Type u) [Preorder X] : (orderDualEquivalence X).unitIso = Iso.refl (Functor.id Xᵒᵈ)

@[simp]

theorem CategoryTheory.orderDualEquivalence_inverse_map (X : Type u) [Preorder X] {X✝ Y✝ : Xᵒᵖ} (f : X✝ ⟶ Y✝) : (orderDualEquivalence X).inverse.map f = homOfLE ⋯

@[simp]

theorem CategoryTheory.orderDualEquivalence_functor_obj (X : Type u) [Preorder X] (x : Xᵒᵈ) : (orderDualEquivalence X).functor.obj x = Opposite.op (OrderDual.ofDual x)

@[simp]

theorem CategoryTheory.orderDualEquivalence_inverse_obj (X : Type u) [Preorder X] (x : Xᵒᵖ) : (orderDualEquivalence X).inverse.obj x = OrderDual.toDual (Opposite.unop x)

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.

@[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

instance instFullFunctor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X ↪o Y) : ⋯.functor.Full

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.

@[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 ⋯) ⋯

@[simp]

theorem OrderIso.equivalence_inverse {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) : e.equivalence.inverse = ⋯.functor

@[simp]

theorem OrderIso.equivalence_functor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) : e.equivalence.functor = ⋯.functor

@[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 ⋯) ⋯

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.

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.

@[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✝

@[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.

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.

@[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

@[simp]

theorem OrderHom.equivFunctor_apply {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X →o Y) : equivFunctor f = f.toFunctor

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.

@[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

@[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✝¹)

@[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

@[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✝

@[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✝¹)

@[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✝

theorem CategoryTheory.Iso.to_eq {X : Type u} [PartialOrder X] {x y : X} (f : x ≅ y) : x = y

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.

@[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

@[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

theorem PartialOrder.isIso_iff_eq {X : Type u} [PartialOrder X] {a b : X} (f : a ⟶ b) : CategoryTheory.IsIso f ↔ a = b