Complete Heyting algebra
From Academic Kids

In mathematics, especially in order theory, a complete Heyting algebra is a Heyting algebra which is complete as a lattice. Depending on the exact field of application, complete Heyting algebras also appear under the names locale and frame. Locales and frames are especially important in the mathematical field of pointless topology, which indeed might roughly be described as the study of locales.
This article give various characterizations for the notion of a complete Heyting algebra and explains in which sense the notions of a complete Heyting algebra, a locale and a frame differ, although they describe the same mathematical objects.
Definition
Consider a partially ordered set (P, ≤) that is a complete lattice. Then P is a complete Heyting algebra if any of the following equivalent conditions hold:
 P is a Heyting algebra, i.e. the operations ( x <math>\wedge<math>  ) are the lower adjoints of a (monotone) Galois connection, for each element x of P.
 For all elements x of P and all subsets S of P, the following infinite distributivity law holds:
 <math>x \wedge \bigvee S = \bigvee \{ x \wedge s \mid s \in S \}<math>
 P is a distributive lattice, i.e., for all x, y and z in P, we have
 <math>x \wedge ( y \vee z ) = ( x \wedge y ) \vee ( x \wedge z )<math>
 and P is meet continuous, i.e. the meet operations ( x <math>\wedge<math>  ) are Scott continuous for all x in P.
As already mentioned, structures with this properties are also called frames or locales.
The most prominent examples of locales are the open set lattices (ordered by subset inclusion) of topological spaces. Moreover, complete Heyting algebras arise as the Lindenbaum algebras of (intuitionistic) logics with infinite disjunction.
Differences between the concepts
Complete Heyting algebras, frames, and locales describe entirely the same concept. Yet, subtle differences in the treatment of the three notions arise when considering them in the framework of category theory (or, on a smaller scale, abstract algebra). These differences originate in the way morphisms are defined for the structures.
Frames are usually defined by the infinite distributivity law given above. Hence it is natural that a frame homomorphism is a (necessarily monotone) function that preserves finite meets and arbitrary joins. On the other hand, the definition of Heyting algebras crucially involves the existence of a Galois connection, the upper adjoint of which defines an additional implication operation =>. Thus, a homomorphism of complete Heyting algebras is a morphism of frames that in addition preserves implication.
Finally, locales usually arise in the context of Stone duality and from the viewpoint of pointless topology it is desirable to obtain a category that covariantly corresponds to the category of topological spaces and continuous mappings. Any continuous mapping from a topological space X to another space Y induces a frame homomorphism between the respective lattices of open sets, which goes in the opposite direction. To obtain a covariant relationship, one has to define a morphism from a locale L to a locale M to be given by a frame homomorphism from M to L: the category of locales is dual to the category of frames. Alternatively one may associate locale morphisms with concrete functions by observing that any function that preserves all joins (and hence any frame homomorphism) is the lower adjoint of a Galois connection. Thus locale morphism can be defined as those upper adjoints of a Galois connection between frames, the (uniquely determined) lower adjoints of which preserve binary meets. Being an upper adjoint between complete lattices, these functions necessarily preserve all meets.
Usually the different names for complete Heyting algebras are employed to distinguish these three notions of a morphism implicitly. Naturally the different morphisms have a wide effect on many other concepts. For example a sublocale is something different than a subframe or a subobject of a complete Heyting algebra. The same holds true for free objects in the respective categories.
Literature
 P. T. Johnstone, Stone Spaces, Cambridge Studies in Advanced Mathematics 3, Cambridge University Press, Cambridge, 1982. (ISBN 0521238935)
 Still a great resource on locales and complete Heyting algebras.
 G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003. ISBN 0521803381
 Includes the characterization in terms of meet continuity.
 Francis Borceux: Handbook of Categorical Algebra III, volume 52 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, 1994.
 Surprisingly extensive resource on locales and Heyting algebras. Takes a more categorical viewpoint.