# mathlibdocumentation

order.category.FinPartialOrder

# The category of finite partial orders #

This defines FinPartialOrder, the category of finite partial orders.

Note: FinPartialOrder is NOT a subcategory of BoundedOrder because its morphisms do not preserve ⊥ and ⊤.

## TODO #

FinPartialOrder is equivalent to a small category.

structure FinPartialOrder  :
Type (u_1+1)

The category of finite partial orders with monotone functions.

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

Construct a bundled FinPartialOrder from fintype + partial_order.

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

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

Equations

order_dual as a functor.

Equations

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

Equations