# Documentation

Mathlib.Order.Category.FinPartOrd

# The category of finite partial orders #

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

Construct a bundled FinPartOrd from PartialOrder + Fintype.

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

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

Instances For
@[simp]
theorem FinPartOrd.dual_map {X : FinPartOrd} {Y : FinPartOrd} (a : X.toPartOrd →o Y.toPartOrd) :
FinPartOrd.dual.map a = OrderHom.dual a
@[simp]

OrderDual as a functor.

Instances For

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

Instances For