pith. sign in

arxiv: 2606.03861 · v2 · pith:JTYY6TZ6new · submitted 2026-06-02 · 🧮 math.LO · math.CT

A topos for \'etale-finite Heyting algebras

Marco Abbadini , Rodrigo Nicolau Almeida , Igor Arrieta This is my paper

Pith reviewed 2026-06-29 05:16 UTC · model grok-4.3

classification 🧮 math.LO math.CT
keywords Heyting algebraselementary toposesEsakia dualityétale-finitefinitely propositional toposessubterminal objects
0
0 comments X

The pith

Every étale-finite Heyting algebra arises as the lattice of subterminal objects in an elementary topos.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tackles the open question of which Heyting algebras can appear as the lattice of truth values in an elementary topos. It extends earlier results for Boolean algebras by showing that every étale-finite Heyting algebra can be realized this way. The method relies on Esakia duality to build the topos explicitly as a category of compact étale spaces. It further proves that these algebras are exactly the ones that occur as truth lattices in finitely propositional toposes, where every object admits a finite cover by subterminals. This identifies a clear obstruction to realizing non-étale-finite Heyting algebras inside that restricted class of toposes.

Core claim

For every étale-finite Heyting algebra H, Esakia duality produces an elementary topos of compact étale spaces whose lattice of subterminal objects is isomorphic to H; a Heyting algebra arises as the subterminal lattice of some finitely propositional topos if and only if it is étale-finite.

What carries the argument

Esakia duality applied to étale-finite Heyting algebras, yielding a topos of compact étale spaces whose subterminals recover H.

If this is right

  • Every étale-finite Heyting algebra is the lattice of subterminals in some elementary topos.
  • The constructed toposes are finitely propositional.
  • A Heyting algebra is the subterminal lattice of a finitely propositional topos precisely when it is étale-finite.
  • The construction extends Freyd's earlier method from Boolean algebras to the larger class of étale-finite Heyting algebras.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The characterization isolates the obstruction to realizing arbitrary Heyting algebras inside finitely propositional toposes.
  • Realizing non-étale-finite Heyting algebras would require toposes outside the finitely propositional class.

Load-bearing premise

Esakia duality applied to an étale-finite Heyting algebra produces an elementary topos whose subterminal objects recover exactly that algebra.

What would settle it

An explicit étale-finite Heyting algebra for which no elementary topos of compact étale spaces has subterminals isomorphic to it, or a finitely propositional topos whose subterminal lattice fails to be étale-finite.

Figures

Figures reproduced from arXiv: 2606.03861 by Igor Arrieta, Marco Abbadini, Rodrigo Nicolau Almeida.

Figure 1
Figure 1. Figure 1: The space (αN) ⊤ and its dual Heyting algebra. Let 2 = 0 < 1 be the discrete two-element chain. Consider the map e´: (αN) ⊤ → 2 that sends ⊤ to 1 and every other point to 0. Then e´ is a continuous strict p-morphism. Therefore, (αN) ⊤ is an ´etale-finite Esakia space. (4) More generally, let X be an ´etale-finite Esakia space, say with e´: X → X0 a continuous strict p-morphism, and let Y0 be a finite poset… view at source ↗
Figure 1
Figure 1. Figure 1: The space (αN) ⊤ and its dual Heyting algebra. (4) More generally, let X be an ´etale-finite Esakia space, say with e´: X → X0 a continuous strict p-morphism, and let Y0 be a finite poset. We can consider X ⊕ Y0, whose underlying topological space is the disjoint union X ⊔ Y0 of X and the discrete space Y0, and whose partial order is defined by letting every point of X be below every point of Y0 (see e.g.,… view at source ↗
Figure 2
Figure 2. Figure 2: The space X ⊕ Y0 and its dual Heyting algebra H0 ⊕ H. (5) (Discrete version) Suppose that e´: P → P0 is a strict p-morphism from a poset P to a finite poset P0. We show that the inverse-image function e´ −1 [−]: Up(P0) → Up(P) satisfies Jibladze’s law, and hence that Up(P) is ´etale-finite. First, notice that every point p ∈ P has only finitely many successors, i.e., ↑p is finite. For each upset U ∈ Up(P),… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper claims that for every étale-finite Heyting algebra H (in the sense of Kuznetsov), Esakia duality yields an elementary topos of compact étale spaces whose lattice of subterminal objects is isomorphic to H. It further claims that a Heyting algebra arises as the subobject classifier of some finitely propositional topos if and only if it is étale-finite, thereby characterizing the Heyting algebras realizable in this restricted class of toposes and extending Freyd's Boolean-algebra construction.

Significance. If the central construction is correct, the result enlarges the known class of Heyting algebras that occur as lattices of truth values in an elementary topos and supplies a clean obstruction (étale-finiteness) for the finitely propositional case. The explicit use of Esakia duality to produce the topos and the if-and-only-if characterization are concrete advances over the Boolean and locale cases already in the literature.

major comments (2)
  1. [Construction via Esakia duality (main theorem)] The central claim requires that the category of compact étale spaces obtained from the Esakia dual of an étale-finite H is an elementary topos (finite limits, exponentials, subobject classifier) whose subterminals recover exactly H. The manuscript must exhibit the verification that the étale/compact condition is preserved under the exponential and subobject-classifier constructions; without an explicit check that the resulting category is not merely a pretopos, the extension beyond Freyd's Boolean case remains the least secure step.
  2. [Characterization theorem] The equivalence 'H arises in a finitely propositional topos ⇔ H is étale-finite' rests on showing both directions. The 'only if' direction needs a concrete argument that any finitely propositional topos has an étale-finite subobject classifier; the manuscript should isolate the step where the finite propositional cover forces the relative excluded-middle law with respect to a finite subalgebra.
minor comments (2)
  1. [Introduction] Notation for the étale-finite condition and the relative excluded-middle law should be introduced with a displayed definition before its first use in the main statements.
  2. [Abstract] The abstract states the result for 'every étale-finite Heyting algebra H' but does not indicate whether the construction is functorial in H or merely objectwise; a sentence clarifying this would help readers compare with Freyd's original construction.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and the constructive major comments. The suggestions identify places where the manuscript would benefit from more explicit verification of key preservation properties and a clearer isolation of steps in the characterization proof. We address each point below and will revise the manuscript to incorporate the requested details.

read point-by-point responses

  1. Referee: [Construction via Esakia duality (main theorem)] The central claim requires that the category of compact étale spaces obtained from the Esakia dual of an étale-finite H is an elementary topos (finite limits, exponentials, subobject classifier) whose subterminals recover exactly H. The manuscript must exhibit the verification that the étale/compact condition is preserved under the exponential and subobject-classifier constructions; without an explicit check that the resulting category is not merely a pretopos, the extension beyond Freyd's Boolean case remains the least secure step.

    Authors: We agree that an explicit verification of preservation of the étale and compact conditions is required to establish that the constructed category is an elementary topos. While the manuscript uses Esakia duality to define the category and asserts the topos structure, the preservation arguments for exponentials and the subobject classifier are only sketched. In the revision we will add a dedicated subsection providing the full verification that these constructions preserve compactness and the étale property when H is étale-finite, thereby confirming the category is elementary rather than merely a pretopos. revision: yes

  2. Referee: [Characterization theorem] The equivalence 'H arises in a finitely propositional topos ⇔ H is étale-finite' rests on showing both directions. The 'only if' direction needs a concrete argument that any finitely propositional topos has an étale-finite subobject classifier; the manuscript should isolate the step where the finite propositional cover forces the relative excluded-middle law with respect to a finite subalgebra.

    Authors: The manuscript proves both directions of the characterization, with the 'only if' direction relying on the fact that a finite propositional cover by subterminals induces the relative excluded-middle law. To address the request for greater concreteness, we will revise the proof of the characterization theorem to isolate this step explicitly, showing how the finite cover forces étale-finiteness of the subobject classifier. This will make the obstruction for non-étale-finite algebras more transparent. revision: yes

Circularity Check

0 steps flagged

No circularity: construction relies on external Esakia duality and extension of Freyd's Boolean case

full rationale

The paper's derivation applies the known Esakia duality theorem (external to the authors) to étale-finite Heyting algebras, defined via Kuznetsov's prior independent work, to build the topos of compact étale spaces. The central claim—that this yields an elementary topos with subterminals recovering H exactly, and the iff characterization for finitely propositional toposes—is presented as a new construction extending Freyd's result, without any equations, fitted parameters, or self-citations that reduce the output to the inputs by definition. No load-bearing step collapses to renaming, ansatz smuggling, or self-referential uniqueness theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work relies on background theorems of category theory, topos theory, and Esakia duality; no new free parameters, ad-hoc axioms, or postulated entities are introduced.

axioms (2)
  • domain assumption Esakia duality theorem applies to the étale-finite Heyting algebras under consideration
    Invoked to construct the topos from the algebra via compact étale spaces.
  • standard math Standard axioms of elementary toposes and category theory
    Required to guarantee that the constructed category is an elementary topos.

pith-pipeline@v0.9.1-grok · 5772 in / 1380 out tokens · 35866 ms · 2026-06-29T05:16:21.634816+00:00 · methodology

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

55 extracted references · 11 canonical work pages

  1. [1]

    Jibladze , title=

    M. Jibladze , title=. 2002 , journal=

    2002

  2. [2]

    Caramello , title =

    O. Caramello , title =. Theory and Applications of Categories , volume =

  3. [3]

    and Reyes, G

    Kock, A. and Reyes, G. E. , title =. Cahiers de Topologie et G\'eom\'etrie Diff\'erentielle Cat\'egoriques , pages =. 1994 , publisher =

    1994

  4. [4]

    W. H. Cornish , journal =. On

  5. [5]

    2000 , publisher=

    Topology , author=. 2000 , publisher=

    2000

  6. [6]

    and van Gool, S

    Gehrke, M. and van Gool, S. , year =. Topological Duality for Distributive Lattices: Theory and Applications , ISBN =. doi:10.1017/9781009349680 , publisher =

    work page doi:10.1017/9781009349680

  7. [7]

    2006 , school =

    Lattices of intermediate and cylindric modal logics , author =. 2006 , school =

    2006

  8. [8]

    , title =

    Litak, T. , title =. Leo Esakia on Duality in Modal and Intuitionistic Logics , series =. 2014 , doi =

    2014

  9. [9]

    2000 , journal =

    Scattered toposes , author =. 2000 , journal =

    2000

  10. [10]

    and Janelidze, G

    Borceux, F. and Janelidze, G. , year =. Galois Theories , place=. doi:10.1017/cbo9780511619939 , publisher =

    work page doi:10.1017/cbo9780511619939

  11. [11]

    , year =

    Visser, A. , year =. On the completenes principle: A study of provability in. Annals of Mathematical Logic , publisher =. doi:10.1016/0003-4843(82)90024-9 , number =

    work page doi:10.1016/0003-4843(82)90024-9

  12. [12]

    Handbook of Boolean algebras , year =

  13. [13]

    Castiglioni, J. L. and Sagastume, M. S. and San Mart. On frontal. Rep. Math. Logic , issn =. 2010 , language =

    2010

  14. [14]

    Hyland, J. M. E. and Johnstone, P. T. and Pitts, A. M. , year =. Tripos theory , volume =. Mathematical Proceedings of the Cambridge Philosophical Society , publisher =. doi:10.1017/s0305004100057534 , number =

    work page doi:10.1017/s0305004100057534

  15. [15]

    Kenney , title =

    T. Kenney , title =. Theory and Applications of Categories , volume =

  16. [16]

    and Kurz, A

    Kupke, C. and Kurz, A. and Venema, Y. , year =. Stone coalgebras , volume =. Theoretical Computer Science , publisher =. doi:10.1016/j.tcs.2004.07.023 , number =

    work page doi:10.1016/j.tcs.2004.07.023 2004

  17. [17]

    Dunn, J. M. and Meyer, R. K. , year =. Algebraic Completeness Results for. Mathematical Logic Quarterly , publisher =. doi:10.1002/malq.19710170126 , number =

    work page doi:10.1002/malq.19710170126

  18. [18]

    Hosoi , year =

    T. Hosoi , year =. On Intermediate Logics. Journal of the Faculty of Science, University of Tokyo, Section I , volume =

  19. [19]

    Horn , journal =

    A. Horn , journal =. Logic with Truth Values in a Linearly Ordered

  20. [20]

    Davey, B. A. and Priestley, H. A. , year=. Introduction to Lattices and Order , publisher=

  21. [21]

    Priestley, H. A. , TITLE =. The Bulletin of the London Mathematical Society , VOLUME =. 1970 , PAGES =

    1970

  22. [22]

    Journal of Symbolic Logic , publisher =

    On an interpretation of second order quantification in first order intuitionistic propositional logic , author =. Journal of Symbolic Logic , publisher =

  23. [23]

    and Zawadowski, M

    Ghilardi, S. and Zawadowski, M. , title =. 2002 , publisher =

    2002

  24. [24]

    , title =

    van Gool, S. , title =. Theory and Applications of Craig Interpolation , publisher=. 2026 , editor =

    2026

  25. [25]

    , title =

    Muravitsky, A. , title =. Leo Esakia on Duality in Modal and Intuitionistic Logics , series =. 2014 , pages =

    2014

  26. [26]

    , year =

    Esakia, L. , year =. The modalized. Journal of Applied Non-Classical Logics , publisher =

  27. [27]

    Canadian Journal of Mathematics , author=

    Simply Connected Limits , volume=. Canadian Journal of Mathematics , author=. 1990 , pages=. doi:10.4153/CJM-1990-038-6 , number=

    work page doi:10.4153/cjm-1990-038-6 1990

  28. [28]

    Kuznetsov , keywords =

    E. Kuznetsov , keywords =. Étale algebras over finite. 2024 , copyright =

    2024

  29. [29]

    Transactions of the American Mathematical Society , year=

    Topologies on spaces of subsets , author=. Transactions of the American Mathematical Society , year=

  30. [30]

    and Harding, J

    Bezhanishvili, G. and Harding, J. and Morandi, P. J. , year =. Remarks on hyperspaces for. doi:10.1016/j.tcs.2022.12.001 , journal =

    work page doi:10.1016/j.tcs.2022.12.001 2022

  31. [31]

    2002 , publisher =

    Sketches of an Elephant: A Topos Theory Compendium , author=. 2002 , publisher =

    2002

  32. [32]

    Pitts, A. M. , TITLE =. Mathematical Structures in Computer Science , VOLUME =. 2002 , NUMBER =

    2002

  33. [33]

    and Sichler, J

    Koubek, V. and Sichler, J. , year =. On. Cahiers Topologie G\'eom. Diff\'erentielle Cat\'eg. , publisher =

  34. [34]

    1972 , journal =

    Aspects of topoi , author =. 1972 , journal =

    1972

  35. [35]

    Johnstone, P. T. , title =. 2012 , howpublished =

    2012

  36. [36]

    Priestley, H. A. , year =. Ordered Sets and Duality for Distributive Lattices , ISBN =. doi:10.1016/s0304-0208(08)73814-3 , booktitle =

    work page doi:10.1016/s0304-0208(08)73814-3

  37. [37]

    Dean, R. A. , title =. Lattice Theory , editor =

  38. [38]

    , title =

    Rival, I. , title =. Ordered Sets , series =. 1982 , note =

    1982

  39. [39]

    2012 , publisher =

    Model theory , author =. 2012 , publisher =

    2012

  40. [40]

    doi: 10.1007/978-3-030-12096-2

    Esakia, L. , title =. 2019 , publisher =. doi:10.1007/978-3-030-12096-2 , keywords =

    work page doi:10.1007/978-3-030-12096-2 2019

  41. [41]

    Esakia , year = 1974, volume = 214, number = 2, pages =

    L. Esakia , year = 1974, volume = 214, number = 2, pages =. Topological

    1974

  42. [42]

    Pitts, A. M. , title =. 2025 , howpublished =

    2025

  43. [43]

    and Kuznetsov, E

    Jibladze, M. and Kuznetsov, E. and Streicher, T. , title =. Book of Abstracts of. 2024 , address =

    2024

  44. [44]

    Is every

    safsom (``Mathematics Stack Exchange'' user) , HOWPUBLISHED =. Is every. 2024 , NOTE =

    2024

  45. [45]

    Constructing a topos from a

    user102845 (``MathOverflow'' user) , year=. Constructing a topos from a

  46. [46]

    Ghilardi , year = 1992, journal =

    S. Ghilardi , year = 1992, journal =. Free

    1992

  47. [47]

    and Moerdijk, I

    Mac Lane, S. and Moerdijk, I. , year =. Sheaves in Geometry and Logic: A First Introduction to Topos Theory , series =

  48. [48]

    Annals of Pure and Applied Logic , volume =

    An explicit. Annals of Pure and Applied Logic , volume =. 2025 , doi=

    2025

  49. [49]

    Almeida, R. N. and Bezhanishvili, G. and Bezhanishvili, N. , keywords =. Esakia order-compactifications and locally. 2025 , note =. doi:10.48550/ARXIV.2512.22042 , url =

    work page doi:10.48550/arxiv.2512.22042 2025

  50. [50]

    Model completion of varieties of co-

    Darni. Model completion of varieties of co-. Houston Journal of Mathematics , issn =. 2018 , language =

    2018

  51. [51]

    Burris and H

    S. Burris and H. P. Sankappanavar , year =. A Course in Universal Algebra , series =

  52. [52]

    Ghilardi and L

    S. Ghilardi and L. Santocanale , title =. Advances in Modal Logic , volume =. 2018 , address =

    2018

  53. [53]

    The Journal of Symbolic Logic , publisher =

    Unification in intuitionistic logic , author =. The Journal of Symbolic Logic , publisher =

  54. [54]

    R. N. Almeida , year=. Representations and model theory of free

  55. [55]

    P. T. Johnstone , publisher=. Topos theory , series =