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 #
homOfLEandleOfHomprovide translations between inequalities in the preorder, and morphisms in the associated category.Monotone.functoris the functor associated to a monotone function.
@[instance 100]
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.
Equations
Equations
- ⋯ = ⋯
Express an inequality as a morphism in the corresponding preorder category.
Equations
- CategoryTheory.homOfLE h = { down := { down := h } }
Instances For
@[simp]
theorem
CategoryTheory.homOfLE_refl
{X : Type u}
[Preorder X]
{x : X}
(h : x ≤ x)
:
h.hom = CategoryTheory.CategoryStruct.id x
@[simp]
theorem
CategoryTheory.homOfLE_comp
{X : Type u}
[Preorder X]
{x : X}
{y : X}
{z : X}
(h : x ≤ y)
(k : y ≤ z)
:
@[reducible, inline]
Extract the underlying inequality from a morphism in a preorder category.
Equations
Instances For
theorem
CategoryTheory.homOfLE_isIso_of_eq
{X : Type u}
[Preorder X]
{x : X}
{y : X}
(h : x ≤ y)
(heq : x = y)
:
@[simp]
theorem
CategoryTheory.homOfLE_comp_eqToHom
{X : Type u}
[Preorder X]
{a : X}
{b : X}
{c : X}
(hab : a ≤ b)
(hbc : b = c)
:
@[simp]
theorem
CategoryTheory.eqToHom_comp_homOfLE
{X : Type u}
[Preorder X]
{a : X}
{b : X}
{c : X}
(hab : a = b)
(hbc : b ≤ c)
:
@[simp]
theorem
CategoryTheory.homOfLE_op_comp_eqToHom
{X : Type u}
[Preorder X]
{a : X}
{b : X}
{c : X}
(hab : b ≤ a)
(hbc : Opposite.op b = Opposite.op c)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.homOfLE hab).op (CategoryTheory.eqToHom hbc) = (CategoryTheory.homOfLE ⋯).op
theorem
CategoryTheory.homOfLE_op_comp_eqToHom_assoc
{X : Type u}
[Preorder X]
{a : X}
{b : X}
{c : X}
(hab : b ≤ a)
(hbc : Opposite.op b = Opposite.op c)
{Z : Xᵒᵖ}
(h : Opposite.op c ⟶ Z)
:
@[simp]
theorem
CategoryTheory.eqToHom_comp_homOfLE_op
{X : Type u}
[Preorder X]
{a : X}
{b : X}
{c : X}
(hab : Opposite.op a = Opposite.op b)
(hbc : c ≤ b)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom hab) (CategoryTheory.homOfLE hbc).op = (CategoryTheory.homOfLE ⋯).op
theorem
CategoryTheory.eqToHom_comp_homOfLE_op_assoc
{X : Type u}
[Preorder X]
{a : X}
{b : X}
{c : X}
(hab : Opposite.op a = Opposite.op b)
(hbc : c ≤ b)
{Z : Xᵒᵖ}
(h : Opposite.op c ⟶ Z)
:
def
CategoryTheory.opHomOfLE
{X : Type u}
[Preorder X]
{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
Instances For
Equations
- CategoryTheory.uniqueToTop = { default := CategoryTheory.homOfLE ⋯, uniq := ⋯ }
Equations
- CategoryTheory.uniqueFromBot = { default := CategoryTheory.homOfLE ⋯, uniq := ⋯ }
@[simp]
theorem
CategoryTheory.orderDualEquivalence_inverse_map
(X : Type u)
[Preorder X]
:
∀ {X_1 Y : Xᵒᵖ} (f : X_1 ⟶ Y), (CategoryTheory.orderDualEquivalence X).inverse.map f = CategoryTheory.homOfLE ⋯
@[simp]
theorem
CategoryTheory.orderDualEquivalence_functor_obj
(X : Type u)
[Preorder X]
(x : Xᵒᵈ)
:
(CategoryTheory.orderDualEquivalence X).functor.obj x = Opposite.op (OrderDual.ofDual x)
@[simp]
theorem
CategoryTheory.orderDualEquivalence_functor_map
(X : Type u)
[Preorder X]
:
∀ {X_1 Y : Xᵒᵈ} (f : X_1 ⟶ Y), (CategoryTheory.orderDualEquivalence X).functor.map f = (CategoryTheory.homOfLE ⋯).op
@[simp]
theorem
CategoryTheory.orderDualEquivalence_inverse_obj
(X : Type u)
[Preorder X]
(x : Xᵒᵖ)
:
(CategoryTheory.orderDualEquivalence X).inverse.obj x = OrderDual.toDual (Opposite.unop x)
@[simp]
@[simp]
theorem
CategoryTheory.orderDualEquivalence_counitIso
(X : Type u)
[Preorder X]
:
(CategoryTheory.orderDualEquivalence X).counitIso = CategoryTheory.Iso.refl
({ obj := fun (x : Xᵒᵖ) => OrderDual.toDual (Opposite.unop x),
map := fun {X_1 Y : Xᵒᵖ} (f : X_1 ⟶ Y) => CategoryTheory.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) => (CategoryTheory.homOfLE ⋯).op, map_id := ⋯, map_comp := ⋯ })
def
Monotone.functor
{X : Type u}
{Y : Type v}
[Preorder X]
[Preorder Y]
{f : X → Y}
(h : Monotone f)
:
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
@[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 ⋯) ⋯
@[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 ⋯) ⋯
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.
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' := ⋯ }
Instances For
@[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
@[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