A note on computable \'{e}tale spaces

TL;DR

This paper introduces computable e9tale spaces over computable topological spaces within the TTE framework, establishing their equivalence to computable functions into the effective quasi-Polish category.

Contribution

It defines computable e9tale spaces in the TTE framework and proves their equivalence to computable functions into the effective quasi-Polish category, extending to computable categories and groupoids.

Findings

Computable e9tale spaces are equivalent to computable functions into a9ODS.

The framework extends to computable categories and groupoids with actions.

Establishes a bridge between computable topology and category theory.

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$.