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

See https://stacks.math.columbia.edu/tag/00D3.

source

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

Subsingleton (U ⟶ V)

source

def CategoryTheory.homOfLE {X : Type u} [Preorder X] {x : X} {y : X} (h : x ≤ y) :

x ⟶ y

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

Instances For

source

def LE.le.hom {X : Type u} [Preorder X] {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

source

@[simp]

theorem CategoryTheory.homOfLE_refl {X : Type u} [Preorder X] {x : X} :

LE.le.hom (_ : x ≤ x) = CategoryTheory.CategoryStruct.id x

source

@[simp]

theorem CategoryTheory.homOfLE_comp {X : Type u} [Preorder X] {x : X} {y : X} {z : X} (h : x ≤ y) (k : y ≤ z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE h) (CategoryTheory.homOfLE k) = CategoryTheory.homOfLE (_ : x ≤ z)

source

theorem CategoryTheory.leOfHom {X : Type u} [Preorder X] {x : X} {y : X} (h : x ⟶ y) :

x ≤ y

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

source

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

x ≤ y

Alias of CategoryTheory.leOfHom.

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

source

theorem CategoryTheory.leOfHom_homOfLE {X : Type u} [Preorder X] {x : X} {y : X} (h : x ≤ y) :

(_ : x ≤ y) = h

source

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

LE.le.hom (_ : x ≤ y) = h

source

def CategoryTheory.opHomOfLE {X : Type u} [Preorder X] {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

source

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

y.unop ≤ x.unop

source

instance CategoryTheory.uniqueToTop {X : Type u} [Preorder X] [OrderTop X] {x : X} :

Unique (x ⟶ ⊤)

source

instance CategoryTheory.uniqueFromBot {X : Type u} [Preorder X] [OrderBot X] {x : X} :

Unique (⊥ ⟶ 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.

Instances For

source

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

source

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.

source

theorem CategoryTheory.Iso.to_eq {X : Type u} [PartialOrder X] {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.

Instances For

source

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

source

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