Documentation

Mathlib.CategoryTheory.Limits.Preorder

(Co)limits in a preorder category #

We provide basic results about the nullary and binary (co)products in the associated category of a preordered type.

source
def Preorder.isInitialBot (C : Type u) [Preorder C] [OrderBot C] :
CategoryTheory.Limits.IsInitial ⊥

The least element in a preordered type is initial in the category associated to this preorder.

Equations
    Instances For
      source
      instance Preorder.instHasInitial (C : Type u) [Preorder C] [OrderBot C] :
      CategoryTheory.Limits.HasInitial C
      source
      def Preorder.isTerminalTop (C : Type u) [Preorder C] [OrderTop C] :
      CategoryTheory.Limits.IsTerminal ⊤

      The greatest element of a preordered type is terminal in the category associated to this preorder.

      Equations
        Instances For
          source
          instance Preorder.instHasTerminal (C : Type u) [Preorder C] [OrderTop C] :
          CategoryTheory.Limits.HasTerminal C
          source
          def Preorder.isLimitBinaryFan {C : Type u} [SemilatticeInf C] (X Y : C) :
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯))

          The infimum of two elements in a preordered type is a binary product in the category associated to this preorder.

          Equations
            Instances For
              source
              def Preorder.isColimitBinaryCofan {C : Type u} [SemilatticeSup C] (X Y : C) :
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯))

              The supremum of two elements in a preordered type is a binary coproduct in the category associated to this preorder.

              Equations
                Instances For