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

@[simp]

theorem Preorder.coneOfLowerBound_pt {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)) : (coneOfLowerBound F h).pt = x

@[simp]

theorem Preorder.coneOfLowerBound_π_app {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)) (i : J) : (coneOfLowerBound F h).π.app i = CategoryTheory.homOfLE ⋯

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

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

The limit cone for a functor F : J ⥤ C to a preorder when pt : C is the greatest lower bound of Set.range F.obj

@[simp]

theorem Preorder.limitConeOfIsGLB_isLimit {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsGLB (Set.range F.obj) pt) : (limitConeOfIsGLB F h).isLimit = isLimitOfIsGLB F (coneOfLowerBound F ⋯) h

@[simp]

theorem Preorder.limitConeOfIsGLB_cone {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsGLB (Set.range F.obj) pt) : (limitConeOfIsGLB F h).cone = coneOfLowerBound F ⋯

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.coconeOfUpperBound {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.

@[simp]

theorem Preorder.coconeOfUpperBound_ι_app {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)) (i : J) : (coconeOfUpperBound F h).ι.app i = CategoryTheory.homOfLE ⋯

@[simp]

theorem Preorder.coconeOfUpperBound_pt {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)) : (coconeOfUpperBound F h).pt = x

theorem Preorder.coconePt_mem_upperBounds {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

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

The colimit cocone for a functor F : J ⥤ C to a preorder when pt : C is the least upper bound of Set.range F.obj

@[simp]

theorem Preorder.colimitCoconeOfIsLUB_isColimit {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsLUB (Set.range F.obj) pt) : (colimitCoconeOfIsLUB F h).isColimit = isColimitOfIsLUB F (coconeOfUpperBound F ⋯) h

@[simp]

theorem Preorder.colimitCoconeOfIsLUB_cocone {C : Type u} [Preorder C] {J : Type u'} [CategoryTheory.Category.{v, u'} J] (F : CategoryTheory.Functor J C) {pt : C} (h : IsLUB (Set.range F.obj) pt) : (colimitCoconeOfIsLUB F h).cocone = coconeOfUpperBound F ⋯

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.

@[implicit_reducible]

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.

@[implicit_reducible]

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.

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.

@[instance 100]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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.

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.

@[instance 100]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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 an inf-semilattice

@[implicit_reducible]

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.

@[implicit_reducible]

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

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.

@[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.

@[instance 100]

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