mathlib documentation

order.category.PartialOrder

Category of partial orders #

This defines PartialOrder, the category of partial orders with monotone maps.

source
def PartialOrder  :
Type (u_1+1)

The category of partially ordered types.

Equations
source
@[protected, instance]
def PartialOrder.partial_order.to_preorder.category_theory.bundled_hom.parent_projection  :
category_theory.bundled_hom.parent_projection partial_order.to_preorder
Equations
source
@[protected, instance]
def PartialOrder.concrete_category  :
category_theory.concrete_category PartialOrder
source
@[protected, instance]
def PartialOrder.large_category  :
category_theory.large_category PartialOrder
source
@[protected, instance]
def PartialOrder.has_coe_to_sort  :
has_coe_to_sort PartialOrder (Type u_1)
Equations
source
def PartialOrder.of (α : Type u_1) [partial_order α] :
PartialOrder

Construct a bundled PartialOrder from the underlying type and typeclass.

Equations
source
@[protected, instance]
def PartialOrder.inhabited  :
inhabited PartialOrder
Equations
source
@[protected, instance]
def PartialOrder.partial_order (α : PartialOrder) :
partial_order ↥α
Equations
source
@[protected, instance]
def PartialOrder.has_forget_to_Preorder  :
category_theory.has_forget₂ PartialOrder Preorder
Equations
source
@[simp]
theorem PartialOrder.iso.mk_hom {α β : PartialOrder} (e : ↥α ≃o ↥β) :
(PartialOrder.iso.mk e).hom = ↑e
source
def PartialOrder.iso.mk {α β : PartialOrder} (e : ↥α ≃o ↥β) :
α ≅ β

Constructs an equivalence between partial orders from an order isomorphism between them.

Equations
source
@[simp]
theorem PartialOrder.iso.mk_inv {α β : PartialOrder} (e : ↥α ≃o ↥β) :
(PartialOrder.iso.mk e).inv = ↑(e.symm)
source
def PartialOrder.to_dual  :
PartialOrder ⥤ PartialOrder

order_dual as a functor.

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

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

Equations
source
@[simp]
theorem PartialOrder.dual_equiv_inverse  :
PartialOrder.dual_equiv.inverse = PartialOrder.to_dual
source
theorem PartialOrder_to_dual_comp_forget_to_Preorder  :
PartialOrder.to_dual ⋙ category_theory.forget₂ PartialOrder Preorder = category_theory.forget₂ PartialOrder Preorder ⋙ Preorder.to_dual