Could not include topos theory - contents
is the category whose objects are distributive lattices and whose morphisms are lattice homomorphisms, that is functions which preserve finitary meets and joins (equivalently, binary meets and joins and the top and bottom elements). is a subcategory of Pos and a replete subcategory of Lat.
is given by a finitary variety of algebras, or equivalently by a Lawvere theory, so has all the usual properties of such categories. The free distributive lattice on a set is the set of irredundant finite subsets of the finite power set of ; a collection of subsets of is irredundant if, whenever for , we have (that is, no two distinct elements of may be comparable). Note that is the free semilattice on ; we may interpret an element of it as a finitary join of elements of . Then we interpret an element of as a finitary meet of elements of . However, if two of the elements of that appear in this meet are comparable, then we need only the smaller of them, so we take only the irredundant elements of . (We could equally well take joins of meets instead of meets of joins; then we keep only the larger of two meets that appear in a given join.)