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.

Construct a bundled FinPartOrd from PartialOrder + Fintype.

Equations
@[simp]
theorem FinPartOrd.coe_of (α : Type u_1) [PartialOrder α] [Fintype α] :
(of α).toPartOrd = α
Equations
  • One or more equations did not get rendered due to their size.
def FinPartOrd.Iso.mk {α β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
α β

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

Equations
@[simp]
theorem FinPartOrd.Iso.mk_inv {α β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
(mk e).inv = e.symm
@[simp]
theorem FinPartOrd.Iso.mk_hom {α β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
(mk e).hom = e

OrderDual as a functor.

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem FinPartOrd.dual_map {x✝ x✝¹ : FinPartOrd} (a : x✝.toPartOrd →o x✝¹.toPartOrd) :

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

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