nLab decidable injection



In classical mathematics, a subsingleton could either be defined as

  • a set SS such that for all elements aSa \in S and bSb \in S, a=ba = b

  • a set SS which is either empty or a singleton.

However, in constructive mathematics, the two notions of subsingleton above are no longer the same, because the axiom of excluded middle no longer holds true. Instead, one usually defines a subsingleton as the first definition, and the second definition is then referred to as about decidable subsingletons.

Similarly, in classical mathematics, an injection between two sets AA and BB is then a function f:ABf:A \to B such that for all elements bBb \in B, the preimage or fiber of ff at bb is a subsingleton. However, in constructive mathematics, there are two notions of injections, resulting from the two notions of subsingletons:

Set of decidable injections

Suppose the set theory has function sets B AB^A. Then one could define the set of decidable injections from AA to BB as the set

Inj d(A,B){fB A|bB.(! *(b))(¬ *(b))}\mathrm{Inj}_d(A, B) \coloneqq \{f \in B^A \vert \forall b \in B.(\exists!a \in A.a \in f^*(b)) \vee (\neg \exists a \in A.a \in f^*(b))\}

where f *(b)f^*(b) is the preimage or fiber of ff at bb.

Last revised on August 2, 2023 at 19:03:16. See the history of this page for a list of all contributions to it.