Soberness as idempotent-completeness:
towards a formal model theory of virtual ultracategories

The notion of idempotent-complete (or Cauchy complete) category arises from completeness of metric spaces. In this talk, we honor the topological roots of this notion and reinterpret it in the setting of virtual ultracategories, a categorification of topological spaces defined independently in [1, 2, 3] last summer.

Virtual ultracategories (or v·u·categories for short) are a multicategorical generalization of ultracategories, abstracting the structure of “categorified convergence of ultrafilters” on the category of points of a topos. The key motivating theorem is that any topos with enough points can be reconstructed as the category of sheaves over its v·u·category of points. Hence, v·u·categories are strong enough to encode any topos with enough points. This raises the following question: when is a v·u·category sober (i.e. arises as the v·u·category of points of a topos)? In this talk, we focus on the following restricted case:

More precisely, for a subclass $𝒦\subseteq ℳ$ of the v·u·category $ℳ$ of points of a topos, the soberification of $𝒦$ yields an extension $𝒦\subseteq \check{𝒦}\subseteq ℳ$ known as subclosure in the localic case [4]. The following result shows that this subclosure corresponds exactly to closure under v·u·retracts, a straightforward analogue of the usual categorical notion of retraction in the setting of v·u·categories. This result strongly echoes Lawvere’s result [5] relating completeness of metric spaces with idempotent-completeness.

In other words, the geometric notion of soberness, the logical notion of geometrically axiomatizable class of models, and the algebraic notion of v·u·idempotent-completeness all coincide.

Finally, it is worth mentioning that the notion of v·u·retract is powerful enough to recover the standard notion of filtered colimit, which plays a central role in the theory of accessible categories. We thus view the notion of v·u·idempotent-completeness as a first step toward a more general understanding of accessibility for v·u·categories, opening the way to a formal model theoretical study of these structures.