complete Heyting algebra

A Heyting algebra that is also a complete lattice is called a complete Heyting algebra. In the following, we give a lattice characterization of complete Heyting algebras without the relative pseudocomplementation operator $\to$.

Proposition 1.

Let $H$ be a complete Heyting algebra, then

$$x\to y=\bigvee \{z\mid z\wedge x\le y\}$$

for any $x\mathrm{,}y\mathrm{\in }H$, and

$$x\wedge \bigvee A=\bigvee (x\wedge A),$$

where $x\mathrm{\wedge }A\mathrm{:=}\mathrm{\{}x\mathrm{\wedge }y\mathrm{\mid }y\mathrm{\in }A\mathrm{\}}$, for any $x\mathrm{\in }H$, and any subset $A$ of $H$.

Proof.

We first prove the identity $x\wedge \bigvee A=\bigvee (x\wedge A)$. For any $y\in H$, we have $x\wedge \bigvee A\le y$ iff $\bigvee A\le x\to y$ iff $a\le x\to y$ for all $a\in A$ iff $x\wedge a\le y$ for all $a\in A$ iff $\bigvee (x\wedge A)\le y$, hence $x\wedge \bigvee A=\bigvee (x\wedge A)$.

Next, we show $x\to y=\bigvee \{z\mid z\wedge x\le y\}$. For any $a\in H$, we have $a\le x\to y$ iff $a\wedge x\le y$ iff $a\in \{z\mid z\wedge x\le y\}$ iff $a\le \bigvee \{z\mid z\wedge x\le y\}$. ∎

The converse of the above is also true.

Proposition 2.

Let $H$ be a complete lattice such that

$$x\wedge \bigvee A=\bigvee (x\wedge A),$$

where $x\mathrm{\wedge }A\mathrm{:=}\mathrm{\{}x\mathrm{\wedge }y\mathrm{\mid }y\mathrm{\in }A\mathrm{\}}$, for any $x\mathrm{\in }H$, and any subset $A$ of $H$. Then for any $x\mathrm{,}y\mathrm{\in }H$, defining

$$x\to y:=\bigvee \{z\mid z\wedge x\le y\}$$

turns $H$ into a complete Heyting algebra.

Proof.

We want to show that $a\le x\to y$ iff $a\wedge x\le y$ for any $a\in H$: $a\le x\to y$ iff $a\le \bigvee \{z\mid z\wedge x\le y\}$. So $x\wedge a\le x\wedge \bigvee \{z\mid z\wedge x\le y\}=\bigvee \{x\wedge z\mid z\wedge x\le y\}\le \bigvee \{y\}=y$ ∎

From this, one readily concludes that any finite distributive lattice is Heyting.

Remark. Since any complete lattice is bounded, a complete Brouwerian lattice is a complete Heyting algebra. A complete Heyting algebra is also called a frame.

Title	complete Heyting algebra
Canonical name	CompleteHeytingAlgebra
Date of creation	2013-03-22 19:31:42
Last modified on	2013-03-22 19:31:42
Owner	CWoo (3771)
Last modified by	CWoo (3771)
Numerical id	10
Author	CWoo (3771)
Entry type	Definition
Classification	msc 03G10
Classification	msc 06D20
Related topic	Locale