nLab
isoinserter

Idea

An iso-inserter is a particular kind of 2-limit in a 2-category, which universally inserts an invertible 2-morphism between a pair of parallel 1-morphisms.

Definition

Let $f,g:A\rightrightarrows B$ be a pair of parallel 1-morphisms in a 2-category. The iso-inserter of $f$ and $g$ is a universal object $V$ equipped with a morphism $v:V\to A$ and an invertible 2-morphism $\alpha :fv\stackrel{\cong }{\to }gv$.

More precisely, universality means that for any object $X$, the induced functor

$$\mathrm{Hom}(X,V)\to \mathrm{IsoIns}(\mathrm{Hom}(X,f),\mathrm{Hom}(X,g))$$Hom(X,V) \to IsoIns(Hom(X,f),Hom(X,g))

is an equivalence, where $\mathrm{IsoIns}(\mathrm{Hom}(X,f),\mathrm{Hom}(X,g))$ denotes the category whose objects are pairs $(u,\beta )$ where $u:X\to A$ is a morphism and $\beta :fu\stackrel{\cong }{\to }gu$ is an invertible 2-morphism. If this functor is an isomorphism of categories, then we say that $V\stackrel{v}{\to }A$ is a strict iso-inserter.

Iso-inserters and strict iso-inserters can be described as a certain sort of weighted 2-limit, where the diagram shape is the walking parallel pair $P=(\cdot \rightrightarrows \cdot )$ and the weight $P\to \mathrm{Cat}$ is the diagram

$$1\rightrightarrows \mathrm{Iso}$$1 \;\rightrightarrows\; Iso

where $1$ is the terminal category and $\mathrm{Iso}$ is the walking isomorphism.

An iso-inserter in $K^{\mathrm{op}}$ (see opposite 2-category) is called a co-iso-inserter in $K$.

Properties

• Any iso-inserter is a faithful morphism, and also a conservative morphism, but not in general a fully faithful morphism.

• Any strict iso-inserter is, in particular, an iso-inserter. (This is not true for all strict 2-limits.)

• Since $\mathrm{Iso}$ is equivalent to $1$, iso-inserters (but not strict iso-inserters) can equivalently be described as the conical limit of a diagram of shape $P$, which might be called a (non-strict) pseudo-equalizer. A strict pseudo-equalizer—that is, a strict pseudolimit of a diagram of shape $P$—is not the same as a strict isoinserter, but if it exists, a strict pseudo-equalizer is also, in particular, a (non-strict) iso-inserter. The relationship between isoinserters and pseudoequalizers is analogous to the relationship between iso-comma-objects and pseudo-pullbacks.

• Iso-inserters can be constructed as an inserter followed by an inverter (for both the strict and non-strict versions). In particular, it follows that strict iso-inserters are a type of PIE-limit.