Documentation

Mathlib.Order.Category.Preord

Category of preorders #

This defines Preord, the category of preorders with monotone maps.

def Preord :
Type (u_1 + 1)

The category of preorders.

Equations
Instances For
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    def Preord.of (α : Type u_1) [Preorder α] :

    Construct a bundled Preord from the underlying type and typeclass.

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

      Constructs an equivalence between preorders from an order isomorphism between them.

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

        OrderDual as a functor.

        Equations
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem preordToCat_map :
            ∀ {X Y : Preord} (f : X Y), preordToCat.map f = .functor

            The embedding of Preord into Cat.

            Equations
            Instances For