mathlib documentation

order.category.Preorder

Category of preorders #

This defines Preorder, the category of preorders with monotone maps.

source
def Preorder  :
Type (u_1+1)

The category of preorders.

Equations
source
@[protected, instance]
def Preorder.order_hom.category_theory.bundled_hom  :
category_theory.bundled_hom order_hom
Equations
source
@[protected, instance]
def Preorder.large_category  :
category_theory.large_category Preorder
source
@[protected, instance]
def Preorder.concrete_category  :
category_theory.concrete_category Preorder
source
@[protected, instance]
def Preorder.has_coe_to_sort  :
has_coe_to_sort Preorder (Type u_1)
Equations
source
def Preorder.of (α : Type u_1) [preorder α] :
Preorder

Construct a bundled Preorder from the underlying type and typeclass.

Equations
source
@[protected, instance]
def Preorder.inhabited  :
inhabited Preorder
Equations
source
@[protected, instance]
def Preorder.preorder (α : Preorder) :
preorder ↥α
Equations
source
def Preorder.iso.mk {α β : Preorder} (e : ↥α ≃o ↥β) :
α ≅ β

Constructs an equivalence between preorders from an order isomorphism between them.

Equations
source
@[simp]
theorem Preorder.iso.mk_inv {α β : Preorder} (e : ↥α ≃o ↥β) :
(Preorder.iso.mk e).inv = ↑(e.symm)
source
@[simp]
theorem Preorder.iso.mk_hom {α β : Preorder} (e : ↥α ≃o ↥β) :
(Preorder.iso.mk e).hom = ↑e
source
@[simp]
theorem Preorder.to_dual_obj (X : Preorder) :
Preorder.to_dual.obj X = Preorder.of (order_dual ↥X)
source
def Preorder.to_dual  :
Preorder ⥤ Preorder

order_dual as a functor.

Equations
source
@[simp]
theorem Preorder.to_dual_map (X Y : Preorder) (ᾰ : ↥X →o ↥Y) :
Preorder.to_dual.map ᾰ = ⇑order_hom.dual ᾰ
source
@[simp]
theorem Preorder.dual_equiv_functor  :
Preorder.dual_equiv.functor = Preorder.to_dual
source
def Preorder.dual_equiv  :
Preorder ≌ Preorder

The equivalence between Preorder and itself induced by order_dual both ways.

Equations
source
@[simp]
theorem Preorder.dual_equiv_inverse  :
Preorder.dual_equiv.inverse = Preorder.to_dual