In
mathematicsMathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
, especially in
order theoryOrder theory is a branch of mathematics which investigates our intuitive notion of order using binary relations. It provides a formal framework for describing statements such as "this is less than that" or "this precedes that". This article introduces the field and gives some basic definitions...
, a
complete Heyting algebra is a
Heyting algebraIn mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...
which is
completeIn the mathematical area of order theory, completeness properties assert the existence of certain infima or suprema of a given partially ordered set . A special use of the term refers to complete partial orders or complete lattices...
as a
latticeIn mathematics, a lattice is a partially ordered set in which any two elements have a unique supremum and an infimum . Lattices can also be characterized as algebraic structures satisfying certain axiomatic identities...
. 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
morphismIn mathematics, a morphism is an abstraction derived from structurepreserving mappings between two mathematical structures. The notion of morphism recurs in much of contemporary mathematics...
s, and thus get distinct names. Only the morphisms of
CHey are
homomorphismIn abstract algebra, a homomorphism is a structurepreserving map between two algebraic structures . The word homomorphism comes from the Greek language: ὁμός meaning "same" and μορφή meaning "shape". Definition :The definition of homomorphism depends on the type of algebraic structure under...
s of complete Heyting algebras.
Locales and frames form the foundation of
pointless topologyIn mathematics, pointless topology is an approach to topology that avoids mentioning points. The name 'pointless topology' is due to John von Neumann...
, which, instead of building on pointset topology, recasts the ideas of
general topologyIn mathematics, general topology or pointset topology is the branch of topology which studies properties of topological spaces and structures defined on them...
in categorical terms, as statements on frames and locales.
Definition
Consider a
partially ordered setIn mathematics, especially order theory, a partially ordered set formalizes and generalizes the intuitive concept of an ordering, sequencing, or arrangement of the elements of a set. A poset consists of a set together with a binary relation that indicates that, for certain pairs of elements in the...
(
P, ≤) that is a
complete latticeIn mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum and an infimum . Complete lattices appear in many applications in mathematics and computer science...
. Then
P is a
complete Heyting algebra if any of the following equivalent conditions hold:
 P is a Heyting algebra, i.e. the operation has a right adjoint
In mathematics, adjoint functors are pairs of functors which stand in a particular relationship with one another, called an adjunction. The relationship of adjunction is ubiquitous in mathematics, as it rigorously reflects the intuitive notions of optimization and efficiency...
(also called the lower adjoint of a (monotone) Galois connectionIn mathematics, especially in order theory, a Galois connection is a particular correspondence between two partially ordered sets . The same notion can also be defined on preordered sets or classes; this article presents the common case of posets. Galois connections generalize the correspondence...
), for each element x of P.
 For all elements x of P and all subsets S of P, the following infinite distributivity
In the mathematical area of order theory, there are various notions of the common concept of distributivity, applied to the formation of suprema and infima...
law holds:

 P is a distributive lattice, i.e., for all x, y and z in P, we have

 and P is meet continuous, i.e. the meet operations are Scott continuous for all x in P.
Examples
The system of all open sets of a given
topological spaceTopological spaces are mathematical structures that allow the formal definition of concepts such as convergence, connectedness, and continuity. They appear in virtually every branch of modern mathematics and are a central unifying notion...
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 the complete lattices satisfying the infinite distributive law. These categories differ in what constitutes a
morphismIn mathematics, a morphism is an abstraction derived from structurepreserving mappings between two mathematical structures. The notion of morphism recurs in much of contemporary mathematics...
.
The morphisms of
Frm are (necessarily monotone) functions that preserve finite meets and arbitrary joins. Such functions are not homomorphisms of complete Heyting algebras. The definition of Heyting algebras crucially involves the existence of right adjoints to the binary meet operation, which together define an additional implication operation ⇒. Thus, a
homomorphism of complete Heyting algebras is a morphism of frames that in addition preserves implication. The morphisms of
Loc are
oppositeIn category theory, a branch of mathematics, duality is a correspondence between properties of a category C and socalled dual properties of the opposite category Cop...
to those of
Frm, and they are usually called maps (of locales).
The relation of locales and their maps to topological spaces and continuous functions may be seen as follows. Let
be any map. The
power sets
P(
X) and
P(
Y) are
complete Boolean algebraIn mathematics, a complete Boolean algebra is a Boolean algebra in which every subset has a supremum . Complete Boolean algebras are used to construct Booleanvalued models of set theory in the theory of forcing...
s, and the map

is a homomorphism of complete Boolean algebras. Suppose the spaces
X and
Y are
topological spaceTopological spaces are mathematical structures that allow the formal definition of concepts such as convergence, connectedness, and continuity. They appear in virtually every branch of modern mathematics and are a central unifying notion...
s, endowed with the topology
O(
X) and
O(
Y) of
open setThe concept of an open set is fundamental to many areas of mathematics, especially pointset topology and metric topology. Intuitively speaking, a set U is open if any point x in U can be "moved" a small amount in any direction and still be in the set U...
s on
X and
Y. Note that
O(
X) and
O(
Y) are subframes of
P(
X) and
P(
Y). If
ƒ is a continuous function, then

preserves finite meets and arbitrary joins of these subframes. This shows that
O is a
functorIn category theory, a branch of mathematics, a functor is a special type of mapping between categories. Functors can be thought of as homomorphisms between categories, or morphisms when in the category of small categories....
from the category
Top of topological spaces to the category
Loc of locales, taking any continuous map

to the map

in
Loc that is defined in
Frm to be the inverse image frame homomorphism
 .
It is common, given a map of locales

in
Loc, to write

for the frame homomorphism that defines it in
Frm. Hence, using this notation,
O(
ƒ) is defined by the equation
Conversely, any locale
A has a topological space
S(
A) that best approximates the locale, called its
spectrum. In addition, any map of locales

determines a continuous map
 ,
and this assignment is functorial: letting
P(1) denote the locale that is obtained as the powerset of the terminal set the points of
S(
A) are the maps

in
Loc, i.e., the frame homomorphisms
 .
For each we define the set that consists of the points such that It is easy to verify that this defines a frame homomorphism whose image is therefore a topology on
S(
A). Then, if
 is a map of locales,
to each point we assign the point
S(
ƒ)(
q) defined by letting
S(
ƒ)(p)* be the composition of
p* with
ƒ*, hence obtaining a continuous map
 .
This defines a functor
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 categoriesIn category theory, an abstract branch of mathematics, an equivalence of categories is a relation between two categories that establishes that these categories are "essentially the same". There are numerous examples of categorical equivalences from many areas of mathematics...
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.
Literature
 P. T. Johnstone, Stone Spaces, Cambridge Studies in Advanced Mathematics 3, Cambridge University Press
Cambridge University Press is the publishing business of the University of Cambridge. Granted letters patent by Henry VIII in 1534, it is the world's oldest publishing house, and the second largest university press in the world...
, 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.
 Steven Vickers, Topology via logic, Cambridge University Press, 1989, ISBN 0521360625.