The quasipoint Stone spectrum of a Heyting algebra is compact

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.heyting_stone_compact

by Mrnaiq · Nov 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

compactnesslattice-theoryquantum-logicstone-duality

Let $L$ be a Heyting algebra, and let $Q(L)$ consist of its maximal proper nonempty directed filter bases. Give $Q(L)$ the topology generated by the membership sets $Q_a=\{B:a\in B\}$ . Then

Q(L)\text{ is compact}.

This uniform compactness lemma applies to Boolean algebras and to lattices of open subsets of arbitrary topological spaces. It provides a common foundation for Stone representation and the compactness of open-set Stone spectra.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20
open Set TopologicalSpace
open scoped Topology

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20
theorem heyting_stone_compact {L : Type*} [HeytingAlgebra L] :
    CompactSpace (StoneSpectrum L) := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20

Source

Supporting generalization formalized here for H. F. de Groote, Observables I: Stone Spectra, arXiv:math-ph/0509020v1, https://arxiv.org/pdf/math-ph/0509020v1: Stone compactness recalled in Section 3.1, printed p.38, and Corollary 3.4, printed p.55 (PDF p.56). The source states the Boolean and open-lattice instances; this lemma unifies them for Heyting algebras using the ultrafilter compactness criterion.

View graph