Partial map classifiers and restriction classifiers
Robin Cockett Dept. Compuer Science University of Calgary Calgary, Alberta CANADA
Sydney category seminar: 27 May 1998
This talk describes work in progress with Steve Lack
Abstract:
Continuing from last week , for restriction categories, we discuss two questions:
- When the category of total maps extensive?
- When does the total map category have a partial map classifier?
The answer to the former question gives an alternative way of establishing that the "copy completion" Cp(X) of a distributive copy category X with a zero is (distributive) extensive . The answer to the latter question will allows us to anwer the question of when a monad is "morally" a partial map classifier (next talk!)
Summary:
More on categories with restriction:
Recall a category X has a restriction if to each f: A -> B there is an associated idempotent {f}:A -> A which satisfies five conditions:
- {f};f = f
- {f};{g} = {g};{f}
- {f;g} = {f;{g}}
- {{f};g} = {f};{g}
- f;{g} = {f;g};f
- 0-cells: categories with a split restriction
- 1-cells: functors which preserve restrictions, that is {F f} = F{f}.
- 2-cells: natural transformations whose components are total.
- 0-cells: a category X together with a stable system of monics M
- 1-cells: functors which preserve the systems of monics and pullbacks along these monics (that is M-stable).
- 2-cells: natural transformations who naturallity squares at M-maps are pullbacks (that is M-cartesian).
A restriction is split if all the idempotents of the form {f} split. A map in a category with a restriction is total in case {f} = 1. The total maps form a subcategory which includes all the monics.
Last time I ended by claiming:
Theorem: MCat is isomorphic to rCat.
Where rCat is defined to be:
and MCat is defined to be the 2-category:
The less obvious aspect of this is how one gets from a category with a restriction to a category with a stable system of monics.
By a stable system of monics I mean a class of monics M containing all isomorphisms, closed to composition, and such that the pullback of a monic in M along any map not only exists but is itself a monic in M.
(Note: any such system of monics also has the property of being "left factor closed," that is if the composite m;m' is in M and m' is in M then m is in M.)
Under the isomorphism of the theorem a split restriction category X is carried to its category of total maps Total(X) in which the monics which split the restrictions are identified as the M maps. Clearly this class contains all isomorphisms but also it is closed to composition as the argument below shows:
Let m: A -> B and m': B -> C have retractions r and r' with r;m ={r;m} and r';m'={r';m'} then m;m' has retraction r';r and we have:
r';r;m;m' = r';{r;m};m' = {r';r;m};r';m' = {r';r;m};{r';m'} = {{r';r;m};{r';m'}} = {r';r;m;m'}.
So what remains is to establish that pullbacks of an M-map along any total map f exists and is itself an M-map. So suppose k ; m = h ; f is a commuting square of total maps with m in M, a splitting of e = {e} = r;m, then we must produce a pullback. We do this by splitting {f;e} = r';m' on the domain of f. This gives a square
m' ; f = (m';f;r) ; m ----- top map is m';f;r
which commutes as
m';f;r;m = m';f;{e} = m';{f;e};f = m';f
and all maps are total as m',f, and m are total and any left factor of a total map whose right factor is total (e,g. the map m';f;m!) is total. Finally to show that this is a pullback, as the vertical arrows are monic, it suffices to show that h factors through m'. But here it suffices to show h;{f;e} = h:
h;{f;e} = {h;f;e};h = {k;m;e};h = {k;m};h = h
where we use for the last two steps m;e = 1 and k;m is total.
This shows that (Total(X) ,M) with the monics which split restrictions in X is an object in MCat. It is straigtforward to show that the partial map category built from (Total(X) ,M) is then just X.
When is Total(X) extensive?
- z_A: 0 -> A is total.
- cD: A+A -> A is total.
- {f+g} = {f}+{g}
- 0 is a final object.
- 0:A -> A has {0} = 0.
- Coproduct embeddings split restrictions
- The coproduct embedding natural transformations are cartesian in Total(X).
- e1;e2 = 0 (disjoint)
- there is an h: A -> A+A such that
- h:cD = {h}
- h; e1+e2 = h
- <e1 | e2>;h = e1 + e2
- X has restriction coproducts
- X has a restriction zero
- Whenever (e1,e2:A) is a decomposition of A and f:A' -> A is a map then ({f;e1},{f;e2}:A') is a decomposition of A'.
If X is a category with a split restriction, we may ask when the corresponding pair (Total(X),M) has Total(X) extensive and has M contain all the coproduct embeddings. An immediate consequence of the classification theorem is that such an X will then have coproducts (with embeddings and codiagonal total etc.) and a zero. However, we do have to work a little harder to obtain a precise characterization (in fact we did not obtain it until just before I was due to give the talk!).
A restriction category has "restriction" coproducts in case as a 0-cell in rCat it has coproducts (i.e the diagonal functor has a left adjoint). Spelling this out this is the demand that:
It follows from these requirements that the coproduct embeddings b0; A-> A +B and b1: B -> A +B are also total. Next we demand that the category has a "restriction zero", that is
Now given these conditions we already have a surprising number of extensive features:
Lemma: If X is a restriction category with restriction coproducts and a restriction zero
This is because a coproduct embedding is essentially 1 + z_B: A + 0 -> A+B but tthis splits 1+0: A + B -> A+ B where {1+0} = {1}+{0} = 1+0. To show that the coproduct embedding is cartesian amounts to showing that the square
f +0 ; 1_A' + z_B' = 1_A + z_B ; f+g
is a pullback. But this amounts to showing that 1_A + z_B splits {f+g;1+0}. But now we have
{f+g;1+0} = {f+0} = {f}+{0} = 1+0
(the last step as f is total) which certainly has the right splitting!
The extensive property which remains to be captured is that the pullback of coproduct embeddings along any map gives a pair of coproduct embeddings. To do this we need a definition. We shall for the remainder of this section be working in categories with a restriction, restriction coproducts and a restriction zero:
Definition: In a category as above (e1,e2:A) is a decomposition of A in case:
We shall say a decomposition is split in case e1, e2, and {h} split.
Although not stated in the definition the map h: A -> A+A is uniquely determined by the conditions. We now have the observation:
Lemma: In X a category with restriction satisfying the above (e1,e2:A) is a split decomposition if and only if
A1 >-m1'-> A'<-m2'-< A2
is a coproduct where r1;m1 = e1, r2;m2 = e2, r;m = {r;m} and m1';m = m1, m2';m = m2.
The proof is not hard but takes some bashing out!
Now it makes sense to say that a category with restriction is an extensive restriction category in case :
It is useful to observe that if X is an extensive restriction category then Kr(X), the category obtained from X by spliting the restrictions, is also an extensive restriction category.
We now claim the following:
Theorem: (Total(Kr(X)),M) is extensive with all coproduct embeddings in M if and only if X is an extensive restriction category.
Note that an extensive restriction category X need not have Total(X) extensive simply because it does not have enough pullbacks, however, the point is it is morally extensive!
Restriction classifiers ....
- There is an n: A -> HA such that n;e = 1 and e;n = {e}
- Given any f: A' -> A there is a unique total map [f]: A' -> H(A) with [f];e = f.
- (H,e,d) is a comonad on X
- The underlying functor from the kliesli category U: X_H -> X factors through the subcategory of total maps as a full and faithful subcategory X_H -> Total(X) -> X.
- (H,n,mu) is a monad on Total(X).
- (KrH(H),n,mu) is an M-partial map classifier on Total(KrH(X)).
Clearly one cannot discuss categories of maps without at some stage talking about partial map classifiers. In this section we shall address the question from the other end: that is what does a partial map classifier look like on the category of partial maps. Well, of course, rather than talking about a category of partial maps, as such, we shall consider a restriction category. The structure we obtain is what I shall call a "restriction classifier":
A category with a restriction has a restriction classifier if for each object A there is a map e: H(A) -> A such that:
Iti is worth noting that if X has a restriction classifier then KrH(X) will also. If q={q} is a restriction idempotent on A then H(e) is an idempotent (although not a restriction idempotent) on H(A) the splitting of this idempotent provides H(q). Thus, here to maintain the structure we must enlarge the class of idempotents we split so that H remains a functor.
It is now a rather enjoyable exercise to show that in fact this defines a comonad (H,e,d) on X where we set H(f) = [e;f] and d = [1_H(A)]. Furthermore, the Kliesli category is isomorphic to the full subcategory of Total(X) determined by the objects of the form H(A).
However, there is more. For while n: A -> H(A) is not natural for all maps in X it is natural for the total maps and, in fact, on the total map category this produces a monad (the multiplication is none other than H(e)). When restrictions split this is exactly a partial map classifier for the M-maps.
Theorem: If X a restriction category with a restriction classifier
What are examples of categories with a restriction classifier?
(1) The partial maps of a topos - indeed partial maps with domain any class which can be classified such (in suitable recursive topoi) as the recurively enumerable maps.
(2) The partial maps in an extensive category with a decidable (=recursive) domains.
(3) The kliesli category of the exception monad on any distributive category. This is where the extensive completion enters the story!
(4) The kliesli category of any "classifying" monad (see next time!)
Remark: A cartesian closed category with a partial map classifier (for all partial maps) is essentially a topos (here no mention of pullbacks). We should therefore be able to turn this round into a more precise statement: a monoidal closed copy category X in which all monics are sections for restrictions which has a restriction classifier has Total(Kr(X)) a topos. The point here is that our primarily concerned is not with this extreme case but rather with the case when the classified monics are a proper subclass of the class of all monics.
Is there more?
We hope so!
One obvious thing to answer is when does a monad on a category give as its Kliesli category a category with a restriction ... and when does the monad become a restriction classifier when viewed from the "other end"? I called it a classifying monad above ... and how do they arise anyway!
We hope to begin answer this next lecture!
... and there is more!
Other talks by the same speaker.
Back to titles of seminars.
Steve Lack Last modified: Mon Jun 1 09:49:48 EST 1998