# nLab n-image

### Context

#### $\left(\infty ,1\right)$-Category theory

(∞,1)-category theory

# Contents

## Idea

The generalization of the notion of image from category theory to (∞,1)-category theory.

## Definition

### By epi/mono factorization in an $\left(\infty ,1\right)$-topos

Let $H$ be an (∞,1)-topos. Then by the discussion at (n-connected, n-truncated) factorization system there is a orthogonal factorization system

$\left(\mathrm{Epi}\left(H\right),\mathrm{Mono}\left(H\right)\right)\subset \mathrm{Mor}\left(H\right)×\mathrm{Mor}\left(H\right)$(Epi(\mathbf{H}), Mono(\mathbf{H})) \subset Mor(\mathbf{H}) \times Mor(\mathbf{H})

whose left class consists of the (-1)-connected morphisms , the (∞,1)-effective epimorphisms, while the right class consists of the (-1)-truncated morphisms morphisms, hence the (∞,1)-monomorphisms.

So given a morphism $f:X\to Y$ in $H$ with epi-mono factorization

$f:X\to {\mathrm{im}}_{1}\left(f\right)↪Y\phantom{\rule{thinmathspace}{0ex}},$f : X \to im_1(f) \hookrightarrow Y \,,

we may call ${\mathrm{im}}_{1}\left(f\right)↪Y$ the image of $f$.

### As the ∞-colimit of the kernel ∞-groupoid

In a sufficiently well-behaved 1-category, the (co)image of a morphism $f:X\to Y$ may be defined as the coequalizer of its kernel pair, hence by the fact that

$X{×}_{Y}X\stackrel{\to }{\to }X\stackrel{}{\to }\mathrm{im}\left(f\right)$X \times_Y X \stackrel{\to}{\to} X \stackrel{}{\to} im(f)

is a colimiting cocone under the parallel morphism diagram.

In an (∞,1)-topos the 1-image is the (∞,1)-colimit not just of these two morphisms, but of the full ”$\infty$-kernel”, namely of the full Cech nerve simplicial object

$\cdots \stackrel{\to }{\stackrel{\to }{\stackrel{\to }{\to }}}X{×}_{Y}X{×}_{Y}X\stackrel{\to }{\stackrel{\to }{\to }}X{×}_{Y}X\stackrel{\to }{\to }X\stackrel{}{\to }\mathrm{im}\left(f\right)\phantom{\rule{thinmathspace}{0ex}}.$\cdots \stackrel{\to}{\stackrel{\to}{\stackrel{\to}{\to}}} X \times_Y X \times_Y X \stackrel{\to}{\stackrel{\to}{\to}} X \times_Y X \stackrel{\to}{\to} X \stackrel{}{\to} im(f) \,.

(Here all degeneracy maps are notionally suppressed.)

To see that this gives the same notion of image as given by the epi-mono factorization as discussed above, let $f:X\stackrel{f}{\to }\mathrm{im}\left(f\right)↪Y$ be such a factorization. Then using (by the discussion at truncated morphism – Recursive characterization) that the (∞,1)-pullback of a monomorphism is its domain, we find a pasting diagram of (∞,1)-pullback squares of the form

$\begin{array}{ccccc}X{×}_{\mathrm{im}\left(f\right)}X& \to & X& \stackrel{\simeq }{\to }& X\\ ↓& & {↓}^{f}& & {↓}^{f}\\ X& \stackrel{f}{\to }& \mathrm{im}\left(f\right)& \stackrel{\simeq }{\to }& \mathrm{im}\left(f\right)\\ {↓}^{\simeq }& & {↓}^{\simeq }& & ↓\\ X& \stackrel{f}{\to }& \mathrm{im}\left(f\right)& ↪& Y\end{array}\phantom{\rule{thinmathspace}{0ex}},$\array{ X \times_{im(f)} X &\to & X &\stackrel{\simeq}{\to} & X \\ \downarrow && \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{f}} \\ X &\stackrel{f}{\to}& im(f) &\stackrel{\simeq}{\to}& im(f) \\ \downarrow^{\mathrlap{\simeq}} && \downarrow^{\mathrlap{\simeq}} && \downarrow \\ X &\stackrel{f}{\to}& im(f) &\hookrightarrow& Y } \,,

which shows, by the pasting law, that $X{×}_{Y}X\simeq X{×}_{\mathrm{im}\left(f\right)}X$ and hence that the Cech nerve of $X\stackrel{f}{\to }Y$ is equivalently that of the effective epimorphism $X\stackrel{f}{\to }\mathrm{im}\left(f\right)$. Now, by one of the Giraud-Rezk-Lurie axioms satisfied by (∞,1)-toposes, the (∞,1)-colimit over the Cech nerve of an effective epimorphism is that morphism itself. Therefore the 1-image defined this way coincides with the one defined by the epi/mono factorization.

### Tower of $n$-images

More generally for $f:X\to Y$ a morphism we have a tower of $n$-images

$X\simeq {\mathrm{im}}_{\infty }\left(f\right)\to \cdots \to {\mathrm{im}}_{2}\left(f\right)\to {\mathrm{im}}_{1}\left(f\right)\to {\mathrm{im}}_{0}\left(f\right)\simeq Y$X \simeq im_\infty(f) \to \cdots \to im_2(f) \to im_1(f) \to im_0(f) \simeq Y

factoring $f$, such that for each $n\in ℕ$ the factorization $X\to {\mathrm{im}}_{n+2}\left(f\right)\to Y$ is the (n-connected, n-truncated) factorization system of $f$.

This is the relative Postnikov system of $f$.

## Properties

### Syntax in homotopy type theory

Let the ambient (∞,1)-category be an (∞,1)-topos $H$. Then its internal language is homotopy type theory. We discuss the syntax of 1-images in this theory.

###### Proposition

If

$a:A\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}f\left(a\right):B$a\colon A \;\vdash \; f(a) \colon B

is a term whose categorical semantics is a morphism $A\stackrel{f}{\to }B$ in $H$, then the 1-image of that morphism, when regarded as an object of $H/B$, is the categorical semantics of the dependent type

$\left(b:B\right)\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}\left(\left[\sum _{a:A}\left(b=f\left(a\right)\right)\right]:\mathrm{Type}\right).$(b:B) \; \vdash \; \Big(\Big[ \sum_{a \colon A} (b = f(a)) \Big] : Type\Big).

Here $=$ denotes the identity type or “path type”, $\sum$ denotes the dependent sum type, and $\left[-\right]$ denotes the bracket type (which is constructible in homotopy type theory either as a higher inductive type or using the univalence axiom and a resizing rule to obtain a subobject classifier).

###### Proof

Let $M$ be a suitable model category presenting $H$. Then by the rules for categorical semantics of identity types and substitution, the interpretation of

$\left(b:B\right),\phantom{\rule{thinmathspace}{0ex}}\left(a:A\right)\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}\left(\left(b=f\left(a\right)\right):\mathrm{Type}\right)$(b:B),\, (a:A) \;\vdash\; ((b = f(a)) : Type)

in $M$ a is the following pullback $\stackrel{˜}{A}$ (see homotopy pullback for more details):

$\begin{array}{ccc}\stackrel{˜}{A}& \to & {B}^{I}\\ ↓& & ↓\\ A×B& \stackrel{\left(f,{\mathrm{id}}_{B}\right)}{\to }& B×B\end{array}.$\array{ \tilde A &\to& B^{I} \\ \downarrow && \downarrow \\ A \times B &\stackrel{(f,id_B)}{\to}& B \times B }.

Here all objects now denote fibrant object representatives of the given objects in $H$, and the right-hand morphism is the fibration out of a path space object for $B$. By the factorization lemma the composite $\stackrel{˜}{A}\to A×B\to B$ here is a fibration resolution of the original $A\stackrel{f}{\to }B$ and $\stackrel{˜}{A}\to A×B$ is a fibration resolution of $A\stackrel{\left({\mathrm{id}}_{A},f\right)}{\to }A×B$. Regarded in the slice category $M/\left(A×B\right)$, this now interprets the syntax $\left(b=f\left(a\right)\right)$ as an $\left(A×B\right)$-dependent type.

Now the interpretation of the sum ${\sum }_{a:A}$ is simply that we forget the map to $A$ (or equivalently compose with the projection $A×B\to B$), regarding $\stackrel{˜}{A}$ as an object of $M/B$. Of course, this is just a fibration resolution of $f$ itself.

Finally, the interpretation of the bracket type of this is precisely the (-1)-truncation of this morphism, which by the discussion there is its 1-image ${\mathrm{im}}_{1}\left(\stackrel{˜}{A}\to B\right)$, regarded as a dependent type over $B$. Thus, it is precisely the the 1-image of $f$.

By additionally forgetting the remaining map to $B$, we obtain:

###### Corollary

In the above situation, the 1-image of $f$, regarded as an object of $H$ itself, is the semantics of the non-dependent type

$⊢\phantom{\rule{thickmathspace}{0ex}}\left(\left(\sum _{b:B}\left[\sum _{a:A}\left(b=f\left(a\right)\right)\right]\right):\mathrm{Type}\right).$\vdash \; \Big(\Big( \sum_{b:B}\Big[\sum_{a:A} (b = f(a))\Big] \Big) : Type\Big).
###### Remark

The bracket type of a dependent sum is the propositions as some types version of the existential quantifier, so we can write the dependent type in Prop. 1 as

$\left(b:B\right)\phantom{\rule{thickmathspace}{0ex}}⊢\phantom{\rule{thickmathspace}{0ex}}\left(\exists a:A.\left(b=f\left(a\right)\right)\phantom{\rule{thickmathspace}{0ex}}:\phantom{\rule{thickmathspace}{0ex}}\mathrm{hProp}\right).$(b:B) \; \vdash \; \left(\exists a:A . (b = f(a)) \;:\; hProp\right).

The dependent sum of an h-proposition is then the propositions-as-some-types version of the comprehension rule?, $\left\{b\in B\mid \varphi \left(b\right)\right\}$, so the non-dependent type in Cor. 1 may be written as

$\left\{b\in B\phantom{\rule{thinmathspace}{0ex}}\mid \phantom{\rule{thinmathspace}{0ex}}\exists a\in A.\left(b=f\left(a\right)\right)\right\}$\left\{ b \in B \,|\, \exists a \in A . (b = f(a)) \right\}

which is manifestly the naive definition of image.

## Examples

### Automorphisms

Let $V\in H$ be a $\kappa$-small object, and let

$*\stackrel{⊢V}{\to }{\mathrm{Obj}}_{\kappa }$* \stackrel{\vdash V}{\to} Obj_\kappa

the corresponding morphism to the object classifier. Then the 1-image of this is $B\mathrm{Aut}\left(V\right)$, the delooping of the internal automorphism ∞-group of $V$.

### Of functors between groupoids

The simplest nontivial case of higher images after the ordinary case of images of functions of sets is images of functors between groupoids hence betwee 1-truncated objects $X,Y\in \mathrm{Grpd}↪$ ∞Grpd.

###### Proposition

For $f:X\to Y$ a functor between groupoids, its image factorization is

$f:X\to {\mathrm{im}}_{2}\left(f\right)\to {\mathrm{im}}_{1}\left(f\right)\to Y\phantom{\rule{thinmathspace}{0ex}},$f \colon X \to im_2(f) \to im_1(f) \to Y \,,

where (up to equivalence of groupoids)

• ${\mathrm{im}}_{1}\left(f\right)\to Y$ is the full subgroupoid of $Y$ on those objects $y$ such that there is an object $x\in X$ with $f\left(x\right)\simeq y$;

• ${\mathrm{im}}_{2}\left(f\right)$ is the gorupoid whose objecs are those of $X$ and whose morphisms are equivalence classes of morphisms in $X$ where $\alpha ,\beta \in \mathrm{Mor}\left(X\right)$ are equivalent if they have the same domain and codomain in $X$ and if $f\left(\alpha \right)=f\left(\beta \right)$

• ${\mathrm{im}}_{2}\left(f\right)\to {\mathrm{im}}_{1}\left(f\right)$ is the identity on objects and the canonical inclusion on sets of morphisms;

• $X\to {\mathrm{im}}_{2}\left(f\right)$ is the identity on objects and the defining quotient map on sets of morphisms.

###### Proof

Evidently ${\mathrm{im}}_{1}\left(f\right)\to Y$ is a fibration (isofibration) and so the homotopy fiber over every point is given by the 1-categorical pullback

$\begin{array}{ccc}{F}_{y}& \to & {\mathrm{im}}_{1}\left(y\right)\\ ↓& & ↓\\ *& \stackrel{y}{\to }& Y\end{array}\phantom{\rule{thinmathspace}{0ex}}.$\array{ F_y &\to& im_1(y) \\ \downarrow && \downarrow \\ * &\stackrel{y}{\to}& Y } \,.

If there is no $x\in X$ such that $f\left(x\right)\simeq y$ then fiber ${F}_{y}$ is empty set. If there is such $x$ then the fiber is the groupoid with that one object and all morphisms in $X$ on that object which are mapped to the identity morphism, which by construction is only the identity morphism itself, hence the fiber is the point. Hence indeed the homotopy fibers of ${\mathrm{im}}_{1}\left(f\right)\to Y$ are (-1)-truncated objects and the map from homotopy fiber of $f$ to those of ${\mathrm{im}}_{1}\left(f\right)$ is their (-1)-truncation.

Next, the homotopy fibers of ${\mathrm{im}}_{2}\left(f\right)\to Y$ over a point $y\in Y$ are the groupoids whose objects are pairs $\left(x,\left(f\left(x\right)\to y\right)\right)$ and whose morphisms are pairs

$\left(\begin{array}{ccc}{x}_{1}& \stackrel{\left[\alpha \right]}{\to }& {x}_{2}\\ f\left({x}_{1}\right)& \stackrel{f\left(\alpha \right)}{\to }& f\left({x}_{2}\right)\\ ↓& & ↓\\ y& =& y\end{array}\right)\phantom{\rule{thinmathspace}{0ex}}.$\left( \array{ x_1 &\stackrel{[\alpha]}{\to}& x_2 \\ f(x_1) &\stackrel{f(\alpha)}{\to}& f(x_2) \\ \downarrow && \downarrow \\ y &=& y } \right) \,.

Notice first that the above is 0-truncated: an automorphism of $\left(x,\left(f\left(x\right)\to y\right)\right)$ is of the form $x\stackrel{\left[\alpha \right]}{\mathrm{to}}x$ such that $f\left(\alpha \right)={\mathrm{id}}_{f\left(x\right)}$ and so there is precisely one such, namely the equivalence class of ${\mathrm{id}}_{x}$.

Notice second that the homotopy fibers of $f$ itself have the same form, only that $\alpha :{x}_{1}\to {x}_{2}$ appears itself, not as its equivalence class. Also if two objects in the homotopy fiber of $f$ are connected by a morphism, then by construction so they are in the homotopy fiber of ${\mathrm{im}}_{2}\left(f\right)\to Y$ and hence the latter is indeed the 0-truncation of the former.

###### Remark

The factroization $f:X\to {\mathrm{im}}_{2}\left(f\right)\to {\mathrm{im}}_{1}\left(f\right)\to Y$ of prop. 2 exhibits a ternary factorization system in Grpd.

###### Remark

This situation can also be considered from the perspective of the formalization of stuff, structure, property. See there at A factorization system.

Revised on November 30, 2012 01:55:21 by Urs Schreiber (82.169.65.155)