mathlib3 documentation

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

Construct a bundled PartOrd from the underlying type and typeclass.

Equations
@[simp]
theorem PartOrd.coe_of (α : Type u_1) [partial_order α] :
@[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_map (X Y : PartOrd) (ᾰ : X →o Y) :

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