Documentation

Mathlib.CategoryTheory.Category.Preorder

Preorders as categories #

We install a category instance on any preorder. This is not to be confused with the category of preorders, defined in Order.Category.Preorder.

We show that monotone functions between preorders correspond to functors of the associated categories.

Main definitions #

The category structure coming from a preorder. There is a morphism X ⟶ Y if and only if X ≤ Y.

Because we don't allow morphisms to live in Prop, we have to define X ⟶ Y as ULift (PLift (X ≤ Y)). See CategoryTheory.homOfLE and CategoryTheory.leOfHom.

See https://stacks.math.columbia.edu/tag/00D3.

Equations
def CategoryTheory.homOfLE {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
x y

Express an inequality as a morphism in the corresponding preorder category.

Equations
Instances For
    def LE.le.hom {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
    x y

    Alias of CategoryTheory.homOfLE.


    Express an inequality as a morphism in the corresponding preorder category.

    Equations
    Instances For
      theorem CategoryTheory.leOfHom {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
      x y

      Extract the underlying inequality from a morphism in a preorder category.

      theorem Quiver.Hom.le {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
      x y

      Alias of CategoryTheory.leOfHom.


      Extract the underlying inequality from a morphism in a preorder category.

      theorem CategoryTheory.leOfHom_homOfLE {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
      (_ : x y) = h
      theorem CategoryTheory.homOfLE_leOfHom {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
      LE.le.hom (_ : x y) = h
      def CategoryTheory.opHomOfLE {X : Type u} [Preorder X] {x : Xᵒᵖ} {y : Xᵒᵖ} (h : x.unop y.unop) :
      y x

      Construct a morphism in the opposite of a preorder category from an inequality.

      Equations
      Instances For
        theorem CategoryTheory.le_of_op_hom {X : Type u} [Preorder X] {x : Xᵒᵖ} {y : Xᵒᵖ} (h : x y) :
        y.unop x.unop
        instance CategoryTheory.uniqueToTop {X : Type u} [Preorder X] [OrderTop X] {x : X} :
        Equations
        instance CategoryTheory.uniqueFromBot {X : Type u} [Preorder X] [OrderBot X] {x : X} :
        Equations
        def Monotone.functor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {f : XY} (h : Monotone f) :

        A monotone function between preorders induces a functor between the associated categories.

        Equations
        Instances For
          @[simp]
          theorem Monotone.functor_obj {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {f : XY} (h : Monotone f) :
          (Monotone.functor h).toPrefunctor.obj = f

          A functor between preorder categories is monotone.

          theorem CategoryTheory.Iso.to_eq {X : Type u} [PartialOrder X] {x : X} {y : X} (f : x y) :
          x = y

          A categorical equivalence between partial orders is just an order isomorphism.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem CategoryTheory.Equivalence.toOrderIso_apply {X : Type u} {Y : Type v} [PartialOrder X] [PartialOrder Y] (e : X Y) (x : X) :
            ↑(CategoryTheory.Equivalence.toOrderIso e) x = e.functor.obj x
            @[simp]