arxiv: 2604.27466 · v1 · submitted 2026-04-30 · 🧮 math.LO · math.CT

Recognition: unknown

A note on computable \'{e}tale spaces

Matthew de Brecht

Pith reviewed 2026-05-07 09:29 UTC · model grok-4.3

classification 🧮 math.LO math.CT

keywords computable topologyétale spacesTTE frameworkquasi-Polish spacesovert-discrete spaceslocal homeomorphismscomputable functionssheaves

0 comments

The pith

Computable étale spaces over a computable topological space Y are equivalent to computable functions from Y to the category ODS of overt-discrete quasi-Polish spaces.

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

The paper defines computable étale spaces in the TTE framework of computable topology as local homeomorphisms equipped with computability data. It proves these objects over a base space Y stand in natural equivalence with computable functions from Y into ODS, the effective quasi-Polish category of overt-discrete spaces. The same correspondence extends to computable categories C, where functors from C to ODS match étale spaces carrying a computable C-action. A reader would care because the result supplies a direct computational representation for local homeomorphisms and sheaf-like data in effective topology.

Core claim

In the TTE framework, a computable étale space over a computable topological space Y is defined via a local homeomorphism carrying computable structure, and this is shown to be naturally equivalent to a computable function from Y to ODS, the effective quasi-Polish category of overt-discrete quasi-Polish spaces. More generally, if C is a computable category or groupoid, then computable functors from C to ODS correspond exactly to computable étale spaces equipped with a computable action by C.

What carries the argument

The TTE-based equivalence between computable local homeomorphisms (étale spaces) and computable functions from the base space into ODS.

If this is right

Computable sheaves on Y become representable by computable functions into ODS.
Computable actions by categories on spaces translate into functors valued in ODS.
Invariants and properties of local homeomorphisms reduce to properties of maps into overt-discrete spaces.
The classical equivalence of sheaves and étale spaces carries over directly to the computable setting.

Where Pith is reading between the lines

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

One could evaluate sections or stalks of a computable sheaf simply by composing the corresponding function to ODS with the appropriate evaluation map.
The result may allow algorithms that decide local homeomorphism properties by checking computability conditions on maps to ODS.
This representation could transfer decidability or computability results from discrete spaces to more general computable topologies.

Load-bearing premise

The TTE representation of computable topological spaces and the definitions of computable functions and overt-discrete spaces are robust enough to capture the intended notion of computable local homeomorphism.

What would settle it

A concrete local homeomorphism over a specific computable space Y that satisfies the intuitive notion of computability yet fails to arise from any computable function to ODS, or a computable function to ODS that fails to produce a computable local homeomorphism.

read the original abstract

An \'{e}tale space over a topological space $Y$ is defined as a local homeomorphism from a topological space $X$ into $Y$. They often come up in topos theory because of the equivalence between sheaves and \'{e}tale spaces over a space. In this note, we define computable \'{e}tale spaces over a computable topological space $Y$ within the TTE framework of computable topology, and show they are naturally equivalent to computable functions from $Y$ to $\mathsf{ODS}$, the effective quasi-Polish category of overt-discrete quasi-Polish spaces. More generally, if $\cal C$ is a computable category (or groupoid), then there is an equivalence between computable functors from $\cal C$ to $\mathsf{ODS}$, and computable \'{e}tale spaces equipped with a computable action by $\cal C$.

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

This note cleanly defines computable étale spaces in TTE and equates them to maps into ODS, with the generalization to category actions as the main addition.

read the letter

The main point is that de Brecht has set up computable étale spaces over a computable base Y inside the TTE model and shown they line up with computable maps from Y into the category ODS of overt-discrete quasi-Polish spaces. The generalization to computable functors from any computable category or groupoid into ODS is also stated directly. This is new as a precise effective counterpart to the classical sheaf-étale equivalence, and the paper does a solid job of keeping the definitions straightforward and tied to existing notions of computable spaces and quasi-Polish spaces without extra machinery. The equivalence appears to follow by translating the usual local-homeomorphism construction into the representation-based setting, which is the right move for this subfield. The work is honest about building on prior TTE and effective descriptive set theory results rather than claiming a broad overhaul. The soft spots are minor and expected for a short note. The proofs are not visible here, but the claim rests on the representations behaving well under the local-homeomorphism condition; if the TTE framework already handles the necessary continuity and effectivity, the equivalence should hold without gaps. No internal contradictions show up in the stated result, and the circularity burden is low since it is an equivalence between two adapted definitions rather than a fitted model. The main limitation is scope: this stays inside computable topology and does not address whether the same equivalence would survive in other computability models or yield new theorems outside the definitional level. This paper is for people already working in computable topology, constructive mathematics, or effective topos theory. A reader who needs a computable version of étale spaces for sheaf-theoretic constructions would find it useful and could build on the ODS equivalence. It shows clear engagement with the literature and the framework, so it deserves a serious referee. I would send it to peer review rather than desk reject.

Referee Report

0 major / 2 minor

Summary. The manuscript defines computable étale spaces over a computable topological space Y in the TTE framework as representations of local homeomorphisms, and establishes a natural equivalence between these and computable functions Y → ODS, where ODS is the effective quasi-Polish category of overt-discrete quasi-Polish spaces. It further claims a generalization: for any computable category (or groupoid) C, there is an equivalence between computable functors C → ODS and computable étale spaces over the base equipped with a computable C-action.

Significance. If the stated equivalences hold, the note supplies a direct effective translation of the classical sheaf-étale space correspondence into computable topology. This could serve as a foundation for computable topos theory or effective versions of geometric morphisms, especially since the construction is presented as a straightforward adaptation without additional parameters or ad-hoc choices.

minor comments (2)

The abstract and introduction state the equivalence but do not indicate the precise category-theoretic functors realizing the 'natural' equivalence (e.g., the direction from computable maps to ODS back to étale spaces). Adding a short diagram or explicit description of the two directions in §2 or §3 would improve readability.
The generalization to computable categories C is announced but the precise definition of 'computable action' on an étale space is not previewed; a one-sentence clarification of how the action is represented in TTE would help readers unfamiliar with the effective groupoid setting.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment of our note and the recommendation for minor revision. The provided summary accurately captures the definitions and equivalences established in the manuscript.

read point-by-point responses

Referee: The manuscript defines computable étale spaces over a computable topological space Y in the TTE framework as representations of local homeomorphisms, and establishes a natural equivalence between these and computable functions Y → ODS, where ODS is the effective quasi-Polish category of overt-discrete quasi-Polish spaces. It further claims a generalization: for any computable category (or groupoid) C, there is an equivalence between computable functors C → ODS and computable étale spaces over the base equipped with a computable C-action.

Authors: We appreciate the referee's concise and accurate summary of the main results. Since the major comments section does not raise any specific objections, questions, or requests for clarification, we have no points requiring rebuttal or revision at this stage. revision: no

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper defines computable étale spaces over a computable space Y in the TTE framework and proves a natural equivalence to computable maps Y → ODS (and a generalization to computable categories). This is a direct translation of the classical sheaf-étale equivalence into an effective setting, with no fitted parameters renamed as predictions, no self-definitional loops, and no load-bearing self-citations that reduce the central claim to prior unverified work by the same author. The equivalence is established by construction from the given representations of computable spaces and overt-discrete spaces, making the derivation self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on the TTE model of computable topology, the existing theory of quasi-Polish spaces, and the definition of overt-discrete spaces; no new free parameters or invented physical entities are introduced.

axioms (2)

domain assumption TTE framework adequately represents computable topological spaces and continuous functions
Invoked throughout the definition of computable étale spaces and computable functions.
standard math Standard properties of quasi-Polish spaces and overt sets
Used to define the target category ODS.

pith-pipeline@v0.9.0 · 5449 in / 1309 out tokens · 57531 ms · 2026-05-07T09:29:52.160408+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

27 extracted references · 1 canonical work pages

[1]

Chen,Borel functors, interpretations, and strong conceptual completeness for Lω1ω, Transactions of the American Mathematical Society372(2019), 8955–8983

R. Chen,Borel functors, interpretations, and strong conceptual completeness for Lω1ω, Transactions of the American Mathematical Society372(2019), 8955–8983

2019
[2]

, ´Etale structures and the Joyal-Tierney representation theorem in countable model theory, To appear in Bull. Symb. Logic (available at arxiv:2310.11539), 2025

work page arXiv 2025
[3]

de Brecht,Quasi-Polish spaces, Annals of Pure and Applied Logic164(2013), 356–381

M. de Brecht,Quasi-Polish spaces, Annals of Pure and Applied Logic164(2013), 356–381

2013
[4]

12098, 2020, pp

,Some notes on spaces of ideals and computable topology, CiE 2020 Pro- ceedings, LNCS, vol. 12098, 2020, pp. 26–37

2020
[5]

,The category of quasi-Polish spaces as a represented space, The 68th Topol- ogy Symposium of the Topology Section of the Mathematical Society of Japan ( https://www.mathsoc.jp/section/topology/topsymp.html), 2021

2021
[6]

de Brecht, J

M. de Brecht, J. Goubault-Larrecq, X. Jia, and Z. Lyu,Domain-complete and LCS- complete spaces, Electronic Notes in Theoretical Computer Science345(2019), 3–35

2019
[7]

de Brecht, T

M. de Brecht, T. Kihara, and V. Selivanov,Ideal presentations and numberings of some classes of effective quasi-Polish spaces, Computability13(2024), 325–348

2024
[8]

de Brecht, A

M. de Brecht, A. Pauly, and M. Schr¨ oder,Overt choice, Computability9(2020), 169–191

2020
[9]

Escard´ o,Synthetic topology of data types and classical spaces, Electronic Notes in Theoretical Computer Science87(2004), 21–156

M. Escard´ o,Synthetic topology of data types and classical spaces, Electronic Notes in Theoretical Computer Science87(2004), 21–156

2004
[10]

Franklin, E

J. Franklin, E. Neumann, A. Pauly, C. Pradic, and M. Valenti,Represented spaces of represented spaces, CiE 2025 Proceedings, LNCS, vol. 15764, 2025, pp. 47–61

2025
[11]

Harrison-Trainor, A

M. Harrison-Trainor, A. Melnikov, R. Miller, and A. Montalb´ an,Computable func- tors and effective interpretability, The Journal of Symbolic Logic82(2017), 77–97

2017
[12]

Heckmann,Spatiality of countably presentable locales (proved with the Baire category theorem), Math

R. Heckmann,Spatiality of countably presentable locales (proved with the Baire category theorem), Math. Struct. in Comp. Science25(2015), 1607–1625

2015
[13]

Hoyrup, C

M. Hoyrup, C. Rojas, V. Selivanov, and D. Stull,Computability on quasi-Polish spaces, Descriptional Complexity of Formal Systems, Springer, 2019, pp. 171–183

2019
[14]

Jacobs,Categorical Logic and Type Theory, Elsevier Science, 1999

B. Jacobs,Categorical Logic and Type Theory, Elsevier Science, 1999

1999
[15]

Joyal and M

A. Joyal and M. Tierney,An extension of the Galois theory of Grothendieck, Mem- oirs of the American Mathematical Society 309, 1984

1984
[16]

Kihara,Lawvere-Tierney topologies for computability theorists, Trans

T. Kihara,Lawvere-Tierney topologies for computability theorists, Trans. Amer. Math. Soc., Series B10(2023), 48–85

2023
[17]

Korovina and O

M. Korovina and O. Kudinov,On higher effective descriptive set theory, Unveiling Dynamics and Complexity, Springer, 2017, pp. 282–291

2017
[18]

Mac Lane and I

S. Mac Lane and I. Moerdijk,Sheaves in Geometry and Logic, Springer-Verlag, 1992

1992
[19]

Miller, B

R. Miller, B. Poonen, H. Schoutens, and A. Shlapentokh,A computable functor from graphs to fields, The Journal of Symbolic Logic83(2018), no. 1, 326–348

2018
[20]

Mummert,On the Reverse Mathematics of General Topology, Ph.D

C. Mummert,On the Reverse Mathematics of General Topology, Ph.D. thesis, Pennsylvania State University, 2005

2005
[21]

Neumann, A

E. Neumann, A. Pauly, C. Pradic, and M. Valenti,Computably discrete represented spaces, CiE 2025 Proceedings, LNCS, vol. 15764, 2025, pp. 349–364

2025
[22]

Pauly,On the topological aspects of the theory of represented spaces, Computabil- ity5(2016), no

A. Pauly,On the topological aspects of the theory of represented spaces, Computabil- ity5(2016), no. 2, 159–180

2016
[23]

Schr¨ oder,Extended admissibility, Theoretical Computer Science284(2002), no

M. Schr¨ oder,Extended admissibility, Theoretical Computer Science284(2002), no. 2, 519 – 538

2002
[24]

Brattka and P

,Admissibly represented spaces and Qcb-spaces, Handbook of Computability and Complexity in Analysis (V. Brattka and P. Hertling, eds.), Springer Interna- tional Publishing, 2021, pp. 305–346

2021
[25]

Selivanov,Towards the effective descriptive set theory, CiE 2015 Proceedings, LNCS, vol

V. Selivanov,Towards the effective descriptive set theory, CiE 2015 Proceedings, LNCS, vol. 9136, Springer, 2015, pp. 324–333

2015
[26]

Vickers,Locales and toposes as spaces, Handbook of Spatial Logics (M

S. Vickers,Locales and toposes as spaces, Handbook of Spatial Logics (M. Aiello, I. Pratt-Hartman, and J. van Bentham, eds.), Springer, 2007, pp. 429–496

2007
[27]

Weihrauch,Computable Analysis, Springer, 2000

K. Weihrauch,Computable Analysis, Springer, 2000

2000