Snowglobe Models
Posted by John Baez
Last week in my course on Classical vs Quantum Computation, James Dolan said a bit about funny nonstandard models of typed λ-theories — like the typed λ-theory for high school calculus. He calls these ‘snowglobe models’, because they live ‘inside’ the usual world of sets — but in their own self-contained miniature universe, like a snowglobe:
I’d like to talk about these a bit before I forget!
Lately in my course I’ve been focusing on ‘classical’ computation, hence closed monoidal categories where the tensor product is the cartesian product. However, the idea of a snowglobe model is more general, so let me talk about it more generally.
Suppose is a closed symmetric monoidal category, as defined here. Very roughly, this a category where any two objects and have a tensor product and also an ‘object of maps’ from to , denoted . The latter should not be confused with the usual set of morphisms ! It’s often called the ‘internal hom’, since it lives inside .
We can think of as a theory. A model of this theory in some other closed monoidal category is a functor
preserving all the relevant structure. Namely:
- The functor must be symmetric monoidal, as defined here. Very roughly, this means preserves tensor products.
- The functor must be closed, meaning that for any pair of objects , the god-given morphism is an isomorphism.
Now, suppose we have a functor
which is symmetric monoidal but not closed. We can think of this as a defective model — but it gives a perfectly fine ‘snowglobe model’ in some other category!
Here’s how.
First, let’s form a kind of ‘hybrid’ of and , having objects of as its objects, but the objects as its ‘hom-objects’.
This hybrid — let’s call it — does not begin life as a category, because instead of a set of morphisms from to , it just has an object in , namely . It’s what people call a category enriched over , as defined here.
The terminology is a little confusing to beginners: it’s important to realize that a ‘category enriched over ’ is not an actual category. But, just as Pinocchio, who began life as a puppet, eventually became a real boy, can with sufficient effort become a real category!
To do it, for each pair of objects we define a morphism to be a morphism in from (the unit object of ) to . This sometimes called a point of the hom-object . These points form an actual set, and with some work becomes an actual category.
In fact, now that is a category, it even becomes a closed symmetric monoidal category in an obvious way!
I know what some of you are thinking:
I felt like that too, the first time Jim showed me this sort of construction a few years ago. But really, once you grok the definitions, the construction is not hard! (Unless, of course, I’m making some mistake.) This is part of the fun of category theory — it gives your brain a real workout, but in the end it all seems perfectly obvious.
Anyway: now our original functor
factors into a first stage
and a second stage
And, is a closed symmetric monoidal functor! This is more or less by construction. preserves the tensor product because did. But, also preserves the internal hom, because the internal hom in is borrowed from .
So,
is a model of our theory : a snowglobe model. It’s called a snowglobe model because while it comes from a defective model that lives in , it really lives inside the miniature universe .
To really appreciate this construction, you need to look at some examples, like the theory of high-school calculus. But, I’m a bit too tired for that right now. For now, I just wanted to get this down in writing.
I should add for the experts that this factorization of into two stages is related to the theory of Postnikov towers, as explained in Section 3.1 here.
I’ve corrected this post thanks to comments by Robin Houston, Todd Trimble and James Dolan. Some of their comments won’t make much sense without knowing what my mistakes had been, so here they are:
- I had written in lots of places where I should have written .
-
I had defined a symmetric monoidal functor to be ‘closed’ if In fact, there’s a god-given morphism and is closed if this is invertible.
To get this god-given morphism, start with the evaluation in . Then apply : Then use the fact that preserves tensor products up to a specified isomorphism to get the morphism
Re: Snowglobe Models
This looks very interesting, but I must be missing something because it isn’t quite making sense.
The way you’ve explained it, the intermediate stage where is viewed as a -enriched category seems to be redundant. A morphism in is a point of , or in other words an arrow in !
So this factorisation is the usual factorisation of a functor into a bijection-on-objects followed by a full-and-faithful functor. But then I don’t see why is closed, unless the functor was closed in the first place, which rather defeats the object!
Any elucidation would be much appreciated.
Also, a little nit or query. You wrote
I think the definition of closed functor is actually more subtle than that: the monoidality of the functor automatically induces a natural transformation , and a (symmetric monoidal) closed functor is one for which this natural transformation is invertible. I suppose it’s possible that your condition implies mine: is that true?
(On a complete tangent, I wonder whether you could be persuaded that the linear logic-inspired notation is a much more pleasant way to denote the internal hom than , which is easily confused with Hom. Another advantage of this notation is that it is readily adapted to the non-symmetric case, where there are two internal homs, by using a left-pointing variant – with the arguments in reverse order – for one of them. (This is unfortunately harder to do on the web, because the left-pointing version doesn’t have a Unicode codepoint. It’s easy in Latex, by rotating or reflecting the right-pointing one.))