Heyting algebra

A Heyting algebra is a bounded distributive lattice with an implication $a\Rightarrow b$ characterized by $x\le (a\Rightarrow b)$ exactly when $x\wedge a\le b$.

In a Heyting algebra, $a\to b$ is the greatest $x$ with $x\wedge a\le b$. Thus $x\le a\to b$ if and only if $x\wedge a\le b$. Every frame has this operation, obtained by taking the join of all such $x$. The open nucleus attached to $a$ is $x\mapsto a\to x$.

The pseudocomplement of $a$ is the greatest element disjoint from $a$. It need not satisfy $a\vee \neg a=1$. In a frame, double pseudocomplementation defines the Booleanization of a locale; its fixed elements are regular open elements.

Meets of subsheaves are pointwise intersections. Joins are J-closures of pointwise unions: a section lies in the join when its restrictions locally belong to some member, with the member allowed to vary. Implication consists of sections every restriction of which belongs to $D$ whenever it belongs to $A$; this gives $C\le (A\Rightarrow D)$ exactly when $C\cap A\le D$. Negation is implication into the initial subobject. Empty covers mean that the initial sheaf need not be pointwise empty.

An element $a$ of a Heyting algebra is regular when $\neg \neg a=a$. The regular elements form its Booleanization.

In a Heyting algebra, meet with a fixed element is left adjoint to Heyting implication, so it preserves joins:The dual distributive law follows from this one by the lattice absorption laws.