Splitting Idempotents

Posted on 8 December 2014 by Mike Shulman

A few days ago Martin Escardo asked me “Do idempotents split in HoTT”? This post is an answer to that question.

Coherent idempotents

To start with, what is an idempotent? The standard meaning of idempotent is a map $f :X \to X$ such that $f\circ f = f$ , which in HoTT would mean a homotopy $I:\prod_{x:X} f(f(x))=f(x)$ . A splitting of an idempotent is a pair of maps $r:X\to A$ and $s:A\to X$ such that $s\circ r = f$ and $r\circ s = \mathrm{id}$ . (Note that the existence of such $r,s$ actually implies $f$ is idempotent, since then $f f = srsr = s1r = sr = f$ .)

Given an idempotent in HoTT, the obvious way to try to split it would be to take $A = \sum_{x:X} (f(x)=x)$ , with $r(x) = (f(x),I(x))$ and $s(x,p) = x$ . However, with this definition we cannot in general prove $r\circ s = \mathrm{id}$ . Indeed, as Martin pointed out, when $f=\mathrm{id}_X$ with the obvious proof of idempotency, for this definition to satisfy $r\circ s =\mathrm{id}_A$ is the same as to say that $X$ is a set.

This suggests that if $X$ is not a set, then we might need some sort of coherence for the witness $I$ of idempotency. For instance, we might ask whether $\mathrm{ap}_f(I(x)) = I(f(x))$ . 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 $r:X\to A$ and $s:A\to X$ and a homotopy $H : r \circ s \sim \mathrm{id}_A$ , yielding as above a witness that $f= s\circ r$ is idempotent. Then the naturality of H implies that the coherence condition $\mathrm{ap}_f(I(x)) = I(f(x))$ 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 $s\circ r$ for functions s and r such that $r\circ s \sim \mathrm{id}$ , then f admits a “coherent system of idempotence data”. It doesn’t say that if f is idempotent with a specified homotopy $I:f\circ f \sim f$ 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 $I:f\circ f \sim f$ 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 $(\infty,1)$ -category theory. In Higher Algebra he showed that if a witness to idempotence satisfies the one additional coherence condition $\mathrm{ap}_f(I(x)) = I(f(x))$ , 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 $f$ , with witness $I:f\circ f \sim f$ and single coherence $J : \prod_{x:X} \mathrm{ap}_f(I(x)) = I(f(x))$ . Lurie constructs a splitting as the colimit of the sequence

$X \xrightarrow{f} X \xrightarrow{f} X \xrightarrow{f} \cdots$

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

$\cdots \xrightarrow{f} X \xrightarrow{f} X \xrightarrow{f} X$

and this is rather easier to work with in HoTT; it’s just

$\sum_{a:\mathbb{N}\to X} \prod_{n:\mathbb{N}} f(a_{n+1}) = a_n.$

If we call this type $A$ , then we have an obvious $s:A\to X$ defined by $s(a) = a_0$ , and a slightly less obvious $r:X\to A$ defined by $r(x) = ((n\mapsto f(x)), (n\mapsto I(x)))$ , such that $s\circ r = f$ . The tricky part is proving $r\circ s = 1$ . (Of course we need function extensionality at this point.) By definition, $r(s(a)) = ((n\mapsto f(a_0)), (n\mapsto I(a_0)))$ , so we need to show first of all that $a_n = f(a_0)$ for all $n$ . We induct on $n$ . The base case is

$a_0 = f(a_1) = f(f(a_1)) = f(a_0),$

where the middle equality is $I(a_1)$ and the other two are the specified equality $f(a_1)=a_0$ (part of the second component of $a$ ). The induction step is similarly

$a_{n+1} = f(a_{n+2}) = f(f(a_{n+2})) = f(a_{n+1}) = a_n = f(a_0),$

using the induction hypothesis at the end. It remains to check a naturality condition, than the composite $f(a_{n+1}) = a_n = f(a_0)$ is equal to the composite $f(a_{n+1}) = f(f(a_0)) = f(a_0)$ , 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 $J$ in there somewhere. One might say that we only need one level of coherence “because” of the induction: we can apply $J$ once at each induction step and build up more and more coherence as $n$ 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 $X = B \mathrm{Aut}([0,1])$ , where $[0,1]$ 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 $\mathbf{2}^{\mathbb{N}}$ . In particular, the topology plays no role in the counterexample (although in constructive models $\mathbf{2}^{\mathbb{N}}$ does of course behave “topologically”).

By definition, in HoTT by $B \mathrm{Aut}(C)$ we mean $\sum_{Z:\mathrm{Type}} \Vert Z = C \Vert$ . Topologically, this is the “classifying space for fibrations with fiber $C$ “. It is connected and pointed (with basepoint $(C,|\mathrm{refl}|)$ ), and its loop space is the type $\mathrm{Aut}(C) = (C\simeq C)$ of self-equivalences of $C$ . Thus, if $C$ is a set (such as Cantor space $\mathbf{2}^{\mathbb{N}}$ ), then $B \mathrm{Aut}(C)$ is a $K(G,1)$ , where $G$ is the (set-)group $\mathrm{Aut}(C)$ .

In particular, a map $f: B \mathrm{Aut}(C) \to B \mathrm{Aut}(C)$ is determined essentially by a group homomorphism $\mathrm{Aut}(C) \to \mathrm{Aut}(C)$ . This is how Lurie talks about it: in the case $C=[0,1]$ he defines the action of $f$ on an automorphism $h:\mathrm{Aut}([0,1])$ by $f(h)(x) = \frac{1}{2} h(2x)$ if $x\le \frac{1}{2}$ and $f(h)(x) = x$ otherwise. For $C=\mathbf{2}^{\mathbb{N}}$ , we could define an analogous $f$ by $f(h)(a) = (0,h(n\mapsto a_{n+1}))$ if $a_0 = 0$ and $f(h)(a) = a$ if $a_1 = 1$ . In other words, we use the fact that our space decomposes into two copies of itself, and we have our automorphism $h$ act on the first copy only.

Now, actually defining $f$ like this in HoTT would require knowing that endomaps of $B \mathrm{Aut}(\mathbf{2}^{\mathbb{N}})$ correspond to group endomorphisms of $\mathrm{Aut}(\mathbf{2}^{\mathbb{N}})$ . The only way I can think of to do this is to construct $K(\mathrm{Aut}(\mathbf{2}^{\mathbb{N}}),1)$ as a HIT, show that it’s equivalent to $B \mathrm{Aut}(\mathbf{2}^{\mathbb{N}})$ , and then use the recursion principle of that HIT. (Is there’s another way?)

However, our definition of $B \mathrm{Aut}(C)$ suggests an alternative approach. An element of $B \mathrm{Aut}(C)$ is a type $Z$ that is merely isomorphic to $C$ ; let’s just define $f(Z) = Z+C$ (where from now on $C$ will be the Cantor space). Note that the action of this $f$ 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 $C$ decomposes as two copies of itself, $C\simeq C+C$ , implies that $f$ is in fact an endomorphism of $B \mathrm{Aut}(C)$ , since we have (merely) $Z+C\simeq C+C \simeq C$ . And the same fact implies that $f$ is idempotent, since $(Z+C)+C \simeq Z+(C+C)\simeq Z+C$ . I think this is a nice example of the benefits of the univalent approach to classifying spaces!

It remains to show that $f$ is not coherently idempotent. Lurie says that if it were, then the colimit $X \xrightarrow{f} X \xrightarrow{f} X \xrightarrow{f} \cdots$ would be its splitting, and hence the map from $X = B\mathrm{Aut}(C)$ to that colimit would be surjective on $\pi_1$ , whereas $f$ itself is certainly not surjective on $\pi_1$ and so this is impossible. In HoTT, this would requite a HIT colimit, and probably an encode-decode argument to characterize the $\pi_1$ of the colimit.

However, here again we can give a more direct argument. Suppose $f$ were coherently idempotent, so that we have $I : f\circ f = f$ and $J : \prod_{Z:B\mathrm{Aut}(C)} \mathrm{ap}_f(I(Z)) = I(f(Z))$ . The coherence $J$ is an equality in the type $f(f(f(Z))) = f(f(Z))$ , thus it is equivalently a homotopy between two equivalences $Z+C+C+C \to Z+C+C$ . Essentially by definition, the first equivalence (corresponding to $\mathrm{ap}_f(I(Z))$ ) decomposes the domain and codomain as $(Z+C+C)+C$ and $(Z+C)+C$ , mapping the first summand $Z+C+C$ to $Z+C$ by $I(Z)$ and the second summand $C$ to $C$ by the identity.

As for the other, if $I$ were the idempotency proof $(Z+C)+C \simeq Z+(C+C)\simeq Z+C$ that we gave above, then the equivalence $Z+C+C+C \to Z+C+C$ corresponding to $I(f(Z))$ would bracket the domain instead as $(Z+C)+(C+C)$ and map it to $(Z+C)+C$ by the identity on $Z+C$ and the “fold” equivalence $C+C\to C$ . Thus, the two could not possibly be homotopic, since they would send the third summand of $Z+C+C+C$ to different summands of the codomain.

This argument doesn’t quite work as stated since $I$ might not be the same proof of idempotency that we gave above. However, whatever $I$ is, it’s defined “for all $Z:B\mathrm{Aut}(C)$ “, which by the HoTT meaning of “for all” implies that the induced equivalences $Z+C+C\to Z+C$ must be natural with respect to automorphisms of $Z$ . In particular, the equivalence $(C+C)+C+C \to (C+C)+C$ induced by $I(f(C)) = I(C+C)$ must be natural with respect to the “flip” automorphism $C+C \simeq C+C$ . By looking at which summands are fixed by the automorphisms induced by this flip, we can conclude that $I(f(C))$ 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.

Open questions

There are a number of further questions to ask. For instance, if we have $I,J$ and we use them to split $f$ , do the new witnesses $I,J$ induced from the splitting agree with the given ones? How many different ways can a given map $f$ “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 $A = \sum_{x:X} (f(x)=x)$ , we can try to add an extra level of coherence corresponding to $J$ and ask for $A = \sum_{x:X} \sum_{p:f(x)=x} (\mathrm{ap}_f(p)=I(x))$ . I tried this first, but the path algebra involved in showing $r\circ s = \mathrm{id}$ was just too much for me. I was able to show that it works when $f$ is the identity function, though, which is promising. Can anyone either show that it works for general $f$ , or exhibit an $f$ for which it doesn’t work?

This entry was posted in Code, Homotopy Theory, Univalence. Bookmark the permalink.

13 Responses to Splitting Idempotents

Martin Escardo says:

8 December 2014 at 05:20

Very nice! Thanks for such a complete answer.

I would like to record a special case of interest that has a more direct proof. Suppose you instead ask

Which functions $f:X\to X$ split with a section-retraction pair $s:A\to X$ and $r:X\to A$ such that $s$ is an embedding in the sense of the HoTT book?

This means that the application map $x=y \to sx=sy$ is an equivalence, or, equivalently, which is what I am going to use, the fibers of $s$ are propositions. Then the answer to the above question is

Precisely those idempotents $f : X \to X$ such that the type $f x = x$ has split support for every $x:X$ .

The proof is easy. In one direction, consider $A=\Sigma(x:X). ||f x = x||.$ Then the obvious section and retraction work. For the other direction, we have to show that if $f$ does split in the above manner, then the type $f x = x$ has split support. Because $f(x)=s(r(x))$ , it is enough to show that the type $s(r(x))=x$ is logically equivalent to a proposition. But it is easy to see that it is logically equivalent to the fiber $\Sigma(a:A).s(a)=x$ , which is a proposition, by assumption.

Reply
- Mike Shulman says:
  
  8 December 2014 at 05:26
  
  Thanks for adding this! It emphasizes in another way the different behavior of idempotents in homotopy theory, since in set theory, the splitting of an idempotent is always a subset of the original carrier.
  
  Reply
- Mike Shulman says:
  
  8 December 2014 at 05:27
  
  Are there any non-sets that have the property “ $f x = x$ has split support for every x” in an interesting way? As an example of a boring way this could happen for a non-set, we could consider $A+B$ , where B is a set and f maps A into B.
  
  Reply
  - Mike Shulman says:
    
    8 December 2014 at 13:12
    
    If f is the identity, then this property just says that we have $\prod_{x:X} x=x$ . Of course that’s true trivially for all X (as it must be, since the identity splits by a pair of identity maps), and can also be true non-trivially, such as when $X=B \mathrm{Aut}(\mathbf{2})$ or $S^1$ .
    
    Reply
- Martin Escardo says:
  
  10 December 2014 at 09:11
  
  Another remark: Notice that the type $A$ constructed in my proof is (equivalent to) the image of the idempotent $f$ , and that the section-retraction pair is simply the canonical factorization of $f$ through its image. Conversely, if the canonical factorization of a function $f$ through its image is a section-retraction pair, then the type $f x = x$ has split support for every $x:X$ (either by direct calculation, or using the fact that the image is always embedded). For a constant map, to use Nicolai’s example below, the image is not in general contractible, but the splitting is through a contractible type.
  
  Reply
Nicolai Kraus says:

9 December 2014 at 23:27

Nice, I have enjoyed this! I have not fully digested some parts of your post, but I think I can answer your last question:

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 $A = \sum_{x:X} (f(x)=x)$ , we can try to add an extra level of coherence corresponding to $J$ and ask for $A = \sum_{x:X} \sum_{p:f(x)=x}(\mathrm{ap}_f(p)=I(x))$ . I tried this first, but the path algebra involved in showing $r\circ s = \mathrm{id}$ was just too much for me. I was able to show that it works when $f$ is the identity function, though, which is promising. Can anyone either show that it works for general $f$ , or exhibit an $f$ for which it doesn’t work?

First, I have a simple positive statement:
If $f$ has the property that the map $\mathrm{ap}_f : (f(x)=x) \to (f(f(x)) = f(x))$ is an equivalence for all $x$ (and $f$ also comes with $I$ and $J$ , of course!), then what you said works.
We can see this as follows: for any given $x$ , the type $\sum_{p:f(x)=x}(\mathrm{ap}_f(p)=I(x))$ will be contractible (it is essentially a coconut – it would be a “pure” coconut if the $\mathrm{ap}_f$ was removed and the $I(x)$ replaced by some other fixed term to make it type check; but because of our assumption, $\mathrm{ap}_f$ does not make a difference). So, $A$ and $X$ are equivalent and the equivalence is the first projection. Thus, to convince ourselves of $r\circ s = \mathrm{id}$ , we only need to check that the first component of $r(s(x,p,q))$ equals $x$ , but this component will be $f(x)$ , and the required witness is $p$ .
Of course, this means that what you suggested works for all embeddings $f$ , and in particular for the identity.

Now one should probably wonder whether $\mathrm{ap}_f : (f(x)=x) \to (f(f(x)) = f(x))$ might be always an equivalence. After all, if we have some $p : f(x)=x$ , then the types $(f(x)=x)$ and $(f(f(x)) = f(x))$ are equivalent. Unfortunately, $\mathrm{ap}_f$ is not necessarily an equivalence anyway.

If I have not made a mistake, I can give an example in which the suggested $A$ does not work. Suppose $X$ is some type with a point $x_0 : X$ . Define $f : X \to X$ to be constantly $x_0$ . Then, $f$ is idempotent with the witness $I$ being constantly $\mathrm{refl}$ , and the coherence proof $J$ can be taken to be constantly $\mathrm{refl}$ as well. Now the type $\sum_{x:X} (f(x)=x)$ simplifies to the coconut $\sum_{x:X} (x_0=x)$ . Set $A = \sum_{x:X} \sum_{p:f(x)=x}(\mathrm{ap}_f(p)=I(x))$ as in your question. We know that $r(s(x,p,q))$ will be $(x_0,\mathrm{refl},\mathrm{refl})$ . We further know now that the two pairs $(x,p)$ and $(x_0,\mathrm{refl})$ live in a contractible type. The equality $(x,p,q) = (x_0,\mathrm{refl},\mathrm{refl})$ can therefore be simplified: we can assume that $(x,p)$ is actually judgmentally $(x_0,\mathrm{refl})$ , and then the equality of the triples is equivalent to the equality $q = \mathrm{refl}$ . This is the case if $X$ is a 1-type, but of course not in general.

Reply
- Mike Shulman says:
  
  10 December 2014 at 13:15
  
  Nice; thanks! I should have thought to look at constant maps (being the “polar opposite” of the identity map). So I guess the sequential limit construction is it. On one hand, this makes sense to me, because just as a “coherent idempotent” ought to involve infinitely many data, I feel that an element of its splitting ought also to involve not just a path $f(x) = x$ but infinitely many coherence data on it. And an element of the sequential limit does involve infinitely many data. But on the other hand, it doesn’t make sense, because the data in a point of the sequential limit are all points and 1-paths; there are no higher coherence paths visible. Are they hidden somewhere?
  
  I’m making a bit of progress on the other questions I asked. In particular, I can now prove that the idempotence datum $I$ is recoverable from the splitting, and I have a guess for a counterexample to show that $J$ is not generally recoverable. Once I’ve sorted it all out, I may make another post.
  
  Reply
  - Nicolai Kraus says:
    
    13 December 2014 at 14:33
    
    It is probably somewhat obvious, but I cannot see what the canonical next coherence condition (after $J$ ) is, or how $A$ should be extended. Can you give me a hint?
    (Side note: In my first comment I said that the splitting works under the condition “ $\mathrm{ap}_f : (f(x)=x) \to (f(f(x)) = f(x))$ is an equivalence”, but together with “ $f$ is idempotent”, this already implies that $f$ is the identity. Martin and I noticed this.)
    
    Reply
    - Mike Shulman says:
      
      13 December 2014 at 15:22
      
      It’s actually a bit of an accident that $J$ can be given such a short type. Really, $J$ should be a homotopy between the two induced homotopies $f^3 \sim f$ , one of which is $fI \cdot I$ and the other of which is $If \cdot I$ . But since whiskering with $I$ is an equivalence, it’s equivalent for $J$ to relate $f I$ and $I f$ .
      
      As we go up in dimensions we can formulate the conditions as cubes or as simplices. With cubes, we would regard $J$ in the form $fI \cdot I = I f \cdot I$ as a square, draw a cube whose faces are all instances of this $J$ (except that one of them is a naturality square), and ask for the next coherence datum that fills in this cube.
      
      With simplices, the dimensions are shifted by one: we regard $I$ as a 2-simplex with boundary 1-simplices $f,f,f$ , then $J$ is a 3-simplex whose boundary 2-simplices are $f I,If,I,I$ , and then the next datum is a 4-simplex whose five boundary 3-simplices are instances of $J$ (in this case the naturality is invisible).
      
      Reply
      - Nicolai Kraus says:
        
        13 December 2014 at 17:41
        
        Thanks! I managed to draw these (up to the three dimensional case). But why did you say that there are no visible higher coherence paths? $I$ gives paths, $J$ gives paths between paths, and so on. Which sort of paths would you have expected?
        
        Reply
        
        Mike Shulman says:
        
        13 December 2014 at 17:53
        
        I mean that in the construction of a splitting of an idempotent as a sequential limit, which I described in the post, there are no visible higher coherence paths. I would naively have expected an element of the splitting to consist of a point $x:X$ and a path $p:f(x)=x$ and a homotopy $q : \mathsf{ap}_f(p)=I_x$ , a higher homotopy involving $J$ , and so on, including paths of all dimensions. Instead, an element of the splitting consists of a function $a:\mathbb{N}\to X$ and a family of paths $p : \prod_{n:\mathbb{N}} f(a_{n+1})=a_n$ , all of which are just 1-dimensional paths.
        
        Reply
        
        Nicolai Kraus says:
        
        14 December 2014 at 07:11
        
        Oh, I see. Thanks.
        
        Reply
Mike Shulman says:

14 July 2015 at 22:40
I’ve now posted a preprint based on the results of this blog post and its sequel; it’s available at arXiv:1507.03634. In addition to the contents of the blog posts, the paper contains
- A few results of Martin’s about situations in which pre-idempotents do split
- A few more details (including some commutative diagrams) in the splitting of quasi-idempotents
- A few more details at the end of the construction of the incoherent pre-idempotent
- A lot more details about $B\mathsf{Aut}(B\mathsf{Aut}(\mathbf{2}))$ , in order to obtain a type having a nontrivial 2-center without making any more assumptions than univalence and propositional truncation. There are two basic ideas involved. The first is that just as an element of the 1-center $\prod_{Z:B\mathsf{Aut}(X)}(Z=Z)$ of $B\mathsf{Aut}(X)$ is an automorphism of $X$ that commutes with all other automorphisms, an element of the 2-center $\prod_{Z:B\mathsf{Aut}(X)}(\mathsf{refl}_Z=\mathsf{refl}_Z)$ is an element of the 1-center of $X$ (that is, $f:\prod_{x:X} (x=x)$ ) that “commutes with” all automorphisms of $X$ . The second is that (like $\mathbf{2}$ ) the type $B\mathsf{Aut}(\mathbf{2})$ is equivalent to its own automorphism group, and the way that it acts on itself is by its structure as an abelian 2-group, described univalently as in example 1 here.
Reply