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
    Equations
    Equations
    • X.instPartialOrderαToPartOrd = X.toPartOrd.str

    Construct a bundled FinPartOrd from PartialOrder + Fintype.

    Equations
    Instances For
      @[simp]
      theorem FinPartOrd.coe_of (α : Type u_1) [PartialOrder α] [Fintype α] :
      (FinPartOrd.of α).toPartOrd = α
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem FinPartOrd.Iso.mk_inv {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
      (FinPartOrd.Iso.mk e).inv = e.symm
      @[simp]
      theorem FinPartOrd.Iso.mk_hom {α : FinPartOrd} {β : FinPartOrd} (e : α.toPartOrd ≃o β.toPartOrd) :
      (FinPartOrd.Iso.mk e).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.

      Equations
      • FinPartOrd.Iso.mk e = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
      Instances For
        @[simp]
        @[simp]
        theorem FinPartOrd.dual_map {X : FinPartOrd} {Y : FinPartOrd} (a : X.toPartOrd →o Y.toPartOrd) :
        FinPartOrd.dual.map a = OrderHom.dual a

        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