nLab decidable object

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.

Related concepts

• theory of decidable objects

• locally decidable topos

• finite object

• separable algebra

References

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