A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.
To start with, what is an idempotent? The standard meaning of idempotent is a map such that , which in HoTT would mean a homotopy . A splitting of an idempotent is a pair of maps and such that and . (Note that the existence of such actually implies is idempotent, since then .)
Given an idempotent in HoTT, the obvious way to try to split it would be to take , with and . However, with this definition we cannot in general prove . Indeed, as Martin pointed out, when with the obvious proof of idempotency, for this definition to satisfy is the same as to say that is a set.
This suggests that if is not a set, then we might need some sort of coherence for the witness of idempotency. For instance, we might ask whether . And if we had a witness of that, then we could ask for that witness to satisfy some further condition, and so on off to infinity.
To see that such extra conditions are necessary, we can observe that they hold for any split idempotent. That is, suppose we have and and a homotopy , yielding as above a witness that is idempotent. Then the naturality of H implies that the coherence condition also holds, and we can continue on as far as we like.
It’s important not to read more into this observation than it says. What it says is that if a function f can be written as for functions s and r such that , then f admits a “coherent system of idempotence data”. It doesn’t say that if f is idempotent with a specified homotopy and f splits, then I must itself be coherent. Therefore:
- Even though a split idempotent automatically gives rise to an infinite system of coherence data, it doesn’t follow that in order to construct a splitting we would necessarily need to give an infinite system of coherence.
- It’s not too hard to give examples of homotopies that are not coherent, but it’s rather less obvious how to give an example of an incoherent idempotent for which there doesn’t exist some other homotopy that is coherent.
Fortunately, Jacob Lurie has already studied the analogous questions in -category theory. In Higher Algebra he showed that if a witness to idempotence satisfies the one additional coherence condition , then the idempotent f can be split, and hence admits some coherent system of idempotence data (which, apparently, may not be the same as the original one). He also gave an example of an incoherent idempotent that does not split, and hence does not admit any coherent system of idempotence data.
In the rest of this post I will describe proofs of the analogous facts in HoTT, inspired by Lurie’s categorical ones (but not quite identical to them, even under the categorical semantics of HoTT). I have verified it all in using the HoTT/Coq library; pull request is here.
Splitting coherent idempotents
Firstly, suppose we have an idempotent , with witness and single coherence . Lurie constructs a splitting as the colimit of the sequence
We could probably do the same in HoTT, using a HIT for the colimit. However, idempotents are self-dual, so we could just as well consider the limit of the sequence
and this is rather easier to work with in HoTT; it’s just
If we call this type , then we have an obvious defined by , and a slightly less obvious defined by , such that . The tricky part is proving . (Of course we need function extensionality at this point.) By definition, , so we need to show first of all that for all . We induct on . The base case is
where the middle equality is and the other two are the specified equality (part of the second component of ). The induction step is similarly
using the induction hypothesis at the end. It remains to check a naturality condition, than the composite is equal to the composite , and we can similarly do this by induction. The details are left to the reader (or you can find them in the formalization). Of course, we have to use the coherence in there somewhere. One might say that we only need one level of coherence “because” of the induction: we can apply once at each induction step and build up more and more coherence as increases.
I have not fully digested the rest of Lurie’s proof; once I got the idea of the sequential limit, I put down his book and constructed the rest of the above proof myself in “HoTT-style”. It could be that when compiled out categorically, it will yield the dual of Lurie’s proof; or it could be that they are honestly different.
An incoherent idempotent that does not split
Lurie’s example of an “irreedeemably incoherent idempotent” lives on , where is the topological unit interval (not to be confused with the HIT interval) and “Aut” denotes its group of self-homemorphisms. However, after digesting the example, I think it’s even more natural to replace the unit interval with Cantor space . In particular, the topology plays no role in the counterexample (although in constructive models does of course behave “topologically”).
By definition, in HoTT by we mean . Topologically, this is the “classifying space for fibrations with fiber “. It is connected and pointed (with basepoint ), and its loop space is the type of self-equivalences of . Thus, if is a set (such as Cantor space ), then is a , where is the (set-)group .
In particular, a map is determined essentially by a group homomorphism . This is how Lurie talks about it: in the case he defines the action of on an automorphism by if and otherwise. For , we could define an analogous by if and if . In other words, we use the fact that our space decomposes into two copies of itself, and we have our automorphism act on the first copy only.
Now, actually defining like this in HoTT would require knowing that endomaps of correspond to group endomorphisms of . The only way I can think of to do this is to construct as a HIT, show that it’s equivalent to , and then use the recursion principle of that HIT. (Is there’s another way?)
However, our definition of suggests an alternative approach. An element of is a type that is merely isomorphic to ; let’s just define (where from now on will be the Cantor space). Note that the action of this on automorphisms is, roughly, what we described explicitly above: it takes an automorphism and restricts it to act on the “first copy”. The fact that decomposes as two copies of itself, , implies that is in fact an endomorphism of , since we have (merely) . And the same fact implies that is idempotent, since . I think this is a nice example of the benefits of the univalent approach to classifying spaces!
It remains to show that is not coherently idempotent. Lurie says that if it were, then the colimit would be its splitting, and hence the map from to that colimit would be surjective on , whereas itself is certainly not surjective on and so this is impossible. In HoTT, this would requite a HIT colimit, and probably an encode-decode argument to characterize the of the colimit.
However, here again we can give a more direct argument. Suppose were coherently idempotent, so that we have and . The coherence is an equality in the type , thus it is equivalently a homotopy between two equivalences . Essentially by definition, the first equivalence (corresponding to ) decomposes the domain and codomain as and , mapping the first summand to by and the second summand to by the identity.
As for the other, if were the idempotency proof that we gave above, then the equivalence corresponding to would bracket the domain instead as and map it to by the identity on and the “fold” equivalence . Thus, the two could not possibly be homotopic, since they would send the third summand of to different summands of the codomain.
This argument doesn’t quite work as stated since might not be the same proof of idempotency that we gave above. However, whatever is, it’s defined “for all “, which by the HoTT meaning of “for all” implies that the induced equivalences must be natural with respect to automorphisms of . In particular, the equivalence induced by must be natural with respect to the “flip” automorphism . By looking at which summands are fixed by the automorphisms induced by this flip, we can conclude that must map the last two summands in the domain to the last one summand in the codomain, just as our original proof of idempotency did. Thus, our previous argument to a contradiction kicks in. Again, the details can be found in the formalization.
There are a number of further questions to ask. For instance, if we have and we use them to split , do the new witnesses induced from the splitting agree with the given ones? How many different ways can a given map “be idempotent” — can you give an example of a map that is idempotent in two genuinely different ways, perhaps with non-equivalent splittings?
Here’s one I’d especially like to know the answer to. There is an arguably more obvious way to try to split a coherent idempotent: instead of the naive definition , we can try to add an extra level of coherence corresponding to and ask for . I tried this first, but the path algebra involved in showing was just too much for me. I was able to show that it works when is the identity function, though, which is promising. Can anyone either show that it works for general , or exhibit an for which it doesn’t work?