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

Stacks Tag 00D3

Equations

Preorder.smallCategory α = CategoryTheory.Category.mk ⋯ ⋯ ⋯

source

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

Subsingleton (U ⟶ V)

source

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.

Equations

CategoryTheory.homOfLE h = { down := { down := h } }

source

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

Equations

@LE.le.hom = @CategoryTheory.homOfLE

source

@[simp]

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

h.hom = CategoryStruct.id x

source

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

source

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.

source

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

Equations

@Quiver.Hom.le = @CategoryTheory.leOfHom

source

@[simp]

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

⋯.hom = h

source

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

IsIso (homOfLE h)

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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

source

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.

Equations

CategoryTheory.opHomOfLE h = (CategoryTheory.homOfLE h).op

source

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

Opposite.unop y ≤ Opposite.unop x

source

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

Unique (x ⟶ ⊤)

Equations

CategoryTheory.uniqueToTop = { default := CategoryTheory.homOfLE ⋯, uniq := ⋯ }

source

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

Unique (⊥ ⟶ x)

Equations

CategoryTheory.uniqueFromBot = { default := CategoryTheory.homOfLE ⋯, uniq := ⋯ }

source

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.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.orderDualEquivalence_inverse_map (X : Type u) [Preorder X] {X✝ Y✝ : Xᵒᵖ} (f : X✝ ⟶ Y✝) :

(orderDualEquivalence X).inverse.map f = homOfLE ⋯

source

@[simp]

theorem CategoryTheory.orderDualEquivalence_unitIso (X : Type u) [Preorder X] :

(orderDualEquivalence X).unitIso = Iso.refl (Functor.id Xᵒᵈ)

source

@[simp]

theorem CategoryTheory.orderDualEquivalence_functor_obj (X : Type u) [Preorder X] (x : Xᵒᵈ) :

(orderDualEquivalence X).functor.obj x = Opposite.op (OrderDual.ofDual x)

source

@[simp]

theorem CategoryTheory.orderDualEquivalence_inverse_obj (X : Type u) [Preorder X] (x : Xᵒᵖ) :

(orderDualEquivalence X).inverse.obj x = OrderDual.toDual (Opposite.unop x)

source

@[simp]

theorem CategoryTheory.orderDualEquivalence_functor_map (X : Type u) [Preorder X] {X✝ Y✝ : Xᵒᵈ} (f : X✝ ⟶ Y✝) :

(orderDualEquivalence X).functor.map f = (homOfLE ⋯).op

source

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

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.

Equations

h.functor = { obj := f, map := fun {X_1 Y_1 : X} (g : X_1 ⟶ Y_1) => CategoryTheory.homOfLE ⋯, map_id := ⋯, map_comp := ⋯ }

Instances For

instFullFunctor

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

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

⋯.functor.Full

source

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.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

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

e.equivalence.functor = ⋯.functor

source

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

source

@[simp]

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

e.equivalence.inverse = ⋯.functor

source

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

source

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.

source

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

Equations

e.toOrderIso = { toFun := e.functor.obj, invFun := e.inverse.obj, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

source

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

source

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

source

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

CategoryTheory.IsIso f ↔ a = b

Documentation

Mathlib.CategoryTheory.Category.Preorder

Preorders as categories #

Main definitions #