# Documentation

Mathlib.Order.Category.PartOrd

# Category of partial orders #

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
Equations
def PartOrd.of (α : Type u_1) [] :

Construct a bundled PartOrd from the underlying type and typeclass.

Equations
Instances For
@[simp]
theorem PartOrd.coe_of (α : Type u_1) [] :
() = α
Equations
Equations
• = α.str
@[simp]
theorem PartOrd.Iso.mk_inv {α : PartOrd} {β : PartOrd} (e : α ≃o β) :
().inv = ()
@[simp]
theorem PartOrd.Iso.mk_hom {α : PartOrd} {β : PartOrd} (e : α ≃o β) :
().hom = e
def PartOrd.Iso.mk {α : PartOrd} {β : PartOrd} (e : α ≃o β) :
α β

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

Equations
Instances For
@[simp]
theorem PartOrd.dual_map :
∀ {X Y : PartOrd} (a : X →o Y), PartOrd.dual.map a = OrderHom.dual a
@[simp]

OrderDual as a functor.

Equations
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

antisymmetrization as a functor. It is the free functor.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• One or more equations did not get rendered due to their size.
Instances For

PreordToPartOrd and OrderDual commute.

Equations
Instances For