Complete Heyting algebra

In mathematics, especially in order theory, a complete Heyting algebra is a Heyting algebra that is complete as a lattice. Complete Heyting algebras are the objects of three different categories; the category CHey, the category Loc of locales, and its opposite, the category Frm of frames. Although these three categories contain the same objects, they differ in their morphisms, and thus get distinct names. Only the morphisms of CHey are homomorphisms of complete Heyting algebras.
Locales and frames form the foundation of pointless topology, which, instead of building on point-set topology, recasts the ideas of general topology in categorical terms, as statements on frames and locales.
Definition.
Consider a partially ordered set ("P", ≤) that is a complete lattice. Then "P" is a complete Heyting algebra or frame if any of the following equivalent conditions hold:
The entailed definition of Heyting implication is formula_5
Using a bit more category theory, we can equivalently define a frame to be a cocomplete cartesian closed poset.
Examples.
The system of all open sets of a given topological space ordered by inclusion is a complete Heyting algebra.
Frames and locales.
The objects of the category CHey, the category Frm of frames and the category Loc of locales are complete Heyting algebras. These categories differ in what constitutes a morphism:
The relation of locales and their maps to topological spaces and continuous functions may be seen as follows. Let formula_6 be any map. The power sets "P"("X") and "P"("Y") are complete Boolean algebras, and the map formula_7 is a homomorphism of complete Boolean algebras. Suppose the spaces "X" and "Y" are topological spaces, endowed with the topology "O"("X") and "O"("Y") of open sets on "X" and "Y". Note that "O"("X") and "O"("Y") are subframes of "P"("X") and "P"("Y"). If formula_8 is a continuous function, then formula_9
preserves finite meets and arbitrary joins of these subframes. This shows that "O" is a functor from the category Top of topological spaces to Loc, taking any continuous map
to the map
in Loc that is defined in Frm to be the inverse image frame homomorphism
Given a map of locales formula_13 in Loc, it is common to write formula_14 for the frame homomorphism that defines it in Frm. Using this notation, formula_15 is defined by the equation formula_16
Conversely, any locale "A" has a topological space "S"("A"), called its "spectrum", that best approximates the locale. In addition, any map of locales formula_13 determines a continuous map formula_18 Moreover this assignment is functorial: letting "P"(1) denote the locale that is obtained as the power set of the terminal set formula_19 the points of "S"("A") are the maps formula_20 in Loc, i.e., the frame homomorphisms formula_21
For each formula_22 we define formula_23 as the set of points formula_24 such that formula_25 It is easy to verify that this defines a frame homomorphism formula_26 whose image is therefore a topology on "S"("A"). Then, if formula_13 is a map of locales, to each point formula_24 we assign the point formula_29 defined by letting formula_30 be the composition of formula_31 with formula_32 hence obtaining a continuous map formula_33 This defines a functor formula_34 from Loc to Top, which is right adjoint to "O".
Any locale that is isomorphic to the topology of its spectrum is called "spatial", and any topological space that is homeomorphic to the spectrum of its locale of open sets is called "sober". The adjunction between topological spaces and locales restricts to an equivalence of categories between sober spaces and spatial locales.
Any function that preserves all joins (and hence any frame homomorphism) has a right adjoint, and, conversely, any function that preserves all meets has a left adjoint. Hence, the category Loc is isomorphic to the category whose objects are the frames and whose morphisms are the meet preserving functions whose left adjoints preserve finite meets. This is often regarded as a representation of Loc, but it should not be confused with Loc itself, whose morphisms are formally the same as frame homomorphisms in the opposite direction.