As a Grothendieck topos is a categorified locale, so an ionad is a categorified topological space. While the opens are primary in toposes and locales, the points are primary in ionads and topological spaces.
Richard Garner developed the theory of ionads, in which the topos $Set^X$ plays an role analogous to that of the lattice $\mathbb{2}^X$ (the power set of $X$) in the theory of topological spaces. Intuitively, we are categorifying the subobject classifier $\mathbb{2}\in Set$ to the “categorified subobject classifier” $Set\in Cat$ (which classifies discrete opfibrations.
The word ‘ionad’ is Irish for a location, place, or site; ‘Ionad’ often translates ‘Centre’ in titles of institutions. It is pronounced /ˈɪnəd/ (roughly ‘INN-ad’ or ‘UNN-ad’, not ‘i-NAD’ or ‘yonad’; ‘ЫН-ад’ in a North Slavic language), or more precisely ˈɨ̞n̪ˠəd̪ˠeast in Munster), following Wikipedia. The plural (which you can use if you like to use ‘topoi’ too) is ‘ionaid’ (/ˈɪnəɟ/, ‘INN-adge’ or ‘UNN-adge’, ‘ЫН-адь’, [nd]). We could go on to decline it out of the nominative case, but now it's getting silly.
Recall that a topology on a set $X$ can be defined by giving its interior operator, an operation $Int\colon \mathbb{2}^X \to \mathbb{2}^X$ (where $\mathbb{2}$ is the poset of truth values) such that
for all subsets $A, B$ of $X$.
In more sophisticated language, $Int$ is a finite meet-preserving comonad on the power set of $X$.
Categorifying (mostly), we have this:
An ionad is a set $X$ together with a finite limit-preserving comonad $Int_X$ on the category $Set^X$. An ionad is bounded if the comonad is accessible.
Although Garner does not require an ionad to be bounded, the nicest results hold for them, and all of his applications involve only bounded ionads. In fact, Garner writes, ‘Indeed, the existence of unbounded ionads is a problem that seems to be independent of the axioms of Zermelo-Fraenkel set theory.’ (Section 3.8).
Bounded ionads give rise to exactly the Grothendieck toposes with enough points as their topos of coalgebras. (See below)
It may seem odd to take $X$ to be a set rather than something else such as a groupoid or a category. An analogous definition can be given where $X$ is a groupoid or a category, of course, but the reason for taking it to be a set is that it makes the analogy to classical topological spaces closer. Consider the following three notions:
All three of these induce a topology on the underlying set of $X$. But it is (1) that is exactly a topological space: (2) and (3) include the extra data of a (perhaps symmetric) preorder on $X$ that maps bijectively-on-objects into the specialization preorder of that topology.
However, as in other cases such as Segal categories/complete Segal spaces and generalized multicategories, another way to “get rid of extra data” is to force it to duplicate data that’s already present (a “completeness” condition). Thus we could consider instead (still in the uncategorified case):
These would give equivalent definitions to (1), but may be better-behaved in some ways. In homotopy type theory without sets cover, they would no longer be equivalent, but the groupoidal/preorder versions might be better. For ionads the corresponding definitions would be
(Asking that these functors also be surjective on objects would be a sobriety condition on an ionad.)
When categorifying further to “$n$-ionads” and “$\infty$-ionads”, the possible options multiply further; but that is probably a topic for another page. For discussion of these questions, see the nForum thread.
Recall that, given two topological spaces $X$ and $Y$, a continuous map from $X$ to $Y$ is a function $f\colon X \to Y$ (on the underlying sets) such that
for every subset $A$ of $Y$, where $f^*$ takes the preimage.
Categorifying (and adding a coherence law), we have this:
Given ionads $X$ and $Y$, a continuous map from $X$ to $Y$ consists of a function $f\colon X \to Y$ (on the underlying sets of points) together with a natural transformation
where $f^*\colon Set^Y \to Set^X$ is $Set^f$, such that $Int_f$ ‘respects the comonad structures’.
I need to figure out exactly what this last clause means.
Note that $Int_f$ is part of the structure here; it is not merely a property. (In other words, the forgetful functor from ionads to topological spaces is not faithful.)
There is an obvious notion of 2-morphism, which turns out to be trivial (but probably would not be if $X$ were allowed to be a groupoid). However, the category of ionads is presumably (like Top) still a locally prosetal 2-category under the specialisation order.
As every topological space has a Heyting algebra (in fact a frame, or dually a locale) of open subsets, so every ionad has a topos (in fact a Grothendieck topos, if it is bounded) of opens.
Given an ionad $X$, an open in $X$ is simply a coalgebra? of the comonad $Int_X$.
The opens of $X$ form a topos $\Omega(X)$, and we have a surjective geometric morphism from $Set^X$ to $\Omega(X)$. In fact, an ionad may be defined as a set $X$ together with a surjective geometric morphism from $Set^X$ to some topos, much as a topological space may be defined as a set $X$ together with a surjective locale morphism from $\mathbb{2}^X$ to some locale. The topos $\Omega(X)$ is essentially unique by surjectivity, and this also shows that $\Omega(X)$ has enough points.
Just as $\Omega(X)$ is a frame whenever $X$ is a topological space, so $\Omega(X)$ should be a Grothendieck topos when $X$ is an ionad. In fact, this holds only for bounded ionads; an ionad may be defined to be bounded if and only if its topos of opens is cocomplete (or equivalently a Grothendieck topos).
A continous map between topological spaces may be given by a function $f\colon X \to Y$ and a commuting square
Similarly, a continuous map between ionads may be given by a function $f\colon X \to Y$ and a commuting square
Without loss of generality, we may require this square to commute on the nose; this is related to the triviality of $2$-morphisms in the category of ionads.
Note that the map $\Omega(Y) \to \Omega(X)$ must be the preimage half of a geometric morphism from $\Omega(X)$ to $\Omega(Y)$; we may also define a continous map $X$ to $Y$ to be such a geometric morphism together with a compatible map between the generating points of the toposes.
…
Ionads have been introduced and studied in
Some basic aspects of the theory are developed there, and applications to topology, logic and geometry are discussed.
Further aspects of the theory of ionads, with a focus on their logical importance were studied in
Ivan Di Liberti, Towards Higher Topology, J. Pure Appl. Algebra 226 (2022)
Ivan Di Liberti, Formal Model Theory & Higher Topology, ArXiv 2020.
Last revised on May 24, 2023 at 21:23:35. See the history of this page for a list of all contributions to it.