nLab walking isomorphism

Redirected from "free-standing isomorphism".
References

Contents

Idea

The interval object in groupoids or free-standing isomorphism or, if you insist, the “walking isomorphism”, is the groupoid:

I {ab} 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 𝒞 I_\sim \longrightarrow \mathcal{C}

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

The interval groupoid 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 free-standing isomorphism is the category generated by two objects 00 and 11, one arrow 010 \rightarrow 1, one arrow 101 \rightarrow 0, and the equations:

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

which make 010 \to 1 an isomorphism.

Remark

The arrow 010 \rightarrow 1 is an isomorphism, whose inverse is the arrow 101 \rightarrow 0.

Remark

The free-standing isomorphism is a groupoid.

Remark

The free-standing isomorphism can also be described as the free groupoid on the interval category, that is to say, the walking arrow. Because it is an interval object for Cat and Grpd, it is also known as the interval groupoid.

Representing of isomorphisms

Proposition

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

Proof

Immediate from the definitions.

Properties

Proposition

{1}\{ 1 \} \subseteq \mathcal{I} is the full subcategory classifier of the 1-category CatCat. 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}\{ 1 \} \subseteq \mathcal{I}.

Proof

Functors into \mathcal{I} are uniquely determined by functions on the sets of objects. {1}\{ 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 XX is a simplicial set, say that a full subspace of XX is a subsimplicial set SXS \subseteq X with the property there is some subset S 0X 0S_0 \subseteq X_0 such that SS contains exactly the simplices whose vertices are all contained in S 0S_0.

Proposition

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

Proof

This can be determined from the explicit description of N n(){0,1} n+1N_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()=indisc({0,1})N(\mathcal{I}) = indisc(\{ 0, 1 \}), where indiscindisc is the indiscrete space functor, which is the direct image part of the geometric embedding SetsSetSet \subseteq sSet whose inverse image is XX 0X \mapsto X_0.

Remark

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

References

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

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

Last revised on April 25, 2023 at 08:49:59. See the history of this page for a list of all contributions to it.