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 a topos is regular, extensive and full on subobjects (Berger & Iwaniack Lem. 1.3(6)), but not in general Boolean or a pretopos (cf. B&I Rem 1.6 and math.SE:q/5138618; unless, of course, the starting topos was a Boolean topos). See also at Subcategories of finite objects.

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, Cahiers Top. Géom. Diff. Cat. XXXII 4 (1991) 345–353 [numdam:CTGDC_1991__32_4_345_0, pdf]

• Aurelio Carboni, George Janelidze: Decidable (=separable) objects and morphisms in lextensive categories, JPAA 110 (1996) 219–240

• Peter Johnstone: Sketches of an elephant: a topos theory compendium, Oxford University Press (2002), Volume 1 [ISBN:9780198534259], Volume 2 [ISBN:9780198515982]

• Clemens Berger, Victor Iwaniack: On the profinite fundamental group of a connected Grothendieck topos [arXiv:2304.05338]