Characterizing partial map classifiers
J.R.B. Cockett Dept. Computer Science University of Calgary Calgary, Alberta CANADA
Sydney category seminar: 10 June 1998
This talk describes work in progress with Steve Lack
Abstract:
When is a monad on a category a partial map classifier? More generally when does a monad have a Keisli category which is a restriction category with (the induced comonad) a restriction classifier?
The latter question, it turns out, is easier to answer given the work we have already done. Furthermore we can describe this in purely algebraic terms as structure on the monad. Such a monad I call a classifying monad. When we start with a cartesian category (i.e. category with products) this structure amounts to a monoidal monad for which the copy map (or diagonal) is monoidal satisfying one other condition:
D; \eta \ox H(!); m ;H(u^R) = H(\eta).
This is what I called a classifying copy monad.
This means that in a category with products it is possible to say quite formally what a partial map classifier is without ever mentioning any limits!! This is a rather amazing fact and it can be used to great effect to produce settings with limit properties from ones with virtually no limits.
However, this still does not answer the question of when a monad actually is a partial map classifier: this I call an effective classifying monad. Here there are two rather different answers: the first comes directly from the above where we have to specify which limits must exist. What is striking here is the minimal limit requirements! There is also a different view of a partial map classifier as a monad whose unit is an exponentiable map and this gives rise to a rather different approach to characterizing these monads (which is not discussed here).
Summary:
Partial map classifiers by monadic reflection:
- {f};f = f
- {f};{g} = {g};{f}
- {f;g} = {f;{g}}
- {{f};g} = {f};{g}
- f;{g} = {f;g};f
- {f};T(f);\mu = f
- {{f};T(g);\mu} = {f};T({g});\mu = {g};T({f});\mu
- {f;T(g);\mu} = {f;T({g});\mu}
- f;T({g});\mu = {f;T(g);\mu};T(f);\mu
- {1_T(A)} = T(\eta)
- {f;\eta} = \eta
- At each A there is a monic \eta_A with \eta_A;\epsilon_A = 1 and {\epsilon_A} = \epsilon_A;\eta_A.
- \eta_H(A);H(\epsilon_A) = 1
- {H(f)} = 1 for all f, that is H(f) is total
- The family of maps \eta is natural for the total maps: {f} = 1 implies f;\eta = \eta;H(f).
Recall that a category X has a restriction in case to each f:A -> B there is an associated {f}: A -> A satisfying five conditions:
Such a category has a classified restriction if the inclusion of the total maps (that is those with {f}=1) has a right adjoint H: X -> Total(X) whose counit \epsilon is a retraction of a restriction (n.b. this actually means there is an \eta with \eta;\epsilon =1 and \epsilon;\eta = {\epsilon}). This structure when it exists is, upto equivalence, unique. The main observation was that when we split all restriction idempotents e (and all idempotents H^n(e) -- to ensure H remains a functor) then the induced monad on Total(KrH(X)) is a partial map classifier.
One may wonder whether one can repeat the process by doing another "monadic reflection" in order to get something new: that is take the Kleisli category of this partial map classifier in order to obtain a new restriction category and whence a new category of total maps. However, the first step simply recovers KrH(X) (and whence the next step recovers Total(KrH(X)) ) so the process stops.
We wish to answer the question of when a monad has a Kleisli category with a classified restriction: in this endeavour we may start more modestly by answering the simpler question of when a monad gives rise, on its Kleisli category, to a restriction.
Defn. A restriction monad is a monad T = (T,\eta,\mu) together with a restriction structure, that is a functional which carries f:A -> T(B) to {f}: A -> T(A) satisfying the following five (expected) properties:
Now these requirements are exactly the statement that on the Kleisli category there is a restriction so that the following is just a tautology:
Prop: The Kleilsi category X^T has a restriction if and only if T has a restriction structure.
If X were a total copy category then we can create a functional on a monoidal monad by the following:
{A -f-> T(B) } = A -D-> A \ox A -f \ox \eta-> T(B) \ox T(A)
-T(!) \ox 1-> T(I) \ox T(A) -m-> T(I \ox A) -T(u)-> T(A)
this is a resriction precisely when T is a copy monad, that is a monoidal monad with the additional requirement that
T(D);m = D
this gives:
Prop: On any total copy category every copy monad is a restriction monad.
In fact, if we require the copy structure to lift to the Kleisli category and the restriction to be given by the copy structure (all afterall natural requirements) then this amounts to the requirement that T be a copy monad.
We may next describe what must be the case in order that the Keisli category have a classified restriction.
Defn. A restriction monad is said to be a classifying monad in case it satisfies the following additional requirements:
We have the following crucial technical lemma:
Lemma: For any classifying monad {f} = \eta implies f;T(\eta) = f;\eta.
Proof:
f;T(\eta) = f;{1_T(A)};\eta;\mu = f;\eta;T({1_TA)});\mu = {f;\eta;T({1_TA)});\mu};T(f;\eta);\mu = {f};T(f;\eta);\mu = \eta;T(f;\eta);\mu = f\;eta.
Now we may prove:
Prop: X^T is a restriction category with its induced comonad a restriction classifier if and only if T is a classifying monad.
To establish this it is useful to have the following description of a comonad which is a restriction classifier:
Prop: If X is a category with a restriction then a comonad H = (H,\epsilon,\delta) is a restriction classifier if and only if
The proof now relies on the following observations: we secure the properties of the Kleisli category by noting that {1} = T(\eta) is essentially the first requirement above. The second requirement above is just a triangle identity of the adjunction between X and X_T. The third requirement is provided by {f;\eta} = \eta. The final requirement is given by the lemma.
In the copy category world we can now observe that a monad on a cartesian category gives rise to a classified copy category (with lifted structure) if and only if T is a classifying copy monad, that is a copy monad which in addition satisfies the "classifying identity":
D; \eta \ox T(!); m ;T(u^R) = T(\eta).
Prop: If X is cartesian (i.e. has products) X^T is a copy category with induced copy structure and classifying comonad if and only if T is a classifying copy monad.
To establish this we observe that the requirement {1} = T(\eta) is exactly the meaning of the classifying identity above and a short diagram chase shows that the second requirement is already true in this setting.
In all the above cases X will have a faithful functor into Total(KrT(X^T)) which preserves the monad so that the monad T becomes a partial map classifier in Total(KrT(X)).
Notice that starting with X and a classifying monad T we have passed to the Kleisli category X^T. We have then split certain idempotents (basically the restrictions and those required to keep T a functor) then we have passed back to Total(KrT(X)). This last passage can be viewed as taking the Eilenberg-Moore coalgebras of the comonad. This follows from the following general fact:
Prop: If T =(T,\eta,\mu) is a monad on X then \eta is the equalizer of \eta and T(\eta) if and only if F_T: X -> X_T is comonadic.
Now considering a restriction classifier H, KrT(X) is the Kleisli category of the partial map classifier nduced by H on Total(KrT(X)). Now any partial map classifier has its unit cartesian so that the condition of the proposition is satisfied. Thus, we have:
Corollary: If X has a classified restriction then F_H -| U_H: KrH(X) -> Total(KrH(X)) is comonadic.
Thus, we may take the attitude that we are basically doing a monadic reflection in order to "complete" the initial category. Of course there are two rather non-trivial twists to this fundamental process: first we are doing alternately Kleisli then coEilenberg-Moore and second we do some idempotent splitting in between these steps.
When is T-restriction-splitting monadic reflection stationary?
- \eta: A -> TA equalizes \eta, and T(\eta): TA -> TTA
- There is a map r_f: R_f -> A such that T(r_f) is the equalizer of T({f});\mu , 1: TA -> TA.
It is worth remarking that the inclusion of X into Total(KrT(X^T)) is only faithful: it may not be full. An example of when it is not full is given by the extensive completion of a distributive category: a distributive lattice has the final category as its extensive completion. Furthermore, almost certainly, as we are adding pullbacks, it will not be an isomorphism of categories.
Observe, however, that if we answer the question of when this inclusion is an isomporphism of categories that we will also have answered the question of when a monad is a partial map classifier.
Defn. A classifying monad T on any category X is said to be an effective classifying monad in case:
It actually follows (using just the first equalizer and the properties of T(r_f)) that r_f must is the equalizer of {f} and \eta. The result then is that:
Prop: X is equivalent to Total(KrT(X^T)) if and only if T is an effective classifying monad.
In the copy category situation this gives a characterization as well where here we may speak of an effective classifying copy monad.
We note that the first condition is implied by the requirement that \eta be cartesian the second condition, however, is more opaque!
Partial map classification as a composable posetal exponad:
- \eta: A -> HA is a cartesian monic natural transformation
- That every \eta_A is exponentiable in the slice over TA and furthermore at x: X -> TA the exponential has a very particular form namely H(\eta*(x)) with evaluation given by x*(\eta).
- That the monad be pointed that is the square (!!) \eta;eta ; \mu = 1 ; \eta is a pullback(this is a rather collapsed version of composable!)
An alternative view of a partial map classifier in the presence of a final object is that the M-subobject fibration is represented by an internal full subcategory given by the exponentiable map \eta_1. This means that we may view the partial map functor an exponad (or a partial product functor). In the absence of a final object each \eta must still be exponentiable and the exponentials must be as if they are derived from an exponad that is they must fit together well. Finally the internal category must have some internal cocompleteness properties which externally means that the classified monics compose.
Thus we are required to specify three bits of structure:
It is useful to introduce some terminology: we shall call a category with a stable system of monics which are classified (by a partial map classifier) a Mulry category (Phil studied partial map classifiers in his thesis).
Steve Lack devised a slick way of specifying thes conditions for he noticed that for each A in X we are guaranteed that \eta*_B: X/T(B) -> X/B has a right adjoint given by T_B (where T_B(x) = T(x) ) which makes X/B a reflexive subcategory of X/T(B).
Prop: X is a Mulry category if and only if there is a pointed monad (T,\eta,mu) with \eta cartesian and such that all pullbacks along each \eta_A exist and \eta*_B -| T_B is a reflexion for each B.
In the case when X is cartesian we can replace both the last two requirement (i.e that the monad be pointed and tha\eta*_B -| T_B be a reflexion) by the requirement that T be a classifying copy monad. this gives:
Prop: X is a Mulry category with products if and only if X has a classifying copy monad (T,\eta,\mu) for which pullbacks along all \eta_A exist, \eta is cartesian, and T preserves this data.
Finally we may sum up with:
Theorem: The following are equivalent
X is a Mulry category.
X has a effective classifying monad
X has a pointed monad (T,\eta,\mu) in which \eta is cartesian, pullbacks along each \eta_B and \eta^*_B -| T_B a reflexion.
Notes:
The third part of this theorem is very similar to a characterization given by Anna Buclao and Guieppe Rosolini. They considered the case of categories with a final object. They also gave a version of the result for cartesian categories which is a little weaker than the one given here - they required T to preserve more pullbacks and \mu to be cartesian. This result was also one of the "copy category" results in my unpublished manuscript on these categories which predated that paper by a few years ... however, I never published it as I was not sure whether it was a new result!
The second characterization (which is also essentially in the copy category manuscript) appears to be new. The completely limit free notion of a classifying is also new and was the one of the main objectives of the copy category manuscript.
Is there more?
Yes ... now we have understood this characterization we can actually use it! In particular, we are interested in functorial structure which has distributions over the subobject classifier and other nice limit properties .... and we are interested in iunderstanding how we can build this up in a limit free way.
Other talks by the same speaker.
Back to titles of seminars.
Steve Lack Last modified: Tue Jun 16 10:49:42 EST 1998