Coexact completion of profinite Heyting algebras and uniform interpolation

Lingyuan Ye

arxiv: 2604.08267 · v2 · submitted 2026-04-09 · 🧮 math.LO · cs.LO· math.CT

Coexact completion of profinite Heyting algebras and uniform interpolation

Lingyuan Ye This is my paper

Pith reviewed 2026-05-10 18:08 UTC · model grok-4.3

classification 🧮 math.LO cs.LOmath.CT

keywords Heyting algebrasprofinite completionsheaf representationuniform interpolationK-toposex/reg completioninfinitary extensive regular category

0 comments

The pith

Profinite completion of Heyting algebras coincides with their sheaf representation.

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

The paper shows that the profinite completion of Heyting algebras supplies the same representation of finitely presented cases that a sheaf construction provides. This follows from proving that the dual category of profinite Heyting algebras is an infinitary extensive regular category whose ex/reg-completion is exactly the K-topos. A sympathetic reader would care because the result unifies an algebraic operation with a logical topos, so that uniform interpolation properties become consequences of the topos internal logic rather than separate verifications.

Core claim

The dual category of profinite Heyting algebras is an infinitary extensive regular category, and its ex/reg-completion is the K-topos that represents finitely presented Heyting algebras via sheaves. This makes profinite completion the algebraic version of the sheaf representation. As a result, certain uniform interpolation properties extend to arbitrary profinite Heyting algebras and follow directly from the internal logic of the K-topos, while further topos-theoretic properties of the K-topos are derived along the way.

What carries the argument

The ex/reg-completion of the dual category of profinite Heyting algebras, which is the K-topos.

If this is right

Uniform interpolation properties extend from finitely presented to arbitrary profinite Heyting algebras.
The extended interpolation properties follow from the internal logic of the K-topos.
Additional topos-theoretic properties of the K-topos are obtained from the completion construction.

Where Pith is reading between the lines

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

The same completion technique might unify algebraic and sheaf representations for other varieties of algebras in intuitionistic logic.
Results about uniform interpolation could transfer more easily between profinite algebraic settings and topos-based ones.
The K-topos construction may supply a template for studying completions in related logical categories.

Load-bearing premise

The dual category of profinite Heyting algebras must be infinitary extensive and regular for its completion to match the sheaf topos.

What would settle it

A specific profinite Heyting algebra whose profinite completion yields a different representation than the K-topos would disprove the claimed equivalence.

read the original abstract

This paper shows that the sheaf representation of finitely presented Heyting algebras constructed by Ghilardi and Zawadowski is, from an algebraic perspective, equivalent to the construction of profinite completion. We show that the dual category of profinite Heyting algebras is an infinitary extensive regular category, and its ex/reg-completion is exactly the aforementioned sheaf topos, which we refer to as the K-topos. We show how certain properties of uniform interpolation can be generalised to the context of arbitrary profinite Heyting algebras, and are consequences of the internal logic of the K-topos. Along the way we also establish various topos-theoretic properties of the K-topos.

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.

Desk Editor's Note private letter to a colleague

Ye shows the Ghilardi-Zawadowski sheaf representation equals profinite completion for Heyting algebras and extends uniform interpolation via the K-topos.

read the letter

The main point is that this paper equates the sheaf representation of finitely presented Heyting algebras from Ghilardi and Zawadowski with the profinite completion construction. It does so by checking that the dual category of profinite Heyting algebras is infinitary extensive and regular, making its ex/reg-completion recover the K-topos exactly. From there it derives uniform interpolation properties for arbitrary profinite Heyting algebras as consequences of the internal logic in that topos, plus some basic topos-theoretic facts about the K-topos itself. This is a direct algebraic unification rather than a restatement of the earlier work. The paper handles the connection cleanly using standard category theory without adding free parameters or circular steps. The K-topos is tied to an existing sheaf topos, which keeps things grounded. The verifications for regularity via kernel pair coequalizers and infinitary extensivity via disjoint coproducts appear to be carried out on the profinite objects themselves, which is the right place to look. No load-bearing gaps show up in the setup. The only real limitation is that the claims are narrow. They organize results inside algebraic logic and topos theory but do not reach outside that circle. A reader already working on Heyting algebras or categorical logic will see the link between the two constructions and pick up the generalized interpolation facts. Someone outside the subfield will not find much to use. The work is coherent on its own terms and uses established methods, so it deserves a serious referee even if the proofs need the usual close check on the category-theoretic details. I would send it to review rather than desk reject.

Referee Report

0 major / 3 minor

Summary. The paper claims that the Ghilardi-Zawadowski sheaf representation of finitely presented Heyting algebras is equivalent, from an algebraic perspective, to profinite completion. It proves that the dual of the category of profinite Heyting algebras is an infinitary extensive regular category whose ex/reg-completion recovers the K-topos (the sheaf topos in question). Properties of uniform interpolation are generalized to arbitrary profinite Heyting algebras as consequences of the internal logic of the K-topos, and various topos-theoretic properties of the K-topos are established along the way.

Significance. If the central identifications hold, the work provides a clean categorical unification of sheaf representations and profinite completions for Heyting algebras. This allows uniform interpolation and related logical properties to be transferred via the internal logic of the K-topos, strengthening connections between algebraic logic and topos theory. The direct verification on profinite objects (rather than reduction to fitted parameters) is a positive feature.

minor comments (3)

§2.3: the notation for the K-topos is introduced without an explicit diagram or commutative square relating the sheaf representation to the profinite completion; adding one would clarify the equivalence claimed in the abstract.
Theorem 4.7: the statement that the ex/reg-completion is exactly the K-topos would benefit from a short remark on how the unit of the completion functor interacts with the existing Ghilardi-Zawadowski embedding.
§5.2: the generalization of uniform interpolation to profinite Heyting algebras is stated in terms of the internal logic, but the precise translation from the topos logic to the algebraic property could be spelled out for one concrete example (e.g., the case of free profinite algebras).

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary of our work and the recommendation of minor revision. No specific major comments were provided in the report, so we have no individual points to address. We are pleased that the equivalence between the Ghilardi-Zawadowski sheaf representation and profinite completion, along with the properties of the K-topos, are viewed as providing a clean categorical unification.

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper connects the Ghilardi-Zawadowski sheaf representation of finitely presented Heyting algebras with profinite completion by directly verifying that the dual of the profinite Heyting algebra category is infinitary extensive regular and that its ex/reg-completion equals the K-topos (the sheaf topos). These verifications rely on standard category-theoretic properties (regularity via coequalizers, infinitary extensivity via coproducts, and exactness of the completion) applied to the profinite objects, without any reduction to self-definitional equations, fitted parameters renamed as predictions, or load-bearing self-citations. The two constructions are treated as independently given and shown equivalent via external categorical machinery; the K-topos is identified with an existing object rather than defined circularly. No steps match the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 1 invented entities

The paper relies on standard axioms and definitions from category theory, topos theory, and algebraic logic. No numerical free parameters are fitted to data. The K-topos is a named identification rather than a new postulated entity with independent evidence.

axioms (2)

standard math Standard axioms and definitions of category theory, including regular categories, extensive categories, ex/reg-completions, and Heyting algebras as models of intuitionistic logic.
Invoked throughout as background for the dual category properties and completions.
domain assumption The dual category of profinite Heyting algebras is infinitary extensive and regular.
Stated as established in the paper and used as the basis for identifying its ex/reg-completion with the K-topos.

invented entities (1)

K-topos no independent evidence
purpose: Name for the ex/reg-completion of the dual category of profinite Heyting algebras, identified with the sheaf topos of Ghilardi and Zawadowski.
Serves as a convenient label for the resulting topos whose internal logic is used to generalize interpolation; no external falsifiable prediction is provided.

pith-pipeline@v0.9.0 · 5401 in / 1619 out tokens · 66115 ms · 2026-05-10T18:08:05.483908+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/ArithmeticFromLogic.lean LogicNat ≃ Nat (recovery theorem) unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

the dual category of profinite Heyting algebras is an infinitary extensive regular category, and its ex/reg-completion is exactly the aforementioned sheaf topos (the K-topos)
IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

uniform interpolation ... consequences of the internal logic of the K-topos

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

6 extracted references · 6 canonical work pages

[1]

Colimits of Heyting algebras through Esakia duality

[Alm24] Rodrigo Nicolau Almeida. Colimits of Heyting algebras through Esakia duality. arXiv preprint arXiv:2402.08058,

work page arXiv
[2]

Flabby and injective objects in toposes

[Ble18] Ingo Blechschmidt. Flabby and injective objects in toposes. arXiv preprint arXiv:1810.12708,

work page arXiv
[3]

A topos-theoretic approach to Stone-type dualities

[Car11] Olivia Caramello. A topos-theoretic approach to Stone-type dualities. arXiv preprint arXiv:1103.3493,

work page Pith review arXiv
[4]

Finite coproducts, coregularity and coexactness for profi- nite interior algebras

[DB25] Matteo De Berardinis. Finite coproducts, coregularity and coexactness for profi- nite interior algebras. arXiv preprint arXiv:2509.13058,

work page arXiv
[5]

A characterisation of the category of compact Hausdorff spaces

[MR20] Vincenzo Marra and Luca Reggio. A characterisation of the category of compact Hausdorff spaces. Theory and Applications of Categories , 35(51):1871–1906,

work page 1906
[6]

Uniform interpolation and layered bisimulation

[Vis96] Albert Visser. Uniform interpolation and layered bisimulation. In Gödel’96: Logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy, Brno, Czech Republic, August 1996, proceedings , volume 6, pages 139–165. Association for Symbolic Logic,

work page 1996

[1] [1]

Colimits of Heyting algebras through Esakia duality

[Alm24] Rodrigo Nicolau Almeida. Colimits of Heyting algebras through Esakia duality. arXiv preprint arXiv:2402.08058,

work page arXiv

[2] [2]

Flabby and injective objects in toposes

[Ble18] Ingo Blechschmidt. Flabby and injective objects in toposes. arXiv preprint arXiv:1810.12708,

work page arXiv

[3] [3]

A topos-theoretic approach to Stone-type dualities

[Car11] Olivia Caramello. A topos-theoretic approach to Stone-type dualities. arXiv preprint arXiv:1103.3493,

work page Pith review arXiv

[4] [4]

Finite coproducts, coregularity and coexactness for profi- nite interior algebras

[DB25] Matteo De Berardinis. Finite coproducts, coregularity and coexactness for profi- nite interior algebras. arXiv preprint arXiv:2509.13058,

work page arXiv

[5] [5]

A characterisation of the category of compact Hausdorff spaces

[MR20] Vincenzo Marra and Luca Reggio. A characterisation of the category of compact Hausdorff spaces. Theory and Applications of Categories , 35(51):1871–1906,

work page 1906

[6] [6]

Uniform interpolation and layered bisimulation

[Vis96] Albert Visser. Uniform interpolation and layered bisimulation. In Gödel’96: Logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy, Brno, Czech Republic, August 1996, proceedings , volume 6, pages 139–165. Association for Symbolic Logic,

work page 1996