nLab
Frm

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 Frm is the category Loc of locales; this is an example of the duality between space and quantity.

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 𝒰𝒫 finX.

(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).

category: category