mathlib documentation

category_theory.limits.lattice

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

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.

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.

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

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

@[simp]
theorem category_theory.limits.complete_lattice.prod_eq_inf {α : Type u} [semilattice_inf α] [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.

@[simp]
theorem category_theory.limits.complete_lattice.coprod_eq_sup {α : Type u} [semilattice_sup α] [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]

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

@[simp]

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

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

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