nLab
n-image

Idea

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

Definition

By epi/mono factorization in an $(\mathrm{\infty },1)$-topos

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

$$(\mathrm{Epi}(H),\mathrm{Mono}(H))\subset \mathrm{Mor}(H)\times \mathrm{Mor}(H)$$(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(f)\hookrightarrow Y,$$f : X \to im_1(f) \hookrightarrow Y \,,

we may call ${\mathrm{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:X\to Y$ may be defined as the coequalizer of its kernel pair, hence by the fact that

$$X{\times }_{Y}X\overrightarrow{\to }X\stackrel{}{\to }\mathrm{im}(f)$$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 ”$\mathrm{\infty }$-kernel”, namely of the full Cech nerve simplicial object

$$\cdots \overrightarrow{\overrightarrow{\overrightarrow{\to }}}X{\times }_{Y}X{\times }_{Y}X\overrightarrow{\overrightarrow{\to }}X{\times }_{Y}X\overrightarrow{\to }X\stackrel{}{\to }\mathrm{im}(f).$$\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}(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

$$\begin{array}{ccccc}X{\times }_{\mathrm{im}(f)}X& \to & X& \stackrel{\simeq }{\to }& X\\ \downarrow & & {\downarrow }^f& & {\downarrow }^f\\ X& \stackrel{f}{\to }& \mathrm{im}(f)& \stackrel{\simeq }{\to }& \mathrm{im}(f)\\ {\downarrow }^{\simeq }& & {\downarrow }^{\simeq }& & \downarrow \\ X& \stackrel{f}{\to }& \mathrm{im}(f)& \hookrightarrow & Y\end{array},$$\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 }_{\mathrm{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 }\mathrm{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:X\to Y$ a morphism we have a tower of $n$-images

$$X\simeq {\mathrm{im}}_{\mathrm{\infty }}(f)\to \cdots \to {\mathrm{im}}_2(f)\to {\mathrm{im}}_1(f)\to {\mathrm{im}}_0(f)\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 \mathbb{N}$ the factorization $X\to {\mathrm{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 $H$. Then its internal language is homotopy type theory. We discuss the syntax of 1-images in this theory.

Proposition

If

$$a:A⊢f(a):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

$$(b:B)⊢\left(\right[\sum _{a:A}(b=f(a))]:\mathrm{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 $M$ be a suitable model category presenting $H$. Then by the rules for categorical semantics of identity types and substitution, the interpretation of

$$(b:B),(a:A)⊢((b=f(a)):\mathrm{Type})$$(b:B),\, (a:A) \;\vdash\; ((b = f(a)) : Type)

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

$$\begin{array}{ccc}\tilde{A}& \to & B^I\\ \downarrow & & \downarrow \\ A\times B& \stackrel{(f,{\mathrm{id}}_B)}{\to }& B\times 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 $\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{({\mathrm{id}}_A,f)}{\to }A\times B$. Regarded in the slice category $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 $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(\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 $H$ itself, is the semantics of the non-dependent type

$$⊢\left(\right(\sum _{b:B}[\sum _{a:A}(b=f(a))]):\mathrm{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. 1 as

$$(b:B)⊢(\exists a:A.(b=f(a)):\mathrm{hProp}).$$(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\mid \varphi (b)\}$, so the non-dependent type in Cor. 1 may be written as

$$\{b\in B\mid \exists a\in A.(b=f(a))\}$$\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}(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 \mathrm{Grpd}\hookrightarrow$ ∞Grpd.

Proposition

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

$$f:X\to {\mathrm{im}}_2(f)\to {\mathrm{im}}_1(f)\to Y,$$f \colon X \to im_2(f) \to im_1(f) \to Y \,,

where (up to equivalence of groupoids)

• ${\mathrm{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$;

• ${\mathrm{im}}_2(f)$ 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}(X)$ are equivalent if they have the same domain and codomain in $X$ and if $f(\alpha )=f(\beta )$

  • ${\mathrm{im}}_2(f)\to {\mathrm{im}}_1(f)$ is the identity on objects and the canonical inclusion on sets of morphisms;

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

Proof

Evidently ${\mathrm{im}}_1(f)\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(y)\\ \downarrow & & \downarrow \\ *& \stackrel{y}{\to }& Y\end{array}.$$\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 ${\mathrm{im}}_1(f)\to Y$ are (-1)-truncated objects and the map from homotopy fiber of $f$ to those of ${\mathrm{im}}_1(f)$ is their (-1)-truncation.

Next, the homotopy fibers of ${\mathrm{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(\begin{array}{ccc}{x}_1& \stackrel{[\alpha ]}{\to }& x_2\\ f(x_1)& \stackrel{f(\alpha )}{\to }& f(x_2)\\ \downarrow & & \downarrow \\ y& =& y\end{array}\right).$$\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 ]}{\mathrm{to}}x$ such that $f(\alpha )={\mathrm{id}}_{f(x)}$ 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(f)\to Y$ and hence the latter is indeed the 0-truncation of the former.

Remark

The factroization $f:X\to {\mathrm{im}}_2(f)\to {\mathrm{im}}_1(f)\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.

Related concepts

• image, coimage

• homotopy image

• Postnikov system

• k-ary factorization system