# mathlib3documentation

order.category.PartOrd

# Category of partial orders #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def PartOrd  :
Type (u_1+1)

The category of partially ordered types.

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

Construct a bundled PartOrd from the underlying type and typeclass.

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

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

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

order_dual as a functor.

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

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

Equations

antisymmetrization as a functor. It is the free functor.

Equations

Preord_to_PartOrd is left adjoint to the forgetful functor, meaning it is the free functor from Preord to PartOrd.

Equations
@[simp]

Preord_to_PartOrd and order_dual commute.

Equations
@[simp]