constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
An object $X$ of a coherent category $\mathcal{C}$ is called decidable if its equality relation (i.e. its diagonal morphism)
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$.
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$.
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.
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.
Last revised on July 31, 2023 at 12:57:55. See the history of this page for a list of all contributions to it.