arxiv: 2602.15583 · v3 · submitted 2026-02-17 · 🧮 math.GN · math.CT

Recognition: 2 theorem links

· Lean Theorem

The lattice of smooth sublocales as a Bruns-Lakser completion

Igor Arrieta , Anna Laura Suarez

Authors on Pith no claims yet

Pith reviewed 2026-05-15 22:09 UTC · model grok-4.3

classification 🧮 math.GN math.CT

keywords sublocalessmooth sublocalesBruns-Lakser completionlocally closed sublocalesframe morphismsBooleanizationlocale theory

0 comments

The pith

The collection of smooth sublocales of a frame is the Bruns-Lakser completion of its locally closed sublocales.

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

The paper establishes that the lattice S_b(L) of smooth sublocales in a frame L coincides with the Bruns-Lakser completion of the meet-semilattice of locally closed sublocales. This equivalence also characterises the frame morphisms from L to M that extend to maps between the respective smooth sublocale lattices. If true, this provides a concrete construction for the Booleanization of the full sublocale lattice using only the locally closed ones. Readers interested in pointfree topology would gain a tool for handling morphisms and completions in locale theory without directly working with all sublocales.

Core claim

We characterise the frame morphisms f:L→M that lift to frame maps overline{f}:S_b(L)→S_b(M) by proving that S_b(L) is isomorphic to the Bruns--Lakser completion of the meet-semilattice formed by the locally closed sublocales, i.e. the sublocales of the form c(a) ∩ o(b) for a,b in L.

What carries the argument

The Bruns-Lakser completion of the meet-semilattice of locally closed sublocales, serving as an isomorphic representation of the lattice S_b(L) of smooth sublocales.

If this is right

Frame morphisms preserving the necessary properties lift to maps on the smooth sublocale lattices.
The Booleanization of the sublocale lattice is realised through this completion process.
S_b(L) can be constructed directly from locally closed sublocales without reference to all sublocales.

Where Pith is reading between the lines

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

This view may simplify the study of lifting properties for morphisms in locale theory.
It connects the theory of sublocales to order-theoretic completions, potentially applicable to other posets in topology.
Checking the isomorphism on concrete frames like the reals could verify the result in practice.

Load-bearing premise

The standard definitions of complemented sublocales, locally closed sublocales, and the Bruns-Lakser completion for meet-semilattices hold, and the isomorphism preserves the frame map properties.

What would settle it

Constructing a frame L for which the lattice of joins of complemented sublocales is not isomorphic to the Bruns-Lakser completion of its locally closed sublocales.

read the original abstract

We characterise the frame morphisms $f:L\to M$ that lift to frame maps $\overline{f}:\mathsf{S}_b(L)\to \mathsf{S}_b(M)$, where $\mathsf{S}_b(L)$ is the collection of joins of complemented sublocales of a frame $L$, or equivalently the Booleanization of the collection $\mathsf{S}(L)$ of all its sublocales. We do so by proving that $\mathsf{S}_b(L)$ is isomorphic to the Bruns--Lakser completion of the meet-semilattice formed by the locally closed sublocales, i.e. the sublocales of the form $\mathfrak{c}(a)\cap \mathfrak{o}(b)$ for $a,b\in L$.

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

S_b(L) is the Bruns-Lakser completion of the locally closed sublocales, which gives a clean characterization of lifting frame morphisms.

read the letter

The punchline is that S_b(L) turns out to be the Bruns-Lakser completion of the meet-semilattice of locally closed sublocales c(a) ∩ o(b). This isomorphism then pins down exactly which frame morphisms from L to M lift to maps between the smooth sublocales. The paper does a good job of making this connection explicit. By routing through the completion, it gives a standard algebraic handle on the Booleanization of the sublocale lattice. That could simplify arguments about complemented sublocales and their joins in future work. It avoids heavy new machinery and sticks to established completions. The new element is the characterization of the lifting morphisms via this isomorphism. It is not presented as prior art, so it adds a specific tool to the toolkit for locale theorists. On the soft side, the main thing to watch is whether the isomorphism is sufficiently natural to carry the frame operations without extra conditions. The abstract suggests it works directly, and there are no red flags in the setup. The definitions used are standard, so the burden is on verifying the details of the proof rather than questioning the framework. No circularity or invented concepts appear. This is squarely for people who already know their way around frames and sublocales. A reader who follows papers on pointfree topology would see the value in having this reorganization. I think it deserves peer review. The claim is focused and the approach is grounded, so referees can sort out if the isomorphism holds as stated and if it opens any new questions.

Referee Report

0 major / 3 minor

Summary. The paper proves that for a frame L, the lattice S_b(L) of joins of complemented sublocales (equivalently, the Booleanization of the sublocale lattice S(L)) is isomorphic to the Bruns-Lakser completion of the meet-semilattice of locally closed sublocales of the form c(a) ∩ o(b) for a, b in L. This isomorphism is then used to characterize those frame morphisms f: L → M that lift to frame maps on S_b.

Significance. If the central isomorphism holds, the result supplies a concrete, standard-construction description of the smooth sublocale lattice, which should facilitate the study of morphism liftings and Booleanizations in pointfree topology. The approach relies on standard definitions of complemented and locally closed sublocales together with the Bruns-Lakser completion for meet-semilattices, and the manuscript supplies the required verification that the isomorphism preserves the necessary frame operations.

minor comments (3)

[§1] §1, first paragraph after the abstract: the notation S_b(L) is introduced without an immediate explicit definition; add a parenthetical gloss such as “the lattice of joins of complemented sublocales” on first use.
[Theorem 3.4] Theorem 3.4 (the main isomorphism): the proof sketch refers to “the universal property of the Bruns-Lakser completion” without citing the precise statement (e.g., the reference or the numbered property) used; supply the citation or internal lemma number.
[Figure 1] Figure 1 (the commutative diagram for lifted morphisms): the arrow labels are too small to read comfortably in the printed version; enlarge the font or add a textual description of the diagram.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive report, accurate summary of our results, and recommendation of minor revision. No specific major comments appear in the report, so we have no points requiring rebuttal or detailed response. We will incorporate any minor editorial or presentational changes in the revised version.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper establishes an isomorphism between S_b(L) (joins of complemented sublocales, or Booleanization of S(L)) and the Bruns-Lakser completion of the meet-semilattice of locally closed sublocales c(a) ∩ o(b) via a direct proof. This relies on standard external definitions of complemented sublocales, locally closed sublocales, and the Bruns-Lakser construction for meet-semilattices, without any reduction of the central claim to self-defined quantities, fitted inputs renamed as predictions, or load-bearing self-citations. The derivation chain is self-contained against external frame-theoretic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

Based solely on the abstract, the paper relies on standard domain assumptions from frame and locale theory with no new free parameters or invented entities visible.

axioms (2)

domain assumption Standard definitions and properties of frames, sublocales, complemented sublocales, and locally closed sublocales hold as in the literature on pointfree topology.
The result is stated in terms of these established concepts.
domain assumption The Bruns-Lakser completion is the standard one for meet-semilattices.
Invoked directly in the isomorphism claim.

pith-pipeline@v0.9.0 · 5420 in / 1260 out tokens · 32761 ms · 2026-05-15T22:09:56.909413+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/AbsoluteFloorClosure.lean absolute_floor_iff_bare_distinguishability unclear

?

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

the admissible meets of LC(L) are exactly the joins of locally closed sublocales which are themselves locally closed

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

22 extracted references · 22 canonical work pages

[1]

Arrieta,A study of localic subspaces, separation, and variants of normality and their duals, PhD thesis, University of Coimbra and University of the Basque Country (UPV/EHU), 2022

I. Arrieta,A study of localic subspaces, separation, and variants of normality and their duals, PhD thesis, University of Coimbra and University of the Basque Country (UPV/EHU), 2022

work page 2022
[2]

Arrieta, On joins of complemented sublocales,Algebra Universalis83(2022), Article no

I. Arrieta, On joins of complemented sublocales,Algebra Universalis83(2022), Article no. 1

work page 2022
[3]

R. N. Ball, M. A. Moshier, and A. Pultr, Exact filters and joins of closed sublocales, Applied Categorical Structures28(2020), 655–667

work page 2020
[4]

R. N. Ball, J. Picado, and A. Pultr, Notes on exact meets and joins,Applied Categorical Structures22(2014), 699–714

work page 2014
[5]

R. N. Ball, J. Picado, and A. Pultr, Some aspects of (non) functoriality of natural discrete covers of locales,Quaestiones Mathematicae42(2019), 701–715

work page 2019
[6]

R. N. Ball and A. Pultr, Maximal essential extensions in the context of frames,Algebra Universalis79(2018), Article no. 32

work page 2018
[7]

Bezhanishvili, F

G. Bezhanishvili, F. Dashiell, A. Razafindrakoto, and J. Walters-Wayland, Semilattice base hierarchy for frames and its topological ramifications,Applied Categorical Structures 32(2024), Article no. 18

work page 2024
[8]

Bezhanishvili, D

G. Bezhanishvili, D. Gabelaia, and M. Jibladze, Funayama’s theorem revisited,Algebra Universalis70(2013), 271–286

work page 2013
[9]

Bezhanishvili, R

G. Bezhanishvili, R. Raviprakash, A. L. Suarez, and J. Walters-Wayland, The Funayama envelope as the TD-hull of a frame,Theory and Applications of Categories44(2025), Paper no. 33, 1106–1147

work page 2025
[10]

Bruns and H

G. Bruns and H. Lakser, Injective hulls of semilattices,Canadian Mathematical Bulletin 13(1970), 115–118

work page 1970
[11]

Funayama, Imbedding infinitely distributive lattices completely isomorphically into Boolean algebras,Nagoya Mathematical Journal15(1959), 71–81

N. Funayama, Imbedding infinitely distributive lattices completely isomorphically into Boolean algebras,Nagoya Mathematical Journal15(1959), 71–81

work page 1959
[12]

Gehrke and S

M. Gehrke and S. van Gool, Distributive envelopes and topological duality for lattices via canonical extensions,Order31(2014), 435–461

work page 2014
[13]

Gehrke and H

M. Gehrke and H. Priestley, Canonical extensions and completions of posets and lat- tices,Reports on Mathematical Logic(2008)

work page 2008
[14]

Jakl and A

T. Jakl and A. L. Suarez, Canonical extensions via fitted sublocales,Applied Categorical Structures33(2025), Article no. 10

work page 2025
[15]

P . T. Johnstone,Stone Spaces, Cambridge Studies in Advanced Mathematics, Vol. 3, Cambridge University Press, Cambridge, 1982

work page 1982
[16]

M. A. Moshier, J. Picado, and A. Pultr, Some general aspects of exactness and strong exactness of meets,Topology and Its Applications309(2022), Article no. 107906

work page 2022
[17]

M. A. Moshier, A. Pultr, and A. L. Suarez, Exact and strongly exact filters,Applied Categorical Structures28(2020), 907–920

work page 2020
[18]

Picado and A

J. Picado and A. Pultr,Frames and Locales: Topology Without Points, Frontiers in Mathe- matics, Vol. 28, Springer, Basel, 2012. THE LATTICE OF SMOOTH SUBLOCALES AS A BRUNS–LAKSER COMPLETION 19

work page 2012
[19]

Picado and A

J. Picado and A. Pultr, A Boolean extension of a frame and a representation of discon- tinuity,Quaestiones Mathematicae40(2017), 1111–1125

work page 2017
[20]

Picado, A

J. Picado, A. Pultr, and A. Tozzi, Joins of closed sublocales,Houston Journal of Mathe- matics45(2019), 21–38

work page 2019
[21]

A. L. Suarez, Raney extensions: A pointfree theory ofT 0 spaces based on canonical extension,Journal of Pure and Applied Algebra229(2025), Article no. 108137

work page 2025
[22]

Wilson,The Assembly Tower and Some Categorical and Algebraic Aspects of Frame Theory, PhD thesis, Carnegie Mellon University, 1994

J. Wilson,The Assembly Tower and Some Categorical and Algebraic Aspects of Frame Theory, PhD thesis, Carnegie Mellon University, 1994. * Departamento deMatem´aticas Universidad delPa´ısVascoUPV/EHU 48080 Bilbao SPAIN Email address:igor.arrieta@ehu.eus ** Department ofMathematics andAppliedMathematics University of theWesternCape PrivateBagX17 Bellville753...

work page 1994