nLab walking isomorphism

Idea

The walking isomorphism (Hadzihasanovic et al 2024, Ozornova & Rovelli 2024), interval groupoid, interval object in groupoids or free-standing isomorphism, is the groupoid:

$$I_\sim \;\coloneqq\; \big\{ a \overset{\;\; \sim \;\;}{\leftrightarrows} b \big\}$$

with precisely two objects and (besides their identity morphisms) one isomorphism and its inverse morphism connecting them.

This is such that for $\mathcal{C}$ any category, a functor of the form

$$I_\sim \longrightarrow \mathcal{C}$$

is precisely a choice of isomorphism in $\mathcal{C}$.

The walking isomorphism can be categorified in a number of ways: to the walking equivalence, to the walking adjoint equivalence, or to the walking 2-isomorphism?. Related, though not quite a categorification in one of the usual senses, is the walking 2-isomorphism with trivial boundary.

Definition

Definition

The walking isomorphism is the groupoid generated by two objects $0$ and $1$ and one morphism $0 \cong 1$, which is an isomorphism by definition of a groupoid.

Definition

Equivalently, the walking isomorphism is the category generated by two objects $0$ and $1$, one arrow $0 \rightarrow 1$, one arrow $1 \rightarrow 0$, and the equations:

$$0 \to 1 \to 0 = \mathrm{id}_0, \quad 1 \to 0 \to 1 = \mathrm{id}_1,$$

which make $0 \to 1$ an isomorphism.

The arrow $0 \rightarrow 1$ is an isomorphism, whose inverse is the arrow $1 \rightarrow 0$. Since these are the only arrows in the category, the interval groupoid is a groupoid.

Remark

The interval groupoid can also be described as the free groupoid on the interval category.

Remark

The interval groupid is an interval object for Cat and Grpd.

Remark

The interval groupoid can also be described as the complete graph with two vertices $K_2$.

Representing of isomorphisms

Proposition

Let $\mathcal{A}$ be a category. Let $\mathcal{I}$ denote the walking isomorphism. Evaluation at the arrow $0\to 1$ establishes a natural bijective correspondence between functors $\mathcal{I}\to\mathcal{A}$ and isomorphisms in $\mathcal{A}$. Thus, for any isomorphism $f$ of $\mathcal{A}$ there is a unique functor $F: \mathcal{I} \rightarrow \mathcal{A}$ such that the arrow $0 \rightarrow 1$ of $\mathcal{I}$ maps under $F$ to $f$.

Proof

Immediate from the definitions.

Properties

Proposition

$\{ 1 \} \subseteq \mathcal{I}$ is the full subcategory classifier of the 1-category $Cat$. That is, for any small category $\mathcal{A}$, there is a bijective correspondence between full subcategories of $\mathcal{A}$ and functors $\mathcal{A} \to \mathcal{I}$, with the reverse direction given by taking the pullback of the inclusion $\{ 1 \} \subseteq \mathcal{I}$.

Proof

Functors into $\mathcal{I}$ are uniquely determined by functions on the sets of objects. $\{ 1 \}$ is a full subcategory of $\mathcal{I}$, and any pullback of a full subcategory can be given as a full subcategory.

In fact, this generalizes. If $X$ is a simplicial set, say that a full subspace of $X$ is a subsimplicial set $S \subseteq X$ with the property there is some subset $S_0 \subseteq X_0$ such that $S$ contains exactly the simplices whose vertices are all contained in $S_0$.

Proposition

The nerve $N(\mathcal{I})$ is the full subspace classifier for $sSet$, and thus $N(\mathcal{I})$ represents the subpresheaf $FullSub \subseteq Sub$ of full subspaces.

Proof

This can be determined from the explicit description of $N_n(\mathcal{I}) \cong \{ 0, 1 \}^{n+1}$ given by listing the vertices of a path. However, it’s more informative to observe that $N(\mathcal{I}) = indisc(\{ 0, 1 \})$, where $indisc$ is the indiscrete space functor, which is the direct image part of the geometric embedding $Set \subseteq sSet$ whose inverse image is $X \mapsto X_0$.

Remark

This also implies $N(\mathcal{I})$ is the full subcategory classifier of $qCat$, the 1-category of quasi-categories, since those are given by full subspaces of simplicial sets.

Related concepts

• walking structure

  • the boolean domain $2 \coloneqq \partial \Delta^1$; i.e. the walking pair of objects

  • the directed interval category $I \coloneqq \Delta^1$; i.e. the walking morphism

  • the (2,0)-horn category $\Lambda_0^2$; i.e. the walking cospan

  • the (2,1)-horn category $\Lambda_1^2$; i.e. the walking composable pair

  • the (2,2)-horn category $\Lambda_2^2$; i.e. the walking span

  • the 2-simplex category $\Delta^2$; i.e. the walking commutative triangle

  • the walking parallel pair

  • the walking isomorphism

  • Adj; i.e. the walking adjunction

  • the walking equivalence

  • the walking adjoint equivalence

  • the walking 2-isomorphism with trivial boundary

  • the syntactic category of a theory $T$; i.e. the walking $T$-model

• In dependent type theory, many higher inductive types can be considered to be walking structures:

  • the unit type is the walking element

  • the boolean type is the walking pair of elements

  • the interval type is the walking identification

  • one definition of the circle type is the walking self-identification

  • another definition of the circle type is the walking parallel pair of identifications.

  • the suspension type of a type $I$ is the walking parallel $I$-indexed family of identifications.

  • the natural numbers type is the walking sequence

  • the integers type is the walking bi-infinite sequence

  • the walking bridge

  • the directed interval type is the walking morphism in the sense of element of a hom type

References

The phrase “walking isomorphism” appears in:

• Amar Hadzihasanovic, Félix Loubaton?, Viktoriya Ozornova, Martina Rovelli A model for the coherent walking $\omega$-equivalence (arXiv:2404.14509)

• Viktoriya Ozornova, Martina Rovelli, What is an equivalence in a higher category, Bulletin of the London Mathematical Society, Volume 56, Issue 1, January 2024, Pages 1-58 (doi:10.1112/blms.12947)

A generalization of the notion of the interval groupoid to simplicial groupoids is considered in

• William Dwyer, Daniel Kan, §2.8 of: Homotopy theory and simplicial groupoids, Indagationes Mathematicae (Proceedings) 87 4 (1984) 379-385 [doi:10.1016/1385-7258(84)90038-6]

and plays a key role in the discussion of the model structure on simplicial groupoids, see there.