nLab split support

Split supports

Split supports

Definition

Recall that the support object of an object XX of a regular category (or n-category) is its (-1)-truncation, i.e. the image of the map X1X\to 1 to the terminal object. Let X\Vert X \Vert denote its support.

We say that XX has a split support if the canonical map XXX\to {\Vert X \Vert} has a section. Since X\Vert X \Vert is a subterminal object, it is equivalent to say that there exists any morphism XX{\Vert X \Vert} \to X.

If all objects has split supports, we say that supports split in the ambient category.

Relation to axiom of choice

Supports splitting in a category is a weak form of the external axiom of choice (all regular epis split). In fact, the splitting of supports is exactly the “difference” between the external axiom of choice and the internal axiom of choice, i.e.

EAC(IAC and SS). EAC \Leftrightarrow (IAC \;\text{ and }\; SS).

In foundations

In set theory

If we assume excluded middle, then supports split in the category Set. This has little to do with the foundational axiom of choice; it is more like well-pointedness. Note, however, that to say there is a function assigning to every XX a section of XXX\to {\Vert X \Vert} is much stronger: such a function is a global choice operator.

In constructive mathematics, however, it may not be true that all supports split in Set; this can fail in the internal logic of some toposes. (Note that the “internal” version of “supports split in Set” in a topos may not be the same as the statement that supports split as an external statement about the topos itself.) See (Fourman-Scedrov) and (KECA). Thus, splitting of supports can be regarded as a weaker form of excluded middle.

In (homotopy) type theory

In type theory under propositions as types), where assertions of existence are always witnessed, to say that “all supports split” would by default mean that there is a function as above called the choice operator, assigning to every XX a section of XXX\to {\Vert X \Vert}, and imply the global axiom of choice. To recover the statement which depends only on excluded middle, we need an additional truncation:

(X:Type)(XX). \prod_{(X:Type)} \Vert ( \Vert X \Vert \to X ) \Vert.

We might pronounce this version as “all supports merely split”.

In homotopy type theory, the pure constructive version of “all supports split” ( (X:Type)XX\prod_{(X:Type)} \Vert X \Vert \to X) is in fact inconsistent: it contradicts the univalence axiom. As before, the truncated version is true under LEM but may fail otherwise.

Objects with split support

Since not all supports split in homotopy type theory, it is interesting to consider whether the support of some particular type is split. For instance, for any f:ABf:A\to B, the type qinv(f) g:BA(fg=id B)×(gf=id A)qinv(f) \coloneqq \sum_{g:B\to A} (f g = id_B) \times (g f = id_A) has split support, since its support can be proven to be equal to the type of coherent equivalence data on ff.

It is shown in (KECA) that a type in homotopy type theory has split support if and only if it admits a steady endomap. Thus, it has merely split support if and only if it merely admits a steady endomap.

Some general classes of types can be shown not to have split support, at least not uniformly, by arguments similar to the one which shows that not all types have split support. For instance, the identity type x= Ayx=_A y has split support for all x,y:Ax,y:A if and only if AA is an h-set; this is proven in (KECA), and the “only if” direction is also a special case of Theorem 7.2.2 of the HoTT book.

Similarly, we have:

Theorem

If the type steady(f) (x,y:A+A)(fx=fy)steady(f)\coloneqq \prod_{(x,y:A+A)} (f x = f y) has split support for every endomap f:A+AA+Af:A+A\to A+A, then AA is an h-set.

Proof

Given a,b:Aa,b:A with a=b\Vert a=b\Vert, we show a=ba=b; this suffices to show that AA is a set. Define g,h:AA+Ag,h : A \to A+A to be constant at inl(a)inl(a) and inl(b)inl(b) respectively, and f=[g,h]:A+AA+Af = [g,h] : A+A \to A+A. Then

steady(f)=((A×A)((a=a)×(a=b)×(b=a)×(b=b)))steady(f) = ( (A\times A) \to ((a=a) \times (a=b) \times (b=a) \times (b=b)) )

Since a=b\Vert a=b\Vert, we have steady(f)\Vert steady(f)\Vert. Thus, by assumption, steady(f)steady(f); hence a=ba=b.

In particular, not all types of the form steady(f)steady(f) have split support. Thus, “steadiness” is not as well-behaved a notion as being quasi-invertible.

References

  • M. P. Fourman and A. Scedrov. The “world’s simplest axiom of choice” fails. Manuscripta Math., 38(3):325{332, 1982.

  • Nicolai Kraus, Martin Escardo, Thierry Coquand, Thorsten Altenkirch, Generalizations of Hedberg’s theorem, in M. Hasegawa (Ed.): TLCA 2013, LNCS 7941, pp. 173-188. Springer, Heidelberg 2013. PDF.

    (In this paper, types with split support are called “h-stable”)

Last revised on November 28, 2022 at 06:59:13. See the history of this page for a list of all contributions to it.