(Co)limits in a preorder category

We provide basic results about (co)limits in the associated category of a preordered type.

• We show that a functor F has a (co)limit iff it has a greatest lower bound (least upper bound).
• We show maximal (minimal) elements correspond to terminal (initial) objects.
• We show that (co)products correspond to infima (suprema).

def Preorder.coneOfLowerBound {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ lowerBounds (Set.range F.obj)) : CategoryTheory.Limits.Cone F

The cone associated to a lower bound of a functor.

Equations

• Preorder.coneOfLowerBound F h = { pt := x, π := { app := fun (i : J) => CategoryTheory.homOfLE ⋯, naturality := ⋯ } }

theorem Preorder.conePt_mem_lowerBounds {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) : c.pt ∈ lowerBounds (Set.range F.obj)

The point of a cone is a lower bound.

theorem Preorder.isGLB_of_isLimit {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cone F} (h : CategoryTheory.Limits.IsLimit c) : IsGLB (Set.range F.obj) c.pt

If a cone is a limit, its point is a glb.

def Preorder.isLimitOfIsGLB {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F) (h : IsGLB (Set.range F.obj) c.pt) : CategoryTheory.Limits.IsLimit c

If the point of cone is a glb, the cone is a limi.t

Equations

• Preorder.isLimitOfIsGLB F c h = { lift := fun (d : CategoryTheory.Limits.Cone F) => ⋯.hom, fac := ⋯, uniq := ⋯ }

theorem Preorder.hasLimit_iff_hasGLB {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.HasLimit F ↔ ∃ (x : C), IsGLB (Set.range F.obj) x

A functor has a limit iff there exists a glb.

def Preorder.coconePt_mem_upperBounds {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {x : C} (h : x ∈ upperBounds (Set.range F.obj)) : CategoryTheory.Limits.Cocone F

The cocone associated to an upper bound of a functor

Equations

• Preorder.coconePt_mem_upperBounds F h = { pt := x, ι := { app := fun (i : J) => CategoryTheory.homOfLE ⋯, naturality := ⋯ } }

theorem Preorder.upperBoundOfCocone {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) : c.pt ∈ upperBounds (Set.range F.obj)

The point of a cocone is an upper bound.

theorem Preorder.isLUB_of_isColimit {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {c : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit c) : IsLUB (Set.range F.obj) c.pt

If a cocone is a colimit, its point is a lub.

def Preorder.isColimitOfIsLUB {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cocone F) (h : IsLUB (Set.range F.obj) c.pt) : CategoryTheory.Limits.IsColimit c

If the point of cocone is a lub, the cocone is a .colimit

Equations

• Preorder.isColimitOfIsLUB F c h = { desc := fun (d : CategoryTheory.Limits.Cocone F) => ⋯.hom, fac := ⋯, uniq := ⋯ }

theorem Preorder.hasColimit_iff_hasLUB {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) : CategoryTheory.Limits.HasColimit F ↔ ∃ (x : C), IsLUB (Set.range F.obj) x

A functor has a colimit iff there exists a lub.

def CategoryTheory.Limits.IsTerminal.orderTop {C : Type u} [Preorder C] {X : C} (t : IsTerminal X) : OrderTop C

A terminal object in a preorder C is top element for C.

Equations

• t.orderTop = { top := X, le_top := ⋯ }

noncomputable def Preorder.orderTopOfHasTerminal {C : Type u} [Preorder C] [CategoryTheory.Limits.HasTerminal C] : OrderTop C

A preorder with a terminal object has a greatest element.

Equations

• Preorder.orderTopOfHasTerminal = CategoryTheory.Limits.terminalIsTerminal.orderTop

def Preorder.isTerminalTop (C : Type u) [Preorder C] [OrderTop C] : CategoryTheory.Limits.IsTerminal ⊤

If C is a preorder with top, then ⊤ is a terminal object.

Equations

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

@[instance 100]

instance Preorder.instHasTerminalOfOrderTop {C : Type u} [Preorder C] [OrderTop C] : CategoryTheory.Limits.HasTerminal C

def CategoryTheory.Limits.IsInitial.orderBot {C : Type u} [Preorder C] {X : C} (t : IsInitial X) : OrderBot C

An initial object in a preorder C is bottom element for C.

Equations

• t.orderBot = { bot := X, bot_le := ⋯ }

noncomputable def Preorder.orderBotOfHasInitial {C : Type u} [Preorder C] [CategoryTheory.Limits.HasInitial C] : OrderBot C

A preorder with an initial object has a least element.

Equations

• Preorder.orderBotOfHasInitial = CategoryTheory.Limits.initialIsInitial.orderBot

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

If C is a preorder with bot, then ⊥ is an initial object.

Equations

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

@[instance 100]

instance Preorder.instHasInitialOfOrderBot {C : Type u} [Preorder C] [OrderBot C] : CategoryTheory.Limits.HasInitial C

def Preorder.semilatticeInfOfIsLimitBinaryFan {C : Type u} [PartialOrder C] (c : (X Y : C) → CategoryTheory.Limits.BinaryFan X Y) (h : (X Y : C) → CategoryTheory.Limits.IsLimit (c X Y)) : SemilatticeInf C

A family of limiting binary fans on a partial order induces an inf-semilattice structure on it.

Equations

• Preorder.semilatticeInfOfIsLimitBinaryFan c h = { toPartialOrder := inst✝, inf := fun (X Y : C) => (c X Y).pt, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

noncomputable def Preorder.semilatticeInfOfHasBinaryProducts (C : Type u) [PartialOrder C] [CategoryTheory.Limits.HasBinaryProducts C] : SemilatticeInf C

If a partial order has binary products, then it is a inf-semilattice

Equations

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

def Preorder.semilatticeSupOfIsColimitBinaryCofan {C : Type u} [PartialOrder C] (c : (X Y : C) → CategoryTheory.Limits.BinaryCofan X Y) (h : (X Y : C) → CategoryTheory.Limits.IsColimit (c X Y)) : SemilatticeSup C

A family of colimiting binary cofans on a partial order induces a sup-semilattice structure on it.

Equations

• Preorder.semilatticeSupOfIsColimitBinaryCofan c h = { toPartialOrder := inst✝, sup := fun (X Y : C) => (c X Y).pt, le_sup_left := ⋯, le_sup_right := ⋯, sup_le := ⋯ }

noncomputable def Preorder.semilatticeSupOfHasBinaryCoproducts (C : Type u) [PartialOrder C] [CategoryTheory.Limits.HasBinaryCoproducts C] : SemilatticeSup C

If a partial order has binary coproducts, then it is a sup-semilattice

Equations

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

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 ⋯) ⋯ ⋯ ⋯

@[instance 100]

instance Preorder.instHasBinaryProducts {C : Type u} [SemilatticeInf C] : CategoryTheory.Limits.HasBinaryProducts C

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 ⋯) ⋯ ⋯ ⋯

@[instance 100]

instance Preorder.instHasBinaryCoproducts {C : Type u} [SemilatticeSup C] : CategoryTheory.Limits.HasBinaryCoproducts C