# mathlib3documentation

order.category.FinPartOrd

# The category of finite partial orders #

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

This defines FinPartOrd, the category of finite partial orders.

Note: FinPartOrd is not a subcategory of BddOrd because finite orders are not necessarily bounded.

## TODO #

FinPartOrd is equivalent to a small category.

structure FinPartOrd  :
Type (u_1+1)

The category of finite partial orders with monotone functions.

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

Construct a bundled FinPartOrd from fintype + partial_order.

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

Constructs an isomorphism of finite partial orders from an order isomorphism between them.

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

order_dual as a functor.

Equations

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

Equations
@[simp]
@[simp]