# mathlibdocumentation

order.category.PartialOrder

# Category of partial orders #

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

def PartialOrder  :
Type (u_1+1)

The category of partially ordered types.

Equations
Instances for PartialOrder
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
def PartialOrder.has_coe_to_sort  :
(Type u_1)
Equations
def PartialOrder.of (α : Type u_1)  :

Construct a bundled PartialOrder from the underlying type and typeclass.

Equations
@[simp]
theorem PartialOrder.coe_of (α : Type u_1)  :
= α
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
theorem PartialOrder.iso.mk_hom {α β : PartialOrder} (e : α ≃o β) :
= e
def PartialOrder.iso.mk {α β : PartialOrder} (e : α ≃o β) :
α β

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

Equations
@[simp]
theorem PartialOrder.iso.mk_inv {α β : PartialOrder} (e : α ≃o β) :
= (e.symm)

order_dual as a functor.

Equations
@[simp]
@[simp]
theorem PartialOrder.dual_map (X Y : PartialOrder) (ᾰ : X →o Y) :
@[simp]

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

Equations
@[simp]

antisymmetrization as a functor. It is the free functor.

Equations

Preorder_to_PartialOrder is left adjoint to the forgetful functor, meaning it is the free functor from Preorder to PartialOrder.

Equations

Preorder_to_PartialOrder and order_dual commute.

Equations
@[simp]