Documentation

Mathlib.Order.Category.BddOrd

The category of bounded orders #

This defines BddOrd, the category of bounded orders.

structure BddOrd :
Type (u_1 + 1)

The category of bounded orders with monotone functions.

  • toPartOrd : PartOrd

    The underlying object in the category of partial orders.

  • isBoundedOrder : BoundedOrder self.toPartOrd
Instances For
    Equations
    • X.instPartialOrderαToPartOrd = X.toPartOrd.str
    def BddOrd.of (α : Type u_1) [PartialOrder α] [BoundedOrder α] :

    Construct a bundled BddOrd from a Fintype PartialOrder.

    Equations
    Instances For
      @[simp]
      theorem BddOrd.coe_of (α : Type u_1) [PartialOrder α] [BoundedOrder α] :
      (BddOrd.of α).toPartOrd = α
      instance BddOrd.instFunLike (X : BddOrd) (Y : BddOrd) :
      FunLike (X Y) X.toPartOrd Y.toPartOrd
      Equations
      • X.instFunLike Y = inferInstance
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem BddOrd.dual_obj (X : BddOrd) :
      BddOrd.dual.obj X = BddOrd.of (↑X.toPartOrd)ᵒᵈ
      @[simp]
      theorem BddOrd.dual_map {X : BddOrd} {Y : BddOrd} (a : BoundedOrderHom X.toPartOrd Y.toPartOrd) :
      BddOrd.dual.map a = BoundedOrderHom.dual a

      OrderDual as a functor.

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

        Constructs an equivalence between bounded orders from an order isomorphism between them.

        Equations
        • BddOrd.Iso.mk e = { hom := e, inv := e.symm, hom_inv_id := , inv_hom_id := }
        Instances For

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

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