nLab
CompLat

CompLatComp Lat is the category whose objects are complete lattices and whose morphisms are complete lattice homomorphisms, that is functions which preserve all joins and meets (including the bottom and top elements). CompLatComp Lat is a subcategory of Pos.

CompLatComp Lat is given by a variety of algebras, or equivalently by an algebraic theory, so it is an equationally presented category; however, it requires operations of arbitrarily large arity. In fact, it is not a monadic category (over Set), because it lacks some free objects. Specifically, the free complete lattice on a set XX, while it exists (by general abstract nonsense) as a class, is small only if XX has at most 22 elements (in which case it is finite and equals the free lattice on XX).

In weak foundations

For all practical purposes, CompLatComp Lat is not available in predicative mathematics. The definition goes through, but we cannot prove that CompLatComp Lat has any infinite objects. (More precisely, the power class of a nontrivial small complete lattice must also be small.) Generally speaking, predicative mathematics treats infinite complete lattices only as large objects.

In impredicative constructive mathematics, it no longer holds that the free complete lattice on a set with at most 22 elements equals the free lattice on that set. In particular, the free complete lattice on the empty set is the set of truth values, while the free lattice on the empty set is the set {,}\{\bot, \top\} of decidable truth values. (I'm not sure whether the free complete lattice on 11 or 22 elements is even small.)

In predicative constructive mathematics, even the free complete lattice on the empty set is a proper class.

category: category

Revised on August 3, 2010 03:54:24 by Toby Bartels (75.88.74.149)