# Documentation

Mathlib.CategoryTheory.Limits.Lattice

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

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

Instances For

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

Instances For
theorem CategoryTheory.Limits.CompleteLattice.finite_limit_eq_finset_univ_inf {α : Type u} {J : Type w} [] [] (F : ) :
= Finset.inf Finset.univ 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} [] [] (F : ) :
= Finset.sup Finset.univ 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} [] [] {ι : Type u} [] (f : ια) :
f = Finset.inf Fintype.elems 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} [] [] {ι : Type u} [] (f : ια) :
f = Finset.sup Fintype.elems f

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

@[simp]
theorem CategoryTheory.Limits.CompleteLattice.prod_eq_inf {α : Type u} [] [] (x : α) (y : α) :
(x y) = x y

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

@[simp]
theorem CategoryTheory.Limits.CompleteLattice.coprod_eq_sup {α : Type u} [] [] (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} [] [] {x : α} {y : α} {z : α} (f : x z) (g : y z) :
= 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} [] [] (x : α) (y : α) (z : α) (f : z x) (g : z y) :
= x y

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

The limit cone over any functor into a complete lattice.

Instances For

The colimit cocone over any functor into a complete lattice.

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

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.