nLab regular element

This entry is about regular elements in formal logic and topology. For regular elements in physics/quantum field theory see at regularization (physics). For regular elements in ring theory and commutative algebra, see cancellative element.

A regular element of a Heyting algebra is an element $x$ such that $\neg{\neg{x}} = x$.

Thus a Boolean algebra is precisely a Heyting algebra in which every element is regular.

As a special case, a regular open in a locale $S$ is a regular element of $S$ as a frame. These define the regular open sublocales of $S$. We may also say regular open subspace for this (or the following concept).

An analogous kind of regular open subspace is a regular open set in a topological space $X$, which is a regular element of the frame of open sets of $X$. Equivalently, this is an open set in $X$ that equals the interior of its closure, or equivalently the exterior of its exterior. (This is the origin of the term, related to a regular space.)

The regularization of $x$ is $\neg{\neg{x}}$; note that this is regular. In fact, any element of the form $\neg{y}$ is regular. Note that $x \leq \neg{\neg{x}}$; in logic, this means that a double negation is a weaker statement.

In a topological space, the regularization of an open set $G$ can be constructed as $Int(Cl(G))$, or equivalently as $Ext(Ext(G))$. Sometimes one performs this operation to an arbitrary set (in the space) to produce a regular open set. But note that while $G \subseteq Int(Cl(G))$ when $G$ is open, this does not hold for an arbitrary set.