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
andleOfHom
provide translations between inequalities in the preorder, and morphisms in the associated category.Monotone.functor
is 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
.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
@[reducible, inline]
Extract the underlying inequality from a morphism in a preorder category.
Equations
Instances For
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
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
@[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)
:
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
@[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)
:
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
def
CategoryTheory.opHomOfLE
{X : Type u}
[Preorder X]
{x y : Xᵒᵖ}
(h : Opposite.unop x ≤ Opposite.unop y)
:
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]
@[simp]
@[simp]
@[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 := ⋯ })
@[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 ⋯) ⋯
def
CategoryTheory.Equivalence.toOrderIso
{X : Type u}
{Y : Type v}
[PartialOrder X]
[PartialOrder Y]
(e : X ≌ Y)
:
A categorical equivalence between partial orders is just an order isomorphism.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Equivalence.toOrderIso_apply
{X : Type u}
{Y : Type v}
[PartialOrder X]
[PartialOrder Y]
(e : X ≌ Y)
(x : X)
:
@[simp]
theorem
CategoryTheory.Equivalence.toOrderIso_symm_apply
{X : Type u}
{Y : Type v}
[PartialOrder X]
[PartialOrder Y]
(e : X ≌ Y)
(y : Y)
: