# mathlibdocumentation

category_theory.limits.lattice

# Limits in lattice categories are given by infimums and supremums. #

def category_theory.limits.complete_lattice.finite_limit_cone {α : Type u} {J : Type w} [order_top α] (F : J α) :

The limit cone over any functor from a finite diagram into a semilattice_inf with order_top.

Equations
def category_theory.limits.complete_lattice.finite_colimit_cocone {α : Type u} {J : Type w} [order_bot α] (F : J α) :

The colimit cocone over any functor from a finite diagram into a semilattice_sup with order_bot.

Equations
@[protected, instance]
@[protected, instance]
theorem category_theory.limits.complete_lattice.finite_limit_eq_finset_univ_inf {α : Type u} {J : Type w} [order_top α] (F : J α) :

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

theorem category_theory.limits.complete_lattice.finite_colimit_eq_finset_univ_sup {α : Type u} {J : Type w} [order_bot α] (F : J α) :

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

theorem category_theory.limits.complete_lattice.finite_product_eq_finset_inf {α : Type u} [order_top α] {ι : Type u} [fintype ι] (f : ι → α) :
( f) = .inf f

A finite product in the category of a semilattice_inf with order_top is the same as the infimum.

theorem category_theory.limits.complete_lattice.finite_coproduct_eq_finset_sup {α : Type u} [order_bot α] {ι : Type u} [fintype ι] (f : ι → α) :
( f) = .sup f

A finite coproduct in the category of a semilattice_sup with order_bot is the same as the supremum.

@[protected, instance]
@[simp]
theorem category_theory.limits.complete_lattice.prod_eq_inf {α : Type u} [order_top α] (x y : α) :
(x y) = x y

The binary product in the category of a semilattice_inf with order_top is the same as the infimum.

@[protected, instance]
@[simp]
theorem category_theory.limits.complete_lattice.coprod_eq_sup {α : Type u} [order_bot α] (x y : α) :
(x ⨿ y) = x y

The binary coproduct in the category of a semilattice_sup with order_bot is the same as the supremum.

@[simp]
theorem category_theory.limits.complete_lattice.pullback_eq_inf {α : Type u} [order_top α] {x y z : α} (f : x z) (g : y z) :

The pullback in the category of a semilattice_inf with order_top is the same as the infimum over the objects.

@[simp]
theorem category_theory.limits.complete_lattice.pushout_eq_sup {α : Type u} [order_bot α] (x y z : α) (f : z x) (g : z y) :
= x y

The pushout in the category of a semilattice_sup with order_bot is the same as the supremum over the objects.

def category_theory.limits.complete_lattice.limit_cone {α : Type u} {J : Type u} (F : J α) :

The limit cone over any functor into a complete lattice.

Equations
def category_theory.limits.complete_lattice.colimit_cocone {α : Type u} {J : Type u} (F : J α) :

The colimit cocone over any functor into a complete lattice.

Equations
@[protected, instance]
@[protected, instance]
theorem category_theory.limits.complete_lattice.limit_eq_infi {α : Type u} {J : Type u} (F : J α) :

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

theorem category_theory.limits.complete_lattice.colimit_eq_supr {α : Type u} {J : Type u} (F : J α) :

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