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.


FinPartOrd is equivalent to a small category.

structure FinPartOrd :
Type (u_1 + 1)

The category of finite partial orders with monotone functions.

Instances For

    Construct a bundled FinPartOrd from PartialOrder + Fintype.

    Instances For
      theorem FinPartOrd.coe_of (α : Type u_1) [PartialOrder α] [Fintype α] :
      (FinPartOrd.of α).toPartOrd = α
      theorem FinPartOrd.Iso.mk_inv {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
      theorem FinPartOrd.Iso.mk_hom {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
      ( e).hom = e
      def {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
      α β

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

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

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

        Instances For