Preorders as categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

hom_of_le and le_of_hom provide translations between inequalities in the preorder, and morphisms in the associated category.
monotone.functor is the functor associated to a monotone function.

source

@[protected, instance]

def preorder.small_category (α : Type u) [preorder α] :

category_theory.small_category α

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 category_theory.hom_of_le and category_theory.le_of_hom.

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

Equations

preorder.small_category α = {to_category_struct := {to_quiver := {hom := λ (U V : α), ulift (plift (U ≤ V))}, id := λ (X : α), {down := {down := _}}, comp := λ (X Y Z : α) (f : X ⟶ Y) (g : Y ⟶ Z), {down := {down := _}}}, id_comp' := _, comp_id' := _, assoc' := _}

source

def category_theory.hom_of_le {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

category_theory.hom_of_le h = {down := {down := h}}

source

def has_le.le.hom {X : Type u} [preorder X] {x y : X} (h : x ≤ y) :

x ⟶ y

Alias of category_theory.hom_of_le.

source

@[simp]

theorem category_theory.hom_of_le_refl {X : Type u} [preorder X] {x : X} :

_.hom = 𝟙 x

source

@[simp]

theorem category_theory.hom_of_le_comp {X : Type u} [preorder X] {x y z : X} (h : x ≤ y) (k : y ≤ z) :

h.hom ≫ k.hom = _.hom

source

theorem category_theory.le_of_hom {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

theorem quiver.hom.le {X : Type u} [preorder X] {x y : X} (h : x ⟶ y) :

x ≤ y

Alias of category_theory.le_of_hom.

source

@[simp]

theorem category_theory.le_of_hom_hom_of_le {X : Type u} [preorder X] {x y : X} (h : x ≤ y) :

_ = h

source

@[simp]

theorem category_theory.hom_of_le_le_of_hom {X : Type u} [preorder X] {x y : X} (h : x ⟶ y) :

_.hom = h

source

def category_theory.op_hom_of_le {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

category_theory.op_hom_of_le h = h.hom.op

source

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

opposite.unop y ≤ opposite.unop x

source

@[protected, instance]

def category_theory.unique_to_top {X : Type u} [preorder X] [order_top X] {x : X} :

unique (x ⟶ ⊤)

Equations

category_theory.unique_to_top = {to_inhabited := category_theory.unique_to_top._aux_1 x, uniq := _}

source

@[protected, instance]

def category_theory.unique_from_bot {X : Type u} [preorder X] [order_bot X] {x : X} :

unique (⊥ ⟶ x)

Equations

category_theory.unique_from_bot = {to_inhabited := category_theory.unique_from_bot._aux_1 x, uniq := _}

source

def monotone.functor {X : Type u} {Y : Type v} [preorder X] [preorder Y] {f : X → Y} (h : monotone f) :

X ⥤ Y

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

Equations

h.functor = {obj := f, map := λ (x₁ x₂ : X) (g : x₁ ⟶ x₂), _.hom, map_id' := _, map_comp' := _}

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

theorem category_theory.functor.monotone {X : Type u} {Y : Type v} [preorder X] [preorder Y] (f : X ⥤ Y) :

monotone f.obj

A functor between preorder categories is monotone.

source

theorem category_theory.iso.to_eq {X : Type u} [partial_order X] {x y : X} (f : x ≅ y) :

x = y

source

def category_theory.equivalence.to_order_iso {X : Type u} {Y : Type v} [partial_order X] [partial_order Y] (e : X ≌ Y) :

X ≃o Y

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

Equations

e.to_order_iso = {to_equiv := {to_fun := e.functor.obj, inv_fun := e.inverse.obj, left_inv := _, right_inv := _}, map_rel_iff' := _}

source

@[simp]

theorem category_theory.equivalence.to_order_iso_apply {X : Type u} {Y : Type v} [partial_order X] [partial_order Y] (e : X ≌ Y) (x : X) :

⇑(e.to_order_iso) x = e.functor.obj x

source

@[simp]

theorem category_theory.equivalence.to_order_iso_symm_apply {X : Type u} {Y : Type v} [partial_order X] [partial_order Y] (e : X ≌ Y) (y : Y) :

⇑(e.to_order_iso.symm) y = e.inverse.obj y