mathlib documentation

category_theory.category.preorder

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. Furthermore, galois connections correspond to adjoint functors.

Main definitions #

@[instance]

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
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
def has_le.le.hom {X : Type u} [preorder X] {x y : X} (h : x y) :
x y

Alias of hom_of_le.

@[simp]
theorem category_theory.hom_of_le_refl {X : Type u} [preorder X] {x : X} :
_.hom = 𝟙 x
@[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
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.

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

Alias of le_of_hom.

@[simp]
theorem category_theory.le_of_hom_hom_of_le {X : Type u} [preorder X] {x y : X} (h : x y) :
_ = h
@[simp]
theorem category_theory.hom_of_le_le_of_hom {X : Type u} [preorder X] {x y : X} (h : x y) :
_.hom = h
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
theorem category_theory.le_of_op_hom {X : Type u} [preorder X] {x y : Xᵒᵖ} (h : x y) :
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
@[simp]
theorem monotone.functor_obj {X : Type u} {Y : Type v} [preorder X] [preorder Y] {f : X → Y} (h : monotone f) :
def galois_connection.adjunction {X : Type u} {Y : Type v} [preorder X] [preorder Y] {l : X → Y} {u : Y → X} (gc : galois_connection l u) :

A galois connection between preorders induces an adjunction between the associated categories.

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

A functor between preorder categories is monotone.

theorem category_theory.adjunction.gc {X : Type u} {Y : Type v} [preorder X] [preorder Y] {L : X Y} {R : Y X} (adj : L R) :

An adjunction between preorder categories induces a galois connection.

The embedding of Preorder into Cat.

Equations
theorem category_theory.iso.to_eq {X : Type u} [partial_order X] {x y : X} (f : x y) :
x = y
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
@[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) :
@[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) :