Limits in lattice categories are given by infimums and supremums.

def CategoryTheory.Limits.CompleteLattice.finiteLimitCone {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeInf α] [OrderTop α] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.LimitCone F

The limit cone over any functor from a finite diagram into a SemilatticeInf with OrderTop.

Equations

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

def CategoryTheory.Limits.CompleteLattice.finiteColimitCocone {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeSup α] [OrderBot α] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.ColimitCocone F

The colimit cocone over any functor from a finite diagram into a SemilatticeSup with OrderBot.

Equations

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

@[instance 100]

instance CategoryTheory.Limits.CompleteLattice.hasFiniteLimits_of_semilatticeInf_orderTop {α : Type u} [SemilatticeInf α] [OrderTop α] : CategoryTheory.Limits.HasFiniteLimits α

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.CompleteLattice.hasFiniteColimits_of_semilatticeSup_orderBot {α : Type u} [SemilatticeSup α] [OrderBot α] : CategoryTheory.Limits.HasFiniteColimits α

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeInf α] [OrderTop α] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.limit F = Finset.univ.inf F.obj

The limit of a functor from a finite diagram into a SemilatticeInf with OrderTop is the infimum of the objects in the image.

theorem CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup {α : Type u} {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J] [SemilatticeSup α] [OrderBot α] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.colimit F = Finset.univ.sup F.obj

The colimit of a functor from a finite diagram into a SemilatticeSup with OrderBot is the supremum of the objects in the image.

theorem CategoryTheory.Limits.CompleteLattice.finite_product_eq_finset_inf {α : Type u} [SemilatticeInf α] [OrderTop α] {ι : Type u} [Fintype ι] (f : ι → α) : ∏ᶜ f = Fintype.elems.inf f

A finite product in the category of a SemilatticeInf with OrderTop is the same as the infimum.

theorem CategoryTheory.Limits.CompleteLattice.finite_coproduct_eq_finset_sup {α : Type u} [SemilatticeSup α] [OrderBot α] {ι : Type u} [Fintype ι] (f : ι → α) : ∐ f = Fintype.elems.sup f

A finite coproduct in the category of a SemilatticeSup with OrderBot is the same as the supremum.

@[instance 100]

instance CategoryTheory.Limits.CompleteLattice.instHasBinaryProductsOfOrderTop {α : Type u} [SemilatticeInf α] [OrderTop α] : CategoryTheory.Limits.HasBinaryProducts α

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Limits.CompleteLattice.prod_eq_inf {α : Type u} [SemilatticeInf α] [OrderTop α] (x y : α) : (x ⨯ y) = x ⊓ y

The binary product in the category of a SemilatticeInf with OrderTop is the same as the infimum.

@[instance 100]

instance CategoryTheory.Limits.CompleteLattice.instHasBinaryCoproductsOfOrderBot {α : Type u} [SemilatticeSup α] [OrderBot α] : CategoryTheory.Limits.HasBinaryCoproducts α

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Limits.CompleteLattice.coprod_eq_sup {α : Type u} [SemilatticeSup α] [OrderBot α] (x y : α) : (x ⨿ y) = x ⊔ y

The binary coproduct in the category of a SemilatticeSup with OrderBot is the same as the supremum.

@[simp]

theorem CategoryTheory.Limits.CompleteLattice.pullback_eq_inf {α : Type u} [SemilatticeInf α] [OrderTop α] {x y z : α} (f : x ⟶ z) (g : y ⟶ z) : CategoryTheory.Limits.pullback f g = x ⊓ y

The pullback in the category of a SemilatticeInf with OrderTop is the same as the infimum over the objects.

@[simp]

theorem CategoryTheory.Limits.CompleteLattice.pushout_eq_sup {α : Type u} [SemilatticeSup α] [OrderBot α] (x y z : α) (f : z ⟶ x) (g : z ⟶ y) : CategoryTheory.Limits.pushout f g = x ⊔ y

The pushout in the category of a SemilatticeSup with OrderBot is the same as the supremum over the objects.

def CategoryTheory.Limits.CompleteLattice.limitCone {α : Type u} [CompleteLattice α] {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.LimitCone F

The limit cone over any functor into a complete lattice.

Equations

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

def CategoryTheory.Limits.CompleteLattice.colimitCocone {α : Type u} [CompleteLattice α] {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.ColimitCocone F

The colimit cocone over any functor into a complete lattice.

Equations

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

@[instance 100]

instance CategoryTheory.Limits.CompleteLattice.hasLimits_of_completeLattice {α : Type u} [CompleteLattice α] : CategoryTheory.Limits.HasLimits α

Equations

• ⋯ = ⋯

@[instance 100]

instance CategoryTheory.Limits.CompleteLattice.hasColimits_of_completeLattice {α : Type u} [CompleteLattice α] : CategoryTheory.Limits.HasColimits α

Equations

• ⋯ = ⋯

theorem CategoryTheory.Limits.CompleteLattice.limit_eq_iInf {α : Type u} [CompleteLattice α] {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.limit F = iInf F.obj

The limit of a functor into a complete lattice is the infimum of the objects in the image.

theorem CategoryTheory.Limits.CompleteLattice.colimit_eq_iSup {α : Type u} [CompleteLattice α] {J : Type u} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J α) : CategoryTheory.Limits.colimit F = iSup F.obj

The colimit of a functor into a complete lattice is the supremum of the objects in the image.