# 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
Equations
Equations
• X.instPartialOrderαToPartOrd = X.toPartOrd.str
def FinPartOrd.of (α : Type u_1) [] [] :

Construct a bundled FinPartOrd from PartialOrder + Fintype.

Equations
Instances For
@[simp]
theorem FinPartOrd.coe_of (α : Type u_1) [] [] :
().toPartOrd = α
Equations
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem FinPartOrd.Iso.mk_hom {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
.hom = e
@[simp]
theorem FinPartOrd.Iso.mk_inv {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
.inv = e.symm
def FinPartOrd.Iso.mk {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
α β

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

Equations
• = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
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.

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

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

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