A note on computable étale spaces

Abstract

An é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 étale spaces over a space. In this note, we define computable é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 $\mathcal{C}$ is a computable category (or groupoid), then there is an equivalence between computable functors from $\mathcal{C}$ to $\mathsf{ODS}$, and computable étale spaces equipped with a computable action by $\mathcal{C}$.