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 #

@[instance 100]

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
instance Preorder.subsingleton_hom {α : Type u} [Preorder α] (U : α) (V : α) :
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
    @[reducible, inline]
    abbrev LE.le.hom {X : Type u_1} [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
      @[simp]
      theorem CategoryTheory.homOfLE_refl {X : Type u} [Preorder X] {x : X} (h : x x) :
      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.

      @[reducible, inline]
      abbrev Quiver.Hom.le {X : Type u_1} [Preorder X] {x : X} {y : X} (h : x y) :
      x y

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

      Equations
      Instances For
        theorem CategoryTheory.leOfHom_homOfLE {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
        = h
        theorem CategoryTheory.homOfLE_leOfHom {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) :
        .hom = h
        theorem CategoryTheory.homOfLE_isIso_of_eq {X : Type u} [Preorder X] {x : X} {y : X} (h : x y) (heq : x = y) :

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

        Equations
        Instances For
          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
          @[simp]
          @[simp]
          @[simp]
          @[simp]
          theorem CategoryTheory.orderDualEquivalence_counitIso (X : Type u) [Preorder X] :
          (CategoryTheory.orderDualEquivalence X).counitIso = CategoryTheory.Iso.refl ({ obj := fun (x : Xᵒᵖ) => OrderDual.toDual (Opposite.unop x), map := fun {X_1 Y : Xᵒᵖ} (f : X_1 Y) => CategoryTheory.homOfLE , map_id := , map_comp := }.comp { obj := fun (x : Xᵒᵈ) => Opposite.op (OrderDual.ofDual x), map := fun {X_1 Y : Xᵒᵈ} (f : X_1 Y) => (CategoryTheory.homOfLE ).op, map_id := , map_comp := })

          The equivalence of categories from the order dual of a preordered type X to the opposite category of the preorder X.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            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
            • h.functor = { obj := f, map := fun {X_1 Y_1 : X} (g : X_1 Y_1) => CategoryTheory.homOfLE , map_id := , map_comp := }
            Instances For
              @[simp]
              theorem Monotone.functor_obj {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] {f : XY} (h : Monotone f) :
              h.functor.obj = f
              instance instFullFunctor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (f : X ↪o Y) :
              .functor.Full
              Equations
              • =
              @[simp]
              theorem OrderIso.equivalence_inverse {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
              e.equivalence.inverse = .functor
              @[simp]
              theorem OrderIso.equivalence_counitIso {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
              e.equivalence.counitIso = CategoryTheory.NatIso.ofComponents (fun (x : Y) => CategoryTheory.eqToIso )
              @[simp]
              theorem OrderIso.equivalence_unitIso {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
              e.equivalence.unitIso = CategoryTheory.NatIso.ofComponents (fun (x : X) => CategoryTheory.eqToIso )
              @[simp]
              theorem OrderIso.equivalence_functor {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
              e.equivalence.functor = .functor
              def OrderIso.equivalence {X : Type u} {Y : Type v} [Preorder X] [Preorder Y] (e : X ≃o Y) :
              X Y

              The equivalence of categories X ≌ Y induced by e : X ≃o Y.

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

                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
                • e.toOrderIso = { toFun := e.functor.obj, invFun := e.inverse.obj, left_inv := , right_inv := , map_rel_iff' := }
                Instances For
                  @[simp]
                  theorem CategoryTheory.Equivalence.toOrderIso_apply {X : Type u} {Y : Type v} [PartialOrder X] [PartialOrder Y] (e : X Y) (x : X) :
                  e.toOrderIso x = e.functor.obj x
                  @[simp]
                  theorem CategoryTheory.Equivalence.toOrderIso_symm_apply {X : Type u} {Y : Type v} [PartialOrder X] [PartialOrder Y] (e : X Y) (y : Y) :
                  e.toOrderIso.symm y = e.inverse.obj y