arxiv: 2605.04038 · v1 · submitted 2026-05-05 · 🧮 math.CT · math.LO

Recognition: 4 theorem links

· Lean Theorem

Localic Relations with Open Cones

Nesta van der Schaaf

Pith reviewed 2026-05-06 04:59 UTC · model claude-opus-4-7

classification 🧮 math.CT math.LO MSC <parameter name="1">06D22

keywords <parameter name="1">localic relations

0 comments

The pith

An open-cone localic relation is determined, up to a strongly dense inclusion, by a join-preserving parallel pair of operators on its frame of opens.

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

The paper sets out to give a frame-theoretic, point-free description of the relations that one can put on a locale, in the spirit of how one studies relations on a set via the up- and down-closures they induce on the powerset. Restricting to relations whose source and target maps are open as locale maps, the author shows the induced cones △,▽ on the underlying frame are join-preserving and "parallel," and packages this data as a "conic frame." From any conic frame one can reconstruct an open-cone localic relation R^△▽ whose cones are exactly the given ones, and this gives an adjunction with identity counit between locales with open-cone relations and conic frames. The original relation R sits inside the reconstructed R^△▽ via a strongly dense inclusion, and the inclusion is an isomorphism for weakly closed relations and for kernel pairs of open maps — a generalisation of Kock's Godement theorem for locales. Reflexivity, transitivity, and symmetry of fixed-point relations are then characterised cleanly as inflationarity, sub-idempotence, and equality of the two cones.

Core claim

For locales equipped with a binary relation whose source and target maps are open ("open cone" relations), the relation's induced up- and down-closure operators on the frame of opens form a join-preserving "parallel" pair, and conversely any such pair (a "conic frame") generates an open-cone relation whose cones recover the pair. This pairing is an adjunction Cone ⊣ Rel between locales-with-open-cone-relations and the opposite of conic frames, with identity counit, so conic frames are reflective inside open-cone relations. The unit embeds any open-cone relation R into the relation R^△▽ generated by its own cones via a strongly dense inclusion, and any weakly closed open-cone relation is a fi

What carries the argument

A "conic frame" (L,△,▽): a frame with a join-preserving parallel pair of operators (parallel meaning △x ∧ y ⊑ △(x ∧ ▽y) and the symmetric inequality). The reconstruction proceeds by defining a relation ∼ on the rectangles of L⊗L via the reduced cones (▲(x,y), ▼(x,y)) = (△x∧y, x∧▽y), showing parallelness makes ∼ a meet-semilattice congruence, and taking the induced sublocale of X×X. Frobenius reciprocity for the open source/target maps is what forces parallelness on the frame side and produces the left adjoints s!, t! that define the cones.

If this is right

<parameter name="1">Any weakly closed open-cone localic equivalence relation is the kernel pair of its quotient map
recovering Kock's Godement theorem from a more general unit-of-adjunction argument.

Where Pith is reading between the lines

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

<parameter name="1">The framework looks well-suited to a localic Esakia or Priestley-type duality once a one-sided (target-only-open) version of conic frames is developed
which the author flags as forthcoming.

Load-bearing premise

The whole construction depends on the source and target maps of the relation being open as locale maps; without that openness the natural cones on sublocales need not preserve infinite joins, need not be parallel, and relational composition stops being associative.

What would settle it

Exhibit two distinct open-cone localic relations R ≠ R' on the same locale X whose induced operators (△,▽) on OX coincide and which are both fixed points of the adjunction; or alternatively, exhibit a weakly closed open-cone relation R for which the canonical inclusion R ⊆ R^△▽ fails to be an isomorphism. Either would break the main reflectivity/Godement claim.

read the original abstract

Localic relations are relations internal to the category of locales, forming the point-free analogues of set-theoretic relations, and providing the general backdrop of localic order theory. This work studies 'open cone' localic relations, whose source and target maps are open, and provides a frame-theoretic description via point-free up and down closure operators, called 'cones'. The cones arising from open cone localic relations form join-preserving and 'parallel' pairs of maps on the underlying frame. Axiomatising this structure, a frame equipped with such a pair of cones is called a 'conic frame'. The main construction shows that, conversely, any conic frame induces a localic relation with open cones, whose cones are exactly the given ones. The main result is an adjunction with identity counit between the category of locales equipped with open cone localic relations, and the opposite of the category of conic frames. The unit gives a strongly dense inclusion of an open cone localic relation into the relation induced by its own cones. Fixed points of the adjunction are those relations recovered by their cones, and include kernel pairs of open maps and all weakly closed localic relations with open cones. As a special case we recover Kock's Godement theorem for locales. Moreover, for fixed points, internal reflexivity and transitivity are completely characterised in terms of the cones.

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

Solid structural locale theory: a clean adjunction with identity counit between open-cone localic relations and "conic frames," with Kock's Godement theorem falling out as a corollary.

read the letter

Worth a look. Van der Schaaf isolates the algebraic shadow of a localic relation whose source and target maps are open: a frame L with a join-preserving "parallel" pair △,▽ : L → L, which he calls a conic frame. The main theorem (8.3) is an adjunction Cone ⊣ Rel between rocLoc and Frmᶜᵒⁿᵉᵒᵖ whose counit is strictly the identity. So conic frames sit as a reflective subcategory, every conic frame is a fixed point automatically, and a relation R is a fixed point iff R ≅ R^△▽ where △,▽ are its own induced cones.

What's genuinely new: the axiomatisation itself, the L⊗L/∼ construction recovering a "universal" relation with prescribed cones (§7), and the strong-density result (Prop 9.20) that R ⊆ R^△▽ is always strongly dense in Johnstone's sense. From that, Kock's Godement theorem for localic equivalence relations falls out as Cor 9.22, and you get a clean cone-level characterisation of reflexivity, transitivity, symmetry on fixed points (Prop 10.11). The §11 isomorphism with a subcategory of P-ordered locales tidies up earlier work of his with Heunen.

The math is workmanlike rather than flashy. The load-bearing step — open s,t plus Frobenius gives parallelness of the induced cones (Prop 6.4) — is a one-line calculation. The harder bookkeeping is in §6, identifying the suplattice tensor with the frame coproduct (Prop 6.18) so that △,▽ join-preserving is the same as "separating," then checking ∼ is a meet-semilattice congruence under parallelness (Prop 6.9). It's all standard frame-coproduct machinery from Picado–Pultr and MPP17, applied carefully. I checked the rectangle calculations in §7 and they're right.

Soft spots are mostly scope, not soundness. Openness of s,t is doing real work and the author is honest about it: §12.1–12.2 give an explicit T op-side counterexample where without openness the internal cones on Sℓ(X) fail to be parallel and fail to preserve infinite joins, and relational composition is non-associative. Counterexample 9.4 (Sierpiński) shows the unit isn't generally an iso, and §10 leaves open whether fixed points are closed under composition (Remark 10.12 — a real gap, acknowledged). The "topological over Frm" question (§12.6) is a small negative result, fine. Citations look complete and proportionate; self-citation to vdS24 is to the author's thesis where longer proofs live.

Audience: locale theorists, people working on point-free order theory, Stone/Priestley/Esakia duality, possibly modal logic semantics. Send to peer review. The reader's ACCEPT verdict is right; the stress-test note is also right that there's no internal soundness issue.

Referee Report

0 major / 11 minor

Summary. The paper introduces "conic frames" (L,△,▽) — frames equipped with a join-preserving parallel pair of endomaps — as the algebraic counterpart of localic relations whose source and target maps are open ("open cone relations"). The main results are: (i) any open cone localic relation R on X induces a conic-frame structure (OX,⌝,⌜) via ⌝ = t! s⁻¹, ⌜ = s! t⁻¹ (Props. 6.3, 6.4); (ii) conversely, any conic frame (L,△,▽) gives a localic relation R△▽ on the corresponding locale, defined as the sublocale of L⊗L cut out by an explicit relation ∼ on rectangles, and Cone(R△▽) = (L,△,▽) on the nose (Thm 7.7); (iii) these constructions assemble into an adjunction Cone ⊣ Rel : rocLoc ⇄ Frmᶜᵒⁿᵉᵒᵖ with identity counit (Thm 8.3); (iv) the unit R ↪ R⌝⌜ is always a strongly dense sublocale inclusion (Prop. 9.20), so all weakly closed open cone relations are fixed points (Cor. 9.21), recovering Kock's Godement theorem (Cor. 9.22) as a special case. Sections 10–11 characterise reflexivity/transitivity/symmetry of fixed points in terms of the cones and identify Frmᶜᵒⁿᵉᵒᵖ_⩽ with a category of P-ordered locales determined by cones (Thm 11.21).

Significance. If correct, the paper supplies a clean algebraic externalisation for the well-studied class of open cone localic relations, with an identity-counit adjunction that turns Frmᶜᵒⁿᵉᵒᵖ into a strict reflective subcategory of rocLoc. Concretely: (a) the strongly dense inclusion R ↪ R⌝⌜ (Prop. 9.20) is a uniform generalisation of Kock's [Koc89] result for localic equivalence relations, reproved here without any equivalence-relation hypothesis; (b) the characterisation of reflexivity and transitivity for fixed points (Prop. 10.11) gives a workable algebraic handle on localic preorders; (c) the explicit isomorphism Frmᶜᵒⁿᵉᵒᵖ_⩽ ≅ PLoc_= (Thm 11.21) clarifies the relationship to the ordered-locale framework of [HS24]. The proofs are short calculations in standard frame-coproduct machinery (Picado–Pultr §III.11, MPP17), the suplattice-tensor identification used in Prop. 6.18 is properly cited, and the openness hypothesis is hypothesised throughout rather than smuggled in. Counterexamples 9.4 and 10.10, and the explicit T op-side discussion in §12.1–12.2, are honest about the limits of the framework. The work plausibly enables the forthcoming localic Esakia duality and connects to several exist

minor comments (11)

[Title page / arXiv id] The title page is dated '5 May 2026' and the paper carries arXiv id 2605.04038. Please verify the date and identifier before publication; a future date is presumably a typo or a preprint-server artifact.
[§1 Introduction] The Introduction states 'composition in rocLoc is not relational composition (which for locales is not associative)' but the supporting argument (non-pullback-stable epis) appears only in §12.2. A one-line forward reference at this point would help the reader who is surprised that rocLoc is not a category of relations in the usual sense.
[§3.1, Lemma 3.7] The proof uses 'image maps preserve unions' to conclude s,t preserve arbitrary opens; it would be slightly cleaner to note explicitly that the rectangles U×V ∩ R form a basis closed under finite intersections, since the argument as stated relies on this implicitly.
[§4.2, Definition 4.13] The notation ⌝, ⌜ for the cones is used throughout but is set in a way that is hard to parse in inline text (especially when combined with reduced cones ▲, ▼). A short notation table near this definition, or a different choice of glyphs, would substantially improve readability of §6–§9.
[§6.2, Prop. 6.18] The proof invokes 'the suplattice tensor product' and cites [Joh82, §II.2.12] and [JV91, §1]. Since this is the only nontrivial input on which separation = join-preservation rests, a sentence stating the universal property used (suplattice bihomomorphisms factor uniquely through L⊗M) would make the section self-contained.
[§9, Counterexample 9.4] The Sierpiński computation is the load-bearing example showing that fixed points are not closed under finite joins (combined with Example 9.5). Consider tabulating ∼-classes explicitly so the reader can see at a glance that ⟨∼⟩ = =.
[§10.2, Remark 10.12] It is worth flagging more prominently that the open question 'is R△▽ ∘ R△▽ = R△∘△,▽∘▽?' obstructs an iff-characterisation of interpolativity for fixed points. Currently the remark sits at the end of the section and is easy to miss.
[§11, Remark 11.22] The discussion of why an adjunction between ordered spaces and conic frames is unlikely (failure of pt to preserve open maps; L not preserving transitivity, citing [Joh02, Remark C5.3.5]) is interesting but compressed. A few more sentences would help readers who do not have [Joh02] at hand.
[§12.6] The argument that U: Frmᶜᵒⁿᵉ → Frm is not topological is clear but uses the specific frame OR of the reals; clarifying that any frame admitting a non-trivial open between {0} and a chosen element would do (and noting whether this requires classical logic) would strengthen the remark.
[References] [Gou26] is cited as 'recently introduced ad-frames' and listed with arXiv:2601.12932; verify the citation and year. Several entries (e.g. [vdS]) are 'in preparation' — standard, but ensure the final version has the most up-to-date references.
[General] Many proofs are very short paragraphs of inline calculation. They are correct as far as I checked, but readers would benefit from displayed equations (numbered) for the parallelness identity, the ∼ definition (Def. 6.5), and the s!, t! formulas (Lemma 7.3), since these are referenced repeatedly.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the thorough and accurate summary of the paper and for the recommendation of minor revision. The referee's report contains no listed major comments: the substantive content is a summary of the results, an assessment of significance, and a recognition that counterexamples and limitations (notably §12.1–12.2, Counterexamples 9.4 and 10.10, and Remark 10.12) are honestly stated. As such, there are no points of mathematical disagreement to address and no required structural changes. We will undertake a routine editorial pass to correct any typographical issues and to polish exposition before submitting the revised version, but the mathematical content stands as written. We are grateful for the referee's careful reading and supportive evaluation.

read point-by-point responses

Referee: The referee recommends minor revision and provides a detailed and accurate summary of the paper's contributions, noting in particular: (a) the strongly dense inclusion R ↪ R⌝⌜ as a uniform generalisation of Kock's theorem; (b) the algebraic handle on reflexivity/transitivity for fixed points; (c) the isomorphism Frmᶜᵒⁿᵉᵒᵖ_⩽ ≅ PLoc_= clarifying the link to ordered locales. The referee also notes that Counterexamples 9.4 and 10.10 and the discussion in §12.1–12.2 are honest about limitations.

Authors: We thank the referee for the careful and accurate reading of the manuscript, and for the favourable recommendation. We are grateful that the structure of the argument — the Cone⊣Rel adjunction, the strongly dense unit, and the recovery of Kock's Godement theorem as a special case — has been faithfully summarised, and that the limits of the framework (in particular the obstructions discussed in §12.1–12.2 and the open question in Remark 10.12 concerning interpolativity and closure of fixed points under composition) have been correctly identified as genuine and acknowledged in the text rather than glossed over. No specific major comments requiring substantive changes were raised. We will make a careful editorial pass for typographical and presentational improvements in the revised version, but no mathematical content needs to be altered in response to the report. revision: no

Circularity Check

0 steps flagged

No significant circularity: the Cone ⊣ Rel adjunction is verified by explicit frame-coproduct calculations against external references (Picado–Pultr, MPP17, JT84, Koc89).

full rationale

The paper's central claim — Theorem 8.3 (adjunction Cone ⊣ Rel with identity counit) — is established by a chain of small, individually checkable lemmas, each of which is either (a) a direct computation in the frame coproduct L⊗L using only standard identities recalled from Picado–Pultr §III.11 and Moshier–Picado–Pultr 2017, or (b) an application of Frobenius reciprocity in the Joyal–Tierney sense (JT84). The load-bearing steps are: Prop 6.3 (cones preserve joins, immediate from s⁻¹,t⁻¹ being frame maps and s_!,t_! being left adjoints); Prop 6.4 (parallelness, one-line use of Frobenius for t plus the unit s⁻¹s_! ≥ id); Prop 6.9 (∼ is a meet-semilattice congruence, by monotonicity of ▲,▼); Prop 6.18 (separation = join-preservation, via the suplattice tensor identification of L⊗L from Joyal–Vickers 1991); Prop 7.4 and 7.6 (adjunction and Frobenius for the constructed s_!,t_!, checked on the rectangle basis); Thm 7.7 (Cone∘Rel = id, by direct computation t_!s⁻¹(U⊗⊤) = △U ∧ ⊤ = △U); Prop 7.11 (R ⊆ R^△▽, via the universal property of the frame quotient applied to r⁻¹). None of these steps redefines its conclusion as its hypothesis. The "prediction" Cone(Rel(△,▽)) = (△,▽) is not a fit; it is a strict equality verified by Lemma 7.3, which itself follows from the explicit Definition 7.2 of s_! together with Prop 6.22. Self-citations to vdS24 (the author's thesis) and to HS24/HS25 are used either for background (§3, §11) or to record that the present construction generalises a previously studied notion; they are not load-bearing for Theorem 8.3. The Kock 1989 Godement theorem is recovered (Cor 9.22) as a special case of an independently proven strong-density result (Prop 9.20), not assumed. The openness hypothesis is a stated scope condition, not a hidden assumption — §12.1–12.2 explicitly exhibit counterexamples when it is dropped. Overall the derivation is self-contained against external frame-theoretic machinery; no step is equivalent to its input by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

[{"axiom": "Open cone hypothesis: source and target maps of the localic relation are open", "kind": "domain_assumption", "rationale": "Load-bearing throughout; without it the existence of s!, t! and Frobenius reciprocity fails, and §12.2 documents that the resulting cones on Sℓ(X) need not be parallel."}, {"axiom": "Picado–Pultr / Moshier–Picado–Pultr theory of generating sublocales from binary relations on a frame", "kind": "standard_math", "rationale": "Used in Definition 7.1 and Theorem 2.7 to define R^△▽ as the sublocale induced by the frame congruence generated by ∼."}, {"axiom": "Joyal–Tierney open-map theory and its consequences (Lemma 9.7 on pullbacks of open maps)", "kind": "standard_math", "rationale": "Standard locale-theoretic input; cited from [JT84] and [Joh02]."}]

pith-pipeline@v0.9.0 · 70685 in / 5854 out tokens · 95053 ms · 2026-05-06T04:59:51.540121+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.

Foundation/UniversalForcing/NaturalNumberObject.lean IsNaturalNumberObject (universal property style — only a structural echo, not isomorphic content) echoes
The main result is an adjunction with identity counit between the category of locales equipped with open cone localic relations, and the opposite of the category of conic frames.
Cost.lean Jcost_symm (reciprocal symmetry J(x)=J(1/x)) echoes
A pair of cones △, ▽ : L → L on a meet-semilattice is called parallel if for all x,y ∈ L: △x ∧ y ⊑ △(x ∧ ▽y) and x ∧ ▽y ⊑ ▽(△x ∧ y). … Note the resemblance of parallelness to the Frobenius reciprocity condition. … Conjugate pairs (Jónsson–Tarski 1951): △x ∧ y = ⊥ iff x ∧ ▽y = ⊥.
Foundation/PrimitiveDistinction.lean non_contradiction_from_equality (symmetry of comparison cost) unclear
Definition 4.10 (Open locale map): f_! ⊣ f^{-1} satisfying Frobenius reciprocity f_!(U ∧ f^{-1}(V)) = f_!(U) ∧ V. … Proposition 6.4: the cones _,_ are parallel (proof uses Frobenius reciprocity for t and s_! ⊣ s^{-1}).
Foundation/RealityFromDistinction.lean reality_from_one_distinction (no relation — different domain) unclear
Theorem 8.3: rocLoc ⇄ Frm_◇^op, Cone ⊣ Rel, with identity counit. The unit is a strongly dense inclusion R ⊆ R^△▽. Corollary 9.22 reobtains Kock's Godement theorem.