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


By epi/mono factorization in an (,1)(\infty,1)-topos

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

(Epi(H),Mono(H))Mor(H)×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:XYf : X \to Y in H\mathbf{H} with epi-mono factorization

f:Xim 1(f)Y, f : X \to im_1(f) \hookrightarrow Y \,,

we may call im 1(f)Yim_1(f) \hookrightarrow Y the image of ff.

As the ∞-colimit of the kernel ∞-groupoid

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

X× YXXim(f) 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

X× YX× YXX× YXXim(f). \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:Xfim(f)Yf \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

X× im(f)X X X f f X f im(f) im(f) X f im(f) Y, \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× YXX× im(f)XX \times_{Y} X \simeq X \times_{im(f)} X and hence that the Cech nerve of XfYX \stackrel{f}{\to} Y is equivalently that of the effective epimorphism Xfim(f)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 nn-images

More generally for f:XYf \colon X \to Y a morphism we have a tower of nn-images

Xim (f)im 2(f)im 1(f)im 0(f)Y X \simeq im_\infty(f) \to \cdots \to im_2(f) \to im_1(f) \to im_0(f) \simeq Y

factoring ff, such that for each nn \in \mathbb{N} the factorization Xim n+2(f)YX \to im_{n+2}(f) \to Y is the (n-connected, n-truncated) factorization system of ff.

This is the relative Postnikov system of ff.


Syntax in homotopy type theory

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



a:Af(a):B a\colon A \;\vdash \; f(a) \colon B

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

(b:B)([ a:A(b=f(a))]: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).


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

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

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

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

Now the interpretation of the sum a:A\sum_{a:A} is simply that we forget the map to AA (or equivalently compose with the projection A×BBA\times B\to B), regarding A˜\tilde A as an object of M/B\mathbf{M}/B. Of course, this is just a fibration resolution of ff 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(A˜B)im_1(\tilde A \to B), regarded as a dependent type over BB. Thus, it is precisely the the 1-image of ff.

By additionally forgetting the remaining map to BB, we obtain:


In the above situation, the 1-image of ff, regarded as an object of H\mathbf{H} itself, is the semantics of the non-dependent type

(( b:B[ a:A(b=f(a))]):Type). \vdash \; \Big(\Big( \sum_{b:B}\Big[\sum_{a:A} (b = f(a))\Big] \Big) : Type\Big).

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)(a:A.(b=f(a)):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, {bB|ϕ(b)}\{b \in B | \phi(b)\}, so the non-dependent type in Cor. 1 may be written as

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

which is manifestly the naive definition of image.

Compatibility with limits


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

im n(X 1×X 2(f,g))X 2×Y 2)(im n(f)×im n(g)X 2×Y 2). 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) \,.

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

X 1×Y 1 (id,g) (f,id) X 1×Y 2 X 2×Y 1 (f,id) (id,g) X 2×Y 2 \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, nn-truncation in the slice \infty-topos preserves products, so that

im n(f,g) =τ n(f,g) τ n((f,id)× X 2×Y 1(id,g)) (τ n(f,id))× X 2×Y 2(τ n(id,g)) (im nf,id)× X 2×Y 2(id,im ng) (im nf,im ng). \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} \,.

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

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

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

Ωf: ΩX im n(Ωf) ΩY id *: * im n+1(id *)* * f: X im n+1(f) Y \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 }



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

*VObj κ * \stackrel{\vdash V}{\to} Obj_\kappa

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

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,YGrpdX, Y \in Grpd \hookrightarrow ∞Grpd.


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

f:Xim 2(f)im 1(f)Y, f \colon X \to im_2(f) \to im_1(f) \to Y \,,

where (up to equivalence of groupoids)

  • im 1(f)Yim_1(f) \to Y is the full subgroupoid of YY on those objects yy such that there is an object xXx \in X with f(x)yf(x) \simeq y;

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

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

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


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

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

If there is no xXx \in X such that f(x)yf(x) \simeq y then fiber F yF_y is empty set. If there is such xx then the fiber is the groupoid with that one object and all morphisms in XX 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)Yim_1(f) \to Y are (-1)-truncated objects and the map from homotopy fiber of ff to those of im 1(f)im_1(f) is their (-1)-truncation.

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

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

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


The factroization f:Xim 2(f)im 1(f)Yf \colon X \to im_2(f) \to im_1(f) \to Y of prop. 4 exhibits a ternary factorization system in Grpd.


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


Discussion of nn-image factorization in homotopy type theory is in

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

Revised on February 2, 2017 11:28:12 by Urs Schreiber (