equivalences in/of $(\infty,1)$-categories
The generalization of the notion of image from category theory to (∞,1)-category theory.
Let $\mathbf{H}$ be an (∞,1)-topos. Then by the discussion at (n-connected, n-truncated) factorization system there is a orthogonal factorization system
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
we may call $im_1(f) \hookrightarrow Y$ the image of $f$.
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
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
(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
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.
More generally for $f \colon X \to Y$ a morphism we have a tower of $n$-images
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$.
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.
If
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
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 $\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
in $\mathbf{M}$ a is the following pullback $\tilde A$ (see homotopy pullback for more details):
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:
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
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
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. 1 may be written as
which is manifestly the naive definition of image.
In an (∞,1)-topos $\mathbf{H}$, the $n$-image of a product is the product of $n$-images:
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
But by this proposition, $n$-truncation in the slice $\infty$-topos preserves products, so that
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
i.e. we have the following diagram, where the columns are homotopy fiber sequences
Let $V \in \mathbf{H}$ be a $\kappa$-small object, and let
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$.
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.
For $f \colon X \to Y$ a functor between groupoids, its image factorization is
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.
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
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
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.
The factroization $f \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 $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