# nLab decidable object

Contents

### Context

category theory

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

## Idea

The concept of decidable object is the generalization to category theory of the concept of a decidable set from computability theory.

This corresponds to the algebraic and topological concepts unramified, respectively separable object, as pointed out by William Lawvere.

## Definition

An object $X$ of a coherent category $\mathcal{C}$ is called decidable if its equality relation (i.e. its diagonal morphism)

$\Delta_X \;\colon\; X \longrightarrow X \times X$

is complemented, as a subobject of the Cartesian product $X \times X$.

A morphism $f \colon A \to B$ is called decidable if it is a decidable object in the slice category $\mathcal{C}/B$.

## Remarks

• For an object $X$ this means that in the internal logic of the category, it is true that “for any $x,y\in X$ , either $x=y$ or $x\neq y$”.

• In constructive mathematics, where Set is not assumed Boolean, one says that a set $X$ has decidable equality if it is a decidable object of $\Set$.

• A decidable subobject simply means a complemented subobject. Again, in constructive mathematics, a decidable subobject in $\Set$ is called a decidable subset.

• An object $X$ in a topos $\mathcal{E}$ is called anti-decidable if $\neg\neg (x=y)$ in the internal language of $\mathcal{E}$ holds for all $x,y\in X$. A formula $\varphi$ is called almost decidable iff $\neg\varphi\vee\neg\neg\varphi$ holds and an object $X$ is called almost decidable if $x=y$ is almost decidable for $x\in X$.

## Examples

• An initial object and terminal object are always decidable, and so is every natural numbers object $N$ in a topos

• A subobject of a decidable object is decidable.

• Decidable morphisms $f:A\to B$ in the opposite of the category of commutative rings $CommRing^{op}$ are precisely the separable $B$-algebras $A$.

• Of course, in a Boolean category, every object is decidable. Conversely in a topos $\mathcal{E}$, or more generally a coherent category with a subobject classifier, every object is decidable precisely if $\mathcal{E}$ is Boolean.

## Properties

The category of decidable objects in an topos is a Boolean pretopos. The category of decidable objects in a topos is only a topos when the original topos itself is a Boolean topos.

• B. P. Chisala, M.-M. Mawanda, Counting Measure for Kuratowski Finite Parts and Decidability , Cah.Top.Géom.Diff.Cat. XXXII 4 (1991) pp.345-353. (pdf)

• A. Carboni, G. Janelidze, Decidable (=separable) objects and morphisms in lextensive categories , JPAA 110 (1996) pp.219-240.

• Peter Johnstone, Sketches of an Elephant vols. I,II, Oxford UP 2002.