nLab Frm

Defintion

$Frm$ is the category whose objects are frames and whose morphisms are frame homomorphisms, that is lattice homomorphisms that preserve directed joins (and thus all joins). $Frm$ is a subcategory of Pos, in fact a replete subcategory of both DistLat and SupLat.

The opposite category of $\mathbf{Frm}$ is the category Loc of locales; this is an example of the duality between space and quantity.

Properties

The category $\mathbf{Frm}$ is algebraic (see Stone Spaces).

Free frames

$Frm$ 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. Nevertheless, it is a monadic category (over Set), because it has free objects. Specifically, the free frame on a set $X$ is the lattice of upper subsets of the free join-semilattice on $X$, that is $\mathcal{U}\mathcal{P}_{fin}X$.

(This construction is constructively valid, but it does not go through in predicative mathematics, where infinite frames are generally large objects.)

Note that free frames are quite different from free locales (which are discrete spaces from a localic perspective).

Related concepts

• geometric category

• geometric hyperdoctrine

• Pos, DistLat

category: category