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
Last revised on February 2, 2017 at 11:28:12. See the history of this page for a list of all contributions to it.