Documentation

Mathlib.Order.Category.PartOrd

Category of partial orders #

This defines PartOrd, the category of partial orders with monotone maps.

def PartOrd :
Type (u_1 + 1)

The category of partially ordered types.

Equations
Instances For
    Equations
    def PartOrd.of (α : Type u_1) [PartialOrder α] :

    Construct a bundled PartOrd from the underlying type and typeclass.

    Equations
    Instances For
      @[simp]
      theorem PartOrd.coe_of (α : Type u_1) [PartialOrder α] :
      (PartOrd.of α) = α
      Equations
      • α.instPartialOrderα = α.str
      @[simp]
      theorem PartOrd.Iso.mk_hom {α : PartOrd} {β : PartOrd} (e : α ≃o β) :
      (PartOrd.Iso.mk e).hom = e
      @[simp]
      theorem PartOrd.Iso.mk_inv {α : PartOrd} {β : PartOrd} (e : α ≃o β) :
      (PartOrd.Iso.mk e).inv = e.symm
      def PartOrd.Iso.mk {α : PartOrd} {β : PartOrd} (e : α ≃o β) :
      α β

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

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

        OrderDual as a functor.

        Equations
        Instances For

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

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

            Antisymmetrization as a functor. It is the free functor.

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

              preordToPartOrd is left adjoint to the forgetful functor, meaning it is the free functor from Preord to PartOrd.

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

                PreordToPartOrd and OrderDual commute.

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