nLab isoinserter



2-Category theory

Limits and colimits



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.


Let f,g:ABf,g\colon A\rightrightarrows B be a pair of parallel 1-morphisms in a 2-category. The iso-inserter of ff and gg is a universal object VV equipped with a morphism v:VAv\colon V\to A and an invertible 2-morphism α:fvgv\alpha\colon f v \xrightarrow{\cong} g v.

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

Hom(X,V)IsoIns(Hom(X,f),Hom(X,g))Hom(X,V) \to IsoIns(Hom(X,f),Hom(X,g))

is an equivalence, where IsoIns(Hom(X,f),Hom(X,g))IsoIns(Hom(X,f),Hom(X,g)) denotes the category whose objects are pairs (u,β)(u,\beta) where u:XAu\colon X\to A is a morphism and β:fugu\beta\colon f u \xrightarrow{\cong} g u is an invertible 2-morphism. If this functor is an isomorphism of categories, then we say that VvAV\xrightarrow{v} 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=()P = (\cdot \rightrightarrows\cdot) and the weight PCatP\to Cat is the diagram

1Iso1 \;\rightrightarrows\; Iso

where 11 is the terminal category and IsoIso is the walking isomorphism.

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


  • 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 IsoIso is equivalent to 11, iso-inserters (but not strict iso-inserters) can equivalently be described as the conical limit of a diagram of shape PP, which might be called a (non-strict) pseudo-equalizer. A strict pseudo-equalizer—that is, a strict pseudolimit of a diagram of shape PP—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.

Last revised on December 14, 2010 at 06:05:20. See the history of this page for a list of all contributions to it.