# nLab n-image

Contents

### Context

#### $(\infty,1)$-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 $(\infty,1)$-topos

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

$(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 $\mathbf{H}$ with epi-mono factorization

$f : X \to im_1(f) \hookrightarrow Y \,,$

we may call $im_1(f) \hookrightarrow 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 \colon X \to Y$ may be defined as the coequalizer of its kernel pair, hence by the fact that

$X \times_Y X \stackrel{\longrightarrow}{\longrightarrow} X \stackrel{}{\longrightarrow} 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{\longrightarrow}{\stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}}} X \times_Y X \times_Y X \stackrel{\longrightarrow}{\stackrel{\longrightarrow}{\longrightarrow}} X \times_Y X \stackrel{\longrightarrow}{\longrightarrow} X \stackrel{}{\longrightarrow} 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 \colon X \stackrel{f}{\longrightarrow} im(f) \hookrightarrow 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

$\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 \times_{Y} X \simeq X \times_{im(f)} X$ and hence that the Cech nerve of $X \stackrel{f}{\to} Y$ is equivalently that of the effective epimorphism $X \stackrel{f}{\to} im(f)$. 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 \colon X \to Y$ a morphism we have a tower of $n$-images

$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 \mathbb{N}$ the factorization $X \to im_{n+2}(f) \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 $\mathbf{H}$. Then its internal language is homotopy type theory. We discuss the syntax of 1-images in this theory.

###### Proposition

If

$a\colon A \;\vdash \; f(a) \colon B$

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

$(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 $[-]$ 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 $\mathbf{M}$ be a suitable model category presenting $\mathbf{H}$. Then by the rules for categorical semantics of identity types and substitution, the interpretation of

$(b:B),\, (a:A) \;\vdash\; ((b = f(a)) : Type)$

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

$\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 $\mathbf{H}$, and the right-hand morphism is the fibration out of a path space object for $B$. By the factorization lemma the composite $\tilde A \to A \times B \to B$ here is a fibration resolution of the original $A \stackrel{f}{\to} B$ and $\tilde A \to A \times B$ is a fibration resolution of $A \stackrel{(id_A,f)}{\to} A \times B$. Regarded in the slice category $\mathbf{M}/(A \times B)$, this now interprets the syntax $(b = f(a))$ as an $(A \times B)$-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\times B\to B$), regarding $\tilde A$ as an object of $\mathbf{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 $im_1(\tilde A \to B)$, 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 $\mathbf{H}$ itself, is the semantics of the non-dependent type

$\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. as

$(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, $\{b \in B | \phi(b)\}$, so the non-dependent type in Cor. may be written as

$\left\{ b \in B \,|\, \exists a \in A . (b = f(a)) \right\}$

which is manifestly the naive definition of image.

### Compatibility with limits

###### Proposition

In an (∞,1)-topos $\mathbf{H}$, the $n$-image of a product is the product of $n$-images:

$im_n\left(X_1 \times X_2 \stackrel{(f,g)}{\longrightarrow}) X_2 \times Y_2\right) \simeq \left( im_n(f) \times im_n(g) \longrightarrow X_2 \times Y_2 \right) \,.$
###### Proof

The morphism $(f,g)$ is the product of $(f,id)$ with $(g,id)$ in the slice (∞,1)-topos over $X_2 \times Y_2$, namely there is a homotopy fiber product in $\mathbf{H}$ of the form

$\array{ && X_1 \times Y_1 \\ & {}^{\mathllap{(id,g)}}\swarrow && \searrow^{\mathrlap{(f,id)}} \\ X_1 \times Y_2 && \swArrow_{\simeq} && X_2 \times Y_1 \\ & {}_{\mathllap{(f,id)}}\searrow && \swarrow_{\mathrlap{(id,g)}} \\ && X_2 \times Y_2 }$

But by this proposition, $n$-truncation in the slice $\infty$-topos preserves products, so that

\begin{aligned} im_n(f,g) & = \tau_n (f,g) \\ & \simeq \tau_n ((f,id)\times_{X_2 \times Y_1} (id,g)) \\ &\simeq (\tau_n(f,id)) \times_{X_2 \times Y_2} (\tau_n(id,g)) \\ & \simeq (im_n f, id)\times_{X_2 \times Y_2} (id, im_n g) \\ & \simeq (im_n f, im_n g) \end{aligned} \,.
###### Proposition

The $n$-image of the looping of a morphism $f \colon X \to Y$ of pointed objects is the looping of its $(n+1)$-image

$im_n (\Omega(f)) \simeq \Omega(im_{n+1}(f)) \,.$

i.e. we have the following diagram, where the columns are homotopy fiber sequences

$\array{ \Omega f \colon & \Omega X &\longrightarrow& im_n(\Omega f) &\longrightarrow& \Omega Y \\ & \downarrow && \downarrow && \downarrow \\ id_\ast \colon & \ast &\longrightarrow & im_{n+1}(id_\ast) \simeq \ast &\longrightarrow& \ast \\ & \downarrow && \downarrow && \downarrow \\ f\colon & X &\stackrel{}{\longrightarrow}& im_{n+1}(f) &\stackrel{}{\longrightarrow}& Y }$

## Examples

### Automorphisms

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

$* \stackrel{\vdash V}{\to} Obj_\kappa$

the corresponding morphism to the object classifier. Then the 1-image of this is $\mathbf{B}\mathbf{Aut}(V)$, 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 Grpd \hookrightarrow$ ∞Grpd.

###### Proposition

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

$f \colon X \to im_2(f) \to im_1(f) \to Y \,,$

where (up to equivalence of groupoids)

• $im_1(f) \to Y$ is the full subgroupoid of $Y$ on those objects $y$ such that there is an object $x \in X$ with $f(x) \simeq y$;

• $im_2(f)$ is the groupoid whose objecs are those of $X$ and whose morphisms are equivalence classes of morphisms in $X$ where $\alpha,\beta \in Mor(X)$ are equivalent if they have the same domain and codomain in $X$ and if $f(\alpha) = f(\beta)$

• $im_2(f)\to im_1(f)$ is the identity on objects and the canonical inclusion on sets of morphisms;

• $X \to im_2(f)$ is the identity on objects and the defining quotient map on sets of morphisms.

###### Proof

Evidently $im_1(f) \to Y$ is a fibration (isofibration) and so the homotopy fiber over every point is given by the 1-categorical pullback

$\array{ F_y &\to& im_1(y) \\ \downarrow && \downarrow \\ * &\stackrel{y}{\to}& Y } \,.$

If there is no $x \in X$ such that $f(x) \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 $im_1(f) \to Y$ are (-1)-truncated objects and the map from homotopy fiber of $f$ to those of $im_1(f)$ is their (-1)-truncation.

Next, the homotopy fibers of $im_2(f) \to Y$ over a point $y \in Y$ are the groupoids whose objects are pairs $(x, (f(x) \to y))$ and whose morphisms are pairs

$\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 $(x,(f(x) \to y))$ is of the form $x \stackrel{[\alpha]}{to} x$ such that $f(\alpha) = id_{f(x)}$ and so there is precisely one such, namely the equivalence class of $id_x$.

Notice second that the homotopy fibers of $f$ itself have the same form, only that $\alpha \colon 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 $im_2(f) \to Y$ and hence the latter is indeed the 0-truncation of the former.

###### Remark

The factroization $f \colon X \to im_2(f) \to im_1(f) \to Y$ of prop. 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.

## References

Discussion of $n$-image factorization in homotopy type theory is in

A construction of $n$-image factorizations in homotopy type theory using only homotopy pushouts and specifically joins (instead of more general higher inductive types) is described in

Last revised on February 2, 2017 at 11:28:12. See the history of this page for a list of all contributions to it.