nLab
decidable object

Contents

Context

Category theory

Constructivism, Realizability, Computability

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 separable, respectively unramified object, as pointed out by William Lawvere.

Definition

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

Δ X:XX×X \Delta_X \;\colon\; X \longrightarrow X \times X

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

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

Remarks

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

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

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

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

Examples

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.

Last revised on July 15, 2019 at 06:50:20. See the history of this page for a list of all contributions to it.