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

    Construct a bundled FinPartOrd from PartialOrder + Fintype.

    Equations
    Instances For
      @[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
      Instances For
        @[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.
        Instances For
          @[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.
          Instances For