Idempotents and their splittings

Basic definitions

Retracts

A *retract* of a type X is a type A equipped with a pair of morphisms r : X → A and s : A → X such that the composite r o s is the identity of A.

For example, here is the identity retraction.

Retractions can be composed with equivalences on either side.

A commuting retract of the domain of map induces a retract of its fibers.

Retraction preserves contractibility

Like any record type, RetractOf X is equivalent to a nested sigma-type. We use a product at one place in the middle, rather than a sigma, to simplify the next proof.

Splittings

If an endomap f : X → X arises from a retract as s o r, we say that that retract is a *splitting* of f.

For example, here is the canonical splitting of the identity.

Pre-idempotents

An "idempotent" is a map that at least "ought" to be splittable. The naive definition of idempotent, which is correct in set-level mathematics, is a morphism f : X → X such that ∀ x, f (f x) = f x. We will call this a "pre-idempotent".

The identity function has a canonical structure of a pre-idempotent.

Any pre-idempotent on a set splits.

Any weakly constant pre-idempotent splits (Escardo)

If f is pre-idempotent and f x = x is collapsible for all x, then f splits (Escardo).

Moreover, in this case the section is an embedding.

Conversely, if f splits with a section that is an embedding, then (it is pre-idempotent and) f x = x is collapsible for all x (Escardo).

Quasi-idempotents

However, homotopically we may naturally expect to need some coherence on the witness isidem of idempotency. And indeed, in homotopy theory there are pre-idempotents which do not split; we will see an example later on. We expect a "coherent idempotent" to involve infinitely many data. However, Lemma 7.3.5.14 of *Higher Algebra* suggests that for an idempotent to admit *some* coherentification, hence also a splitting, it suffices to have *one* additional datum. By modifying the construction given there, we can show similarly in type theory that any idempotent satisfying an additional coherence datum splits. We will call a pre-idempotent with this one additional datum a "quasi-idempotent", since it is related to a fully coherent idempotent similarly to the way having a "quasi-inverse" is related to being a coherent equivalence.

The identity function has a canonical structure of a quasi-idempotent.

We have made IsPreIdempotent and IsQuasiIdempotent typeclasses as an experiment. It could be that they should revert back to Definitions.

Split morphisms are quasi-idempotent

First we show that given a retract, the composite s o r is quasi-idempotent.

In particular, it follows that any split function is quasi-idempotent.

Quasi-idempotents split

We now show the converse, that every quasi-idempotent splits.

We need funext because our construction will involve a sequential limit. We could probably also use a HIT sequential colimit, which is more like what Lurie does. (Note that, like an interval type, HIT sequential colimits probably imply funext, so our construction uses strictly weaker hypotheses.)

The splitting will be the sequential limit of the sequence ... → X → X → X.

The section, retraction, and the fact that the composite in one direction is f are easy.

What remains is to show that the composite in the other direction is the identity. We begin by showing how to construct paths in split_idem.

And we verify how those paths compute under split_idem_sect.

Next we show that every element of split_idem can be nudged to an equivalent one in which all the elements of X occurring are double applications of f.

Now we're ready to prove the final condition. We prove the two arguments of path_split_idem separately, in order to make the first one transparent and the second opaque.

We end this section by showing that we can recover the witness I of pre-idempotence from the splitting.

However, the particular witness J of quasi-idempotence can *not* in general be recovered from the splitting; we will mention a counterexample below. This is analogous to how eissect and eisretr cannot both be recovered after isequiv_adjointify; one of them has to be modified.

Splitting already-split idempotents

In the other direction, suppose we are given a retract, we deduce from this a quasi-idempotent, and then split it by the above construction. We will show that the resulting retract is equivalent to the original one, so that RetractOf X is itelf a retract of QuasiIdempotent X.

We begin by constructing an equivalence between split_idem (s o r) and A. We want to make this equivalence transparent so that we can reason about it later. In fact, we want to reason not only about the equivalence function and its inverse, but the section and retraction homotopies! Therefore, instead of using equiv_adjointify we will give the coherence proof explicitly, so that we can control these homotopies. However, we can (and should) make the coherence proof itself opaque. Thus, we prove it first, and end it with Qed.

Now we can construct the desired equivalence.

It is easy to show that this equivalence respects the section and the retraction.

Less trivial is to show that it respects the retract homotopy.

For some reason this last one needs help.

We will also show that it respects the homotopy to the split map. It's unclear whether this has any use.

Brace yourself.

Whew, that's not so bad.

Using these facts, we can show that RetractOf X is a retract of QuasiIdempotent X.

We have a similar result for splittings of a fixed map f.

And also for splittings of a fixed map that also induce a given witness of pre-idempotency.

Fully coherent idempotents

This gives us a way to define fully coherent idempotents. By Corollary 4.4.5.14 of *Higher Topos Theory*, if we assume univalence then RetractOf X has the correct homotopy type of the type of fully coherent idempotents on X. However, its defect is that it raises the universe level. But now that we've shown that RetractOf X is a retract of the type QuasiIdempotent X, which is of the same size as X, we can obtain an equivalent type by splitting the resulting idempotent on QuasiIdempotent X. For convenience, we instead split the idempotent on splittings of a fixed map f, and then sum them up to obtain the type of idempotents.

The above definitions depend on Univalence. Technically this is the case by their construction, since they are a splitting of a map that we only know to be idempotent in the presence of univalence. This map could be defined, and hence "split", without univalence; but also only with univalence do we know that they have the right homotopy type. Thus univalence is used in two places: concluding (meta-theoretically) from HTT 4.4.5.14 that RetractOf X has the right homotopy type, and showing (in the next lemma) that it is equivalent to Idempotent X. In the absence of univalence, we don't currently have *any* provably-correct definition of the type of coherent idempotents; it ought to involve an infinite tower of coherences as defined in HTT section 4.4.5. However, there may be some Yoneda-like meta-theoretic argument which would imply that the above-defined types do have the correct homotopy type without univalence (though almost certainly not without funext).

For instance, here is the standard coherent idempotent structure on the identity map.

Quasi-idempotents need not be fully coherent

We have shown that every quasi-idempotent can be "coherentified" into a fully coherent idempotent, analogously to how every quasi-inverse can be coherentified into an equivalence. However, just as for quasi-inverses, not every witness to quasi-idempotency *is itself* coherent. This is in contrast to a witness of pre-idempotency, which (if it extends to a quasi-idempotent) can itself be extended to a coherent idempotent; this is roughly the content of split_idem_preidem and splitting_preidem_retractof_qidem. The key step in showing this is to observe that when f is the identity, the retract type Splitting_PreIdempotent f of splitting_preidem_retractof_qidem is equivalent to the type of types-equivalent-to-X, and hence contractible.

Therefore, there is a unique coherentification of the canonical witness preidem_idmap of pre-idempotency for the identity. Hence, to show that not every quasi-idempotent is coherent, it suffices to give a witness of quasi-idempotency extending preidem_idmap which is nontrivial (i.e. not equal to qidem_idmap). Such a witness is exactly an element of the 2-center, and we know that some types such as BAut (BAut Bool) have nontrivial 2-centers. In Spaces.BAut.Bool.IncoherentIdempotent we use this to construct an explicit counterexample.

A pre-idempotent that is not quasi-idempotent

We can also give a specific example of a pre-idempotent that does not split, hence is not coherentifiable and not even quasi-idempotent. The construction is inspired by Warning 1.2.4.8 in *Higher Algebra*, and can be found in Spaces.BAut.Cantor.