The Covariance of Coloured Balls
Posted by David Corfield
When you reach over 150 messages in response to a post, it’s probably time to start a new one, especially for those with inefficient browsers. In this post I want to see if I can make sense of discussions we were having there about general relativity, covariance, groupoids and sameness in a much more intuitively clear setting, though perhaps it will introduce its own problems.
OK, so say I have a set, , of 5 indiscernible balls in a box, each of which can be coloured in 3 ways. Then I might take the state space to be , of cardinality 243. But perhaps while doing physics on these balls, I come to see that nothing about them matters aside from their colour. Since I can’t tell the difference between any two versions of 2 reds, 2 greens and a blue, I decide to reduce my state space to , a set of equivalence classes of cardinality 21.
However, after a time this starts to strike me as odd. I have represented the fact that any colouring of 2 reds, 2 greens and a blue are equal, and yet were someone to swap a green and a red I’d notice in a way that I wouldn’t notice a swap of two reds. Any swaps in a state of 5 red balls would also go unnoticed. At the very least, there seems to be a difference between a monochrome state and a tricoloured state.
So I decide to change my state space to the action groupoid . This has 21 connected components, but an object in the all red component has 120 automorphisms, where an object in the 2 reds, 2 greens and a blue component has 4 automorphisms. The groupoid as a whole has cardinality 243/120.
Hopefully the analogy with general covariance, where we consider , is clear. So what is it legitimate to ask, and what illegitimate?
Well, I shouldn’t ask how many worlds there are. Nor should I ask how many worlds there are in which there are 2 reds, 2 greens and a blue, but I can ask how many automorphisms there are on that world. I can also ask how many distinguishable kinds of world there are (21).
Can I even ask how many balls there are? If I model the space of balls as , then ‘No’, all I have is its cardinality, 1/24.
On the other hand, so long as I know the symmetry group, I can reconstruct the number of balls. This is reflected by the magic of dependent type theory.
denotes a dependent type, which we interpret externally as the balls with the action of their symmetry group. Now I can ask things like “-equivariantly, is a set, and if so what cardinality does it have?”, and be told “Yes, 5.”
So you hand me a groupoid and I may be able to reconstruct it as an action groupoid of a group acting on a set, but I won’t be able to do this uniquely. I can’t tell the difference between and . If you tell me that every object I see has a double residing within it, which is identical to it in a canonical way, I should say that’s equivalent to my ordinary view of the world. However, once we agree on the action group, you can say things like “-equivariantly there are two cups in front of me.” But I shouldn’t ask you “Which is in front of you now?”
In the analogy between the coloured balls and the case of general covariance, something like the following seems to be going on. I see two reds, two greens and a blue. I agree there’s no difference between this and the situation where the two reds are swapped. Since I can’t tell the difference, I take the two cases to represent the same state of affairs. However, once I’ve done this, I seem to have given up any way of conceiving of there to be 5 balls. Hopefully, we can agree, that via the action groupoid understood in a certain equivariant context, we can still say there are 5 balls, while agreeing that we can’t tell the two coloured worlds apart.
Re: The Covariance of Coloured Balls
This is a very nice way of thinking about it.
I do think we shouldn’t use the same letter for the set of balls, for a variable of type , and for the type in that context whose fiber is the set of balls. It’s even worse because we’re using for delooping! So despite the fact that “balls” begins with B, I suggest using a different letter like for the set of balls. Then the set is acted on by the group :
and this action can be encoded by a dependent type
with the property that , where is the canonical basepoint.
Now it’s true that if we define to be the image of , i.e.
then its canonical basepoint is and the dependent type is . So if we decided not to notate the second components of elements of this image (which is not unreasonable, since they are hprops), then would be the identity and the basepoint would be ; thus we would write
and upon substituting for we would get as the fiber over the basepoint . However, one might argue that this is more confusing rather than less.
What we shouldn’t do is use the same letter for the fixed set and for a variable of type . Indeed, the whole point is that is defined over that whole type rather than just at the basepoint, and that definition encodes the action of on .
The intuition does argue for using the same letter for and for , since is “ equipped with its action by ”. That seems okay as long as we find a way to notate the dependence on , such as writing
so that we could then say (or, I suppose, ; ugh). It may also be tempting to write for , but properly that notation belongs rather to the dependent sum , so I think that confusion could arise there as well.