nLab
partial map classifier

Partial map classifier

Partial map classifier

Idea

A partial function f:ABf:A\rightharpoonup B between two sets can be turned into a total function f¯:AB \overline{f}:A\to B_\bot by adding a new element \bot to BB and sending all aAa\in A that are not in the domain of definition of ff to this new value \bot = “undefined” and the rest just to their value under ff. Conversely, every function with codomain B B_\bot corresponds to a unique partial function to BB whence B B_\bot is a ‘classifying object’ for these.

More generally, a partial map classifier of an object BB in a category 𝒞\mathcal{C} is a representing object for partial maps with codomain BB.

Definition

Let 𝒞\mathcal{C} be a category with pullbacks. Recall that a partial map ABA \rightharpoonup B in 𝒞\mathcal{C} is a span ADBA \leftarrow D \to B in which the map DAD\to A is a monomorphism. The subobject DAD \hookrightarrow A is called the domain of the partial map. Two partial maps are considered equal if they are related by an isomorphism of spans; in this way we obtain a set of partial maps Par 𝒞(A,B)Par_{\mathcal{C}}(A,B).

We can compose a partial map ABA\rightharpoonup B with a map BBB\to B' in an obvious way. We can also compose it with a map AAA'\to A by pulling back the mono DAD\hookrightarrow A to AA'. In this way Par 𝒞(,)Par_{\mathcal{C}}(-,-) becomes a profunctor from 𝒞\mathcal{C} to itself. (In fact, it is the hom-set of another category with the same objects as 𝒞\mathcal{C}.)

A partial map classifier for BB is an object B B_\bot together with an isomorphism

𝒞(A,B )Par 𝒞(A,B) \mathcal{C}(A,B_\bot) \cong Par_{\mathcal{C}}(A,B)

natural in AA. By the Yoneda lemma this means there is a universal partial map B BB_\bot \rightharpoonup B.

The existence of partial map classifiers B B_\bot for all objects BB in 𝒞\mathcal{C} amounts to the existence of a right adjoint for the inclusion 𝒞Par(𝒞)\mathcal{C}\hookrightarrow Par(\mathcal{C}) where the latter is the usual category of partial maps of 𝒞\mathcal{C}.

Constructions

In a Boolean extensive category (such as a Boolean topos), we can define the partial map classifier as B =B+1B_\bot = B + 1, where 11 is the terminal object. This is because in an extensive category, a map AB+1A\to B+1 is equivalent to a decomposition of AA as a coproduct D+ED+E together with a map DBD\to B (the map E1E\to 1 being unique), and in a Boolean category every subobject of AA is complemented and hence induces such a coproduct decomposition. The universal partial map B+1BB+1 \rightharpoonup B has domain the summand BB, on which it is the identity. Note that BB+1B\mapsto B+1 is also known as the maybe monad.

Partial map classifiers also exist in every elementary topos, but in the non-Boolean case they are harder to construct. In the internal logic, B B_\bot can be defined in two ways:

  • B B_\bot is a subobject of the power object 𝒫B\mathcal{P}B consisting of the subsingleton subobjects of BB. In this case, the universal partial map B BB_\bot \rightharpoonup B has domain the set of singleton subobjects of BB, on which it is an isomorphism.

  • B B_\bot is the object of partial maps 1B1 \rightharpoonup B. In this case, the universal partial map B BB_\bot \rightharpoonup B has domain the set of partial maps which are total, on which it is an isomorphism.

Note that neither of these constructions is predicative. The second makes more sense in a higher category (or in its internal logic such as homotopy type theory).

Remark

In an intuitionistic context, B+1B + 1 still classifies something: namely partial maps ABA \rightharpoonup B whose domain of definition is a decidable subobject of AA.

In type theory one uses the partiality monad to treat general recursion as an algebraic effect. In this we we obtain a classifier for recursively enumerable subsets. Is this the first appearance? It is clear that this idea can be generalized to other classes of propositions.

Properties

  • In a topos, the partial map classifier B B_\bot of BB is injective. The canonical embedding BB B\rightarrowtail B_\bot shows accordingly that a topos has enough injectives!

  • In a topos, the subobject classifier true:1Ωtrue:1\rightarrow\Omega coincides with the monomorphism η 1:11 \eta_1:1\rightarrowtail 1_\bot.

  • In a topos, the assignment of B B_\bot to BB is functorial.

References

  • F. Borceux, Handbook of Categorical Algebra - vol. 3 , Cambridge UP 1994. (sec.5.5)

Section 1.2 of

  • Peter Johnstone, Topos theory, London Math. Soc. Monographs 10, Acad. Press 1977, xxiii+367 pp. (Dover reprint 2014)

A2.4 of the Elephant

Last revised on July 3, 2015 at 07:03:45. See the history of this page for a list of all contributions to it.