mathlib3 documentation

category_theory.category.preorder

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 #

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

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) :
@[protected, instance]
def category_theory.unique_to_top {X : Type u} [preorder X] [order_top X] {x : X} :
Equations
@[protected, instance]
def category_theory.unique_from_bot {X : Type u} [preorder X] [order_bot X] {x : X} :
Equations
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) :
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.iso.to_eq {X : Type u} [partial_order X] {x y : X} (f : x y) :
x = 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]