nLab partial map classifier

Redirected from "partial function classifier".
Contents

Contents

Idea

A partial function f:ABf \colon A\rightharpoonup B between two sets can be turned into a total function f¯:AB \overline{f} \colon A\to B_\bot by adjoining a further 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 function classifier or 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.

This can be unpacked into the following condition:

Proposition

A partial map classifier for BB is uniquely determined by a map BB B \to B_\bot with the property that, for every partial map ABA\rightharpoonup B depicted below, there is a unique AB A \to B_\bot making a pullback square

Proof

For any monomorphism BB B \to B_\bot, there is a natural transformation 𝒞(,B )Par 𝒞(,B)\mathcal{C}(-,B_\bot) \to Par_{\mathcal{C}}(-,B) given by forming pullbacks along BB B \to B_\bot. It is a natural bijection iff it satisfies the condition of the proposition.

If BB B \to B_\bot satisfies the condition of the proposition, then it is a monomorphism, by considering the (total) partial map id B\id_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. Letting t:1Ωt : 1 \to \Omega denote the top element, the dependent product t *(B)t_*(B) is precisely the map B ΩB_\bot \to \Omega classifying BB B \subseteq B_\bot. To wit, with this definition,

𝒞(A,B ) p:AΩ𝒞/Ω(p,t *(B)) p:AΩ𝒞(t *(p),B) AA𝒞(A,B) Par 𝒞(A,B) \begin{aligned} \mathcal{C}(A, B_\bot) &\cong \coprod_{p : A \to \Omega} \mathcal{C}/\Omega(p, t_*(B)) \\&\cong \coprod_{p : A \to \Omega} \mathcal{C}(t^*(p), B) \\&\cong \coprod_{A' \subseteq A} \mathcal{C}(A', B) \\&\cong Par_{\mathcal{C}}(A, B) \end{aligned}

Alternatively, in the internal logic, two ways of defining B B_\bot that more closely follow the classical construction are:

  • 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.

Relative partial maps

Given objects p:XSp : X \to S and q:YSq : Y \to S of 𝒞/S\mathcal{C}/S, a partial map from pp to qq can be described as a commutative diagram in 𝒞\mathcal{C}.

A partial map classifier Opt S(q)Opt_S(q) for qq in 𝒞/S\mathcal{C}/S can be described as a representing object for the presheaf on 𝒞\mathcal{C} sending XX to the set of diagrams of this form (modulo choice of representatives for subobjects), together with its structure map Opt S(q)SOpt_S(q) \to S, which represents the natural transformation sending this diagram to p𝒞(X,S)p \in \mathcal{C}(X, S).

Proposition

If 𝒞\mathcal{C} is a topos and p:XSp : X \to S is an object of 𝒞/S\mathcal{C}/S, there is a pullback in 𝒞\mathcal{C}

where Opt S(q)X Opt_S(q) \to X_\bot corresponds to forgetting the base of a relative partial map, and Opt S(q)SOpt_S(q) \to S is the structure map, and Opt S(q)ΩOpt_S(q) \to \Omega corresponds to giving the domain of definition.

Proof

Let AA be an object of 𝒞\mathcal{C}. It suffices to show this square is a pullback after applying 𝒞(A,)\mathcal{C}(A, -) and the isomorphism to the presheaves these objects represent.

An object of the pullback can be described as an arrow ASA \to S, a subobject BAB \hookrightarrow A, and a partial map ABXA \hookleftarrow B' \to X with the property that the induced partial maps ABSA \hookleftarrow B \to S and ABSA \hookleftarrow B' \to S are the same partial map (up to choice of representative for the subobject).

This is bijective with the set of commutative diagrams of the form

and the projection to 𝒞(A,S)\mathcal{C}(A, S) takes the bottom horizontal arrow.

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

For related topics in homotopy type theory:

Discussion for topological spaces:

Last revised on June 13, 2023 at 16:42:33. See the history of this page for a list of all contributions to it.