Complete Heyting algebra

Last updated

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.


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:

and the meet operations are Scott continuous (i.e., preserve the suprema of directed sets) for all x in P.

The entailed definition of Heyting implication is

Using a bit more category theory, we can equivalently define a frame to be a cocomplete cartesian closed poset.


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 be any map. The power sets P(X) and P(Y) are complete Boolean algebras, and the map 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 is a continuous function, then 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 in Loc, it is common to write for the frame homomorphism that defines it in Frm. Using this notation, is defined by the equation

Conversely, any locale A has a topological space S(A), called its spectrum, that best approximates the locale. In addition, any map of locales determines a continuous map Moreover this assignment is functorial: letting P(1) denote the locale that is obtained as the power set of the terminal set the points of S(A) are the maps in Loc, i.e., the frame homomorphisms

For each we define as the set of 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 defined by letting be the composition of 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 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.


Still a great resource on locales and complete Heyting algebras.
Includes the characterization in terms of meet continuity.
Surprisingly extensive resource on locales and Heyting algebras. Takes a more categorical viewpoint.

Related Research Articles

In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects are associated to topological spaces, and maps between these algebraic objects are associated to continuous maps between spaces. Nowadays, functors are used throughout modern mathematics to relate various categories. Thus, functors are important in all areas within mathematics to which category theory is applied.

In category theory, a branch of mathematics, a Grothendieck topology is a structure on a category C that makes the objects of C act like the open sets of a topological space. A category together with a choice of Grothendieck topology is called a site.

In mathematics, pointless topology is an approach to topology that avoids mentioning points.

In algebra and algebraic geometry, the spectrum of a commutative ring R, denoted by , is the set of all prime ideals of R. It is commonly augmented with the Zariski topology and with a structure sheaf, turning it into a locally ringed space. A locally ringed space of this form is called an affine scheme.

In mathematics, a complete lattice is a partially ordered set in which all subsets have both a supremum (join) and an infimum (meet). Specifically, every non-empty finite lattice is complete. Complete lattices appear in many applications in mathematics and computer science. Being a special instance of lattices, they are studied both in order theory and universal algebra.

In mathematics, specifically category theory, adjunction is a relationship that two functors may have. Two functors that stand in this relationship are known as adjoint functors, one being the left adjoint and the other the right adjoint. Pairs of adjoint functors are ubiquitous in mathematics and often arise from constructions of "optimal solutions" to certain problems, such as the construction of a free group on a set in algebra, or the construction of the Stone–Čech compactification of a topological space in topology.

Homological algebra

Homological algebra is the branch of mathematics that studies homology in a general algebraic setting. It is a relatively young discipline, whose origins can be traced to investigations in combinatorial topology and abstract algebra at the end of the 19th century, chiefly by Henri Poincaré and David Hilbert.

In mathematics, especially in order theory, a Galois connection is a particular correspondence (typically) between two partially ordered sets (posets). 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 between subgroups and subfields investigated in Galois theory. They find applications in various mathematical theories.

In category theory, a category is Cartesian closed if, roughly speaking, any morphism defined on a product of two objects can be naturally identified with a morphism defined on one of the factors. These categories are particularly important in mathematical logic and the theory of programming, in that their internal language is the simply typed lambda calculus. They are generalized by closed monoidal categories, whose internal language, linear type systems, are suitable for both quantum and classical computation.

In mathematics, a Heyting algebra is a bounded lattice equipped with a binary operation ab of implication such that ≤ b is equivalent to c ≤. From a logical standpoint, AB is by this definition the weakest proposition for which modus ponens, the inference rule AB, AB, is sound. Like Boolean algebras, Heyting algebras form a variety axiomatizable with finitely many equations. Heyting algebras were introduced by Arend Heyting (1930) to formalize intuitionistic logic.

In mathematics, the Gelfand representation in functional analysis has two related meanings:

In mathematics, there is an ample supply of categorical dualities between certain categories of topological spaces and categories of partially ordered sets. Today, these dualities are usually collected under the label Stone duality, since they form a natural generalization of Stone's representation theorem for Boolean algebras. These concepts are named in honor of Marshall Stone. Stone-type dualities also provide the foundation for pointless topology and are exploited in theoretical computer science for the study of formal semantics.

In algebraic topology, a branch of mathematics, singular homology refers to the study of a certain set of algebraic invariants of a topological space X, the so-called homology groups Intuitively, singular homology counts, for each dimension n, the n-dimensional holes of a space. Singular homology is a particular example of a homology theory, which has now grown to be a rather broad collection of theories. Of the various theories, it is perhaps one of the simpler ones to understand, being built on fairly concrete constructions.

In mathematics, the category of topological spaces, often denoted Top, is the category whose objects are topological spaces and whose morphisms are continuous maps. This is a category because the composition of two continuous maps is again continuous, and the identity function is continuous. The study of Top and of properties of topological spaces using the techniques of category theory is known as categorical topology.

In category theory, a branch of mathematics, a pushout is the colimit of a diagram consisting of two morphisms f : ZX and g : ZY with a common domain. The pushout consists of an object P along with two morphisms XP and YP that complete a commutative square with the two given morphisms f and g. In fact, the defining universal property of the pushout essentially says that the pushout is the "most general" way to complete this commutative square. Common notations for the pushout are and .

In abstract algebra, an interior algebra is a certain type of algebraic structure that encodes the idea of the topological interior of a set. Interior algebras are to topology and the modal logic S4 what Boolean algebras are to set theory and ordinary propositional logic. Interior algebras form a variety of modal algebras.

In mathematics, a field of sets is a mathematical structure consisting of a pair where is a set and is a family of subsets of called an algebra over that contains the empty set as an element, and is closed under the operations of taking complements in finite unions, and finite intersections. Equivalently, an algebra over is a subset of the power set of such that

  1. for all
  2. , and
  3. for all

In mathematics, the homotopy category is a category built from the category of topological spaces which in a sense identifies two spaces that have the same shape. The phrase is in fact used for two different categories, as discussed below.

In mathematics, specifically in category theory, an exponential object or map object is the categorical generalization of a function space in set theory. Categories with all finite products and exponential objects are called cartesian closed categories. Categories without adjoined products may still have an exponential law.

In mathematics, especially in the area of topology known as algebraic topology, an induced homomorphism is a homomorphism derived in a canonical way from another map. For example, a continuous map from a topological space X to a space Y induces a group homomorphism from the fundamental group of X to the fundamental group of Y.