In mathematics, especially in order theory, a complete Heyting algebra is a Heyting algebra which 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. Euclid, Greek mathematician, 3rd century BC, as imagined by by Raphael in this detail from The School of Athens. ... Order theory is a branch of mathematics that studies various kinds of binary relations that capture the intuitive notion of a mathematical ordering. ... In mathematics, Heyting algebras are special partially ordered sets that constitute a generalization of Boolean algebras. ... In the mathematical area of order theory, completeness properties assert the existence of certain infima or suprema of a given partially ordered set. ... The name lattice is suggested by the form of the Hasse diagram depicting it. ... Category theory is a mathematical theory that deals in an abstract way with mathematical structures and relationships between them. ... In mathematics, categories allow one to formalize notions involving abstract structure and processes which preserve structure. ... In category theory, an abstract branch of mathematics, the dual category or opposite category Cop of a category C is the category formed by reversing all the morphisms of C. That is, we take Cop to be the category with objects that are those of C, but with the morphisms... In mathematics, a morphism is an abstraction of a structure-preserving process between two mathematical structures. ... In abstract algebra, a homomorphism is a structure-preserving map between two algebraic structures (such as groups, rings, or vector spaces). ...

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. Pointless topology is an approach to topology which avoids the mentioning of points. ... In mathematics, general topology or point set topology is that branch of topology which studies elementary properties of topological spaces and structures defined on them. ... In mathematics, general topology or point set topology is that branch of topology which studies elementary properties of topological spaces and structures defined on them. ...

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: In mathematics, especially order theory, a partially ordered set (or poset) is a set equipped with a partial order relation. ... In mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum (join) and an infimum (meet). ...

• P is a Heyting algebra, i.e. the operation ( x - ) has a left adjoint (also called the lower adjoint 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:

• 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 ( x - ) are Scott continuous for all x in P.

In mathematics, adjoint functors are pairs of functors which stand in a particular relationship with one another. ... In mathematics, especially in order theory, a Galois connection is a particular correspondence between two partially ordered sets (posets). Galois connections generalize the correspondence between subgroups and subfields investigated in Galois theory. ... 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. ... In mathematics, a function is Scott-continuous if it is continuous with respect to the Scott topology. ... A monotone function f : P → Q between posets P and Q is Scott-continuous if, for every directed set D that has a supremum sup D in P, the set {fx | x in D} has the supremum f(sup D) in Q. Stated differently, a Scott-continuous function is...

Examples

Complete Heyting algebras arise as the Lindenbaum algebras of (intuitionistic) logics with infinite disjunction. In mathematical logic, the Lindenbaum-Tarski algebra A of a logical theory T consists of the equivalence classes of sentences p of the theory, under the equivalence relation ~ defined by p ~ q when p and q are logically equivalent in T. That is, in T q can be deduced from...

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 morphism. Category theory is a mathematical theory that deals in an abstract way with mathematical structures and relationships between them. ... In mathematics, a morphism is an abstraction of a structure-preserving process between two mathematical structures. ...

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 opposite to those of Frm, and they are usually called maps (of locales). In mathematics, functions between ordered sets are monotonic (or monotone) if they preserve the given order. ... In the mathematical area of order theory, one often speaks about functions that preserve certain limits, i. ... In category theory, an abstract branch of mathematics, the dual of a category C is the category formed by reversing all the morphisms of C. That is, we take Cop to be the category with objects that are those of C, but with the morphisms from X to Y in...

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 algebras, and the map In mathematics, given a set S, the power set (or powerset) of S, written or 2S, is the set of all subsets of S. In axiomatic set theory (as developed e. ... In mathematics, a complete Boolean algebra is a Boolean algebra in which every subset has a supremum. ...

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 f is a continuous function, then Topological spaces are structures that allow one to formalize concepts such as convergence, connectedness and continuity. ... In topology and related fields of mathematics, a set U is called open if, intuitively speaking, you can wiggle or change any point x in U by a small amount in any direction and still be inside U. In other words, if x is surrounded only by elements of U...

preserves finite meets and arbitrary joins of these subframes. This shows that O is a functor from the category Top of topological spaces to the category Loc of locales, taking any continuous map Did somebody just say functor? In category theory, a functor is a special type of mapping between categories. ...

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(f) is defined by the equation O(f) ^* = f ^{− 1}.

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 1 = { * }, 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 p ^* (a) = { * }. 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(f)(q) defined by letting S(f)(p) ^* be the composition of p ^* with f ^* , hence obtaining a continuous map

.

This defines a functor S 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. In 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. ...

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, 1982. (ISBN 0-521-23893-5)

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 0-521-80338-1

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.