A topos for \'etale-finite Heyting algebras

A longstanding open problem is whether every Heyting algebra is the lattice of truth values (i.e., of subterminal objects) of some elementary topos. A positive answer is known for complete Heyting algebras (i.e., locales) via sheaves, and for Boolean algebras via a construction due to Peter Freyd. We extend Freyd's construction to all \'etale-finite Heyting algebras, in the sense of Evgeny Kuznetsov. These are the Heyting algebras satisfying a generalisation of the law of excluded middle relative to some finite Heyting subalgebra. For every \'etale-finite Heyting algebra H, we use Esakia duality to construct an elementary topos whose lattice of truth values is isomorphic to H, thereby extending the class of Heyting algebras for which a positive answer to the Heyting-to-topos problem is known. The toposes we construct are categories of certain compact \'etale spaces. As a consequence, they are finitely propositional: every object has a finite cover by subterminal objects. We show that a Heyting algebra occurs as the lattice of truth values of some finitely propositional topos if and only if it is \'etale-finite. This exhibits an obstruction to extending the use of compact \'etale spaces beyond the \'etale-finite case.