nLab partial map 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.

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

As a higher inductive-inductive type

Given a type TT, the partial function classifier T T_\bot is inductively generated by

  • a function inj:TT inj:T \to T_\bot
  • a term :T \bot:T_\bot
  • a function n:()(n):(T)T\Vee_{n:\mathbb{N}} (-)(n): (\mathbb{N} \to T) \to T

and the partial order type family \leq is simultaneously inductively generated by

  • a family of dependent terms

    a:T,b:Tπ(a,b):isProp(ab)a:T, b:T \vdash \pi(a,b):isProp(a \leq b)

    representing that each type aba \leq b is a proposition.

  • a family of dependent terms

    a:Tρ(a):aaa:T \vdash \rho(a):a \leq a

    representing the reflexive property of \leq.

  • a family of dependent terms

    a:T,b:T,c:Tτ(a,b,c):(ab)×(bc)(ac)a:T, b:T, c:T \vdash \tau(a, b, c):(a \leq b) \times (b \leq c) \to (a \leq c)

    representing the transitive property of \leq.

  • a family of dependent terms

    a:T,b:Tσ(a,b):(ab)×(ba)(a=b)a:T, b:T \vdash \sigma(a, b):(a \leq b) \times (b \leq a) \to (a = b)

    representing the anti-symmetric property of \leq.

  • a family of dependent terms

    a:Pt(a):aa:P \vdash t(a):\bot \leq a

    representing that \bot is initial in the poset.

  • a family of dependent terms

    n:,s:Ti(n,s):s(n) n:s(n)n:\mathbb{N}, s:\mathbb{N} \to T \vdash i(n, s):s(n) \leq \Vee_{n:\mathbb{N}} s(n)
  • a family of dependent terms

    x:Σ,s:Σi(s,x):( n:(s(n)x))( n:s(n)x)x:\Sigma, s:\mathbb{N} \to \Sigma \vdash i(s, x):\left(\prod_{n:\mathbb{N}}(s(n) \leq x)\right) \to \left(\Vee_{n:\mathbb{N}} s(n) \leq x\right)

representing that denumerable/countable joins exist in the poset.

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.

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

For partial function classifiers in homotopy type theory:

  • Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type (abs:1610.09254)

  • Martín Escardó, Cory Knapp, Partial Elements and Recursion via Dominances in Univalent Type Theory (pdf)

Discussion for topological spaces:

Last revised on June 20, 2022 at 07:32:17. See the history of this page for a list of all contributions to it.