(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.

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

• Preorder.isInitialBot C = CategoryTheory.Limits.IsInitial.ofUnique ⊥

instance Preorder.instHasInitial (C : Type u) [Preorder C] [OrderBot C] : CategoryTheory.Limits.HasInitial C

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

• Preorder.isTerminalTop C = CategoryTheory.Limits.IsTerminal.ofUnique ⊤

instance Preorder.instHasTerminal (C : Type u) [Preorder C] [OrderTop C] : CategoryTheory.Limits.HasTerminal C

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

• Preorder.isLimitBinaryFan X Y = CategoryTheory.Limits.BinaryFan.isLimitMk (fun (s : CategoryTheory.Limits.BinaryFan X Y) => CategoryTheory.homOfLE ⋯) ⋯ ⋯ ⋯

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

• Preorder.isColimitBinaryCofan X Y = CategoryTheory.Limits.BinaryCofan.isColimitMk (fun (s : CategoryTheory.Limits.BinaryCofan X Y) => CategoryTheory.homOfLE ⋯) ⋯ ⋯ ⋯