Background
Basic concepts
equivalences in/of -categories
Universal constructions
Local presentation
Theorems
Extra stuff, structure, properties
Models
The generalization of the notion of image from category theory to (∞,1)-category theory.
Let 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 in with epi-mono factorization
we may call the image of .
In a sufficiently well-behaved 1-category, the (co)image of a morphism 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 “-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 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 and hence that the Cech nerve of is equivalently that of the effective epimorphism . 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 a morphism we have a tower of -images
factoring , such that for each the factorization is the (n-connected, n-truncated) factorization system of .
This is the relative Postnikov system of .
Let the ambient (∞,1)-category be an (∞,1)-topos . 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 in , then the 1-image of that morphism, when regarded as an object of , is the categorical semantics of the dependent type
Here
denotes the dependent pair type,
“” denotes the identification type,
denotes the bracket type (which is constructible in homotopy type theory either as a higher inductive type as described at n-truncation modalitym or using the univalence axiom and a resizing rule to obtain a subobject classifier).
Let be a suitable model category presenting . Then by the rules for categorical semantics of identity types and substitution, the interpretation of
in a is the following pullback (see homotopy pullback for more details):
Here all objects now denote fibrant object representatives of the given objects in , and the right-hand morphism is the fibration out of a path space object for . By the factorization lemma the composite here is a fibration resolution of the original and is a fibration resolution of . Regarded in the slice category , this now interprets the syntax as an -dependent type.
Now the interpretation of the sum is simply that we forget the map to (or equivalently compose with the projection ), regarding as an object of . Of course, this is just a fibration resolution of 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 , regarded as a dependent type over . Thus, it is precisely the the 1-image of .
By additionally forgetting the remaining map to , we obtain:
In the above situation, the 1-image of , regarded as an object of 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. as
The dependent sum of an h-proposition is then the propositions-as-some-types version of the comprehension rule, , so the non-dependent type in Cor. may be written as
which is manifestly the naive definition of image.
In an (∞,1)-topos , the -image of a product is the product of -images:
The morphism is the product of with in the slice (∞,1)-topos over , namely there is a homotopy fiber product in of the form
But by this proposition, -truncation in the slice -topos preserves products, so that
The -image of the looping of a morphism of pointed objects is the looping of its -image
i.e. we have the following diagram, where the columns are homotopy fiber sequences
Let be a -small object, and let
the corresponding morphism to the object classifier. Then the 1-image of this is , the delooping of the internal automorphism ∞-group of .
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 ∞Grpd.
For a functor between groupoids, its image factorization is
where (up to equivalence of groupoids)
is the full subgroupoid of on those objects such that there is an object with ;
is the groupoid whose objecs are those of and whose morphisms are equivalence classes of morphisms in where are equivalent if they have the same domain and codomain in and if
is the identity on objects and the canonical inclusion on sets of morphisms;
is the identity on objects and the defining quotient map on sets of morphisms.
Evidently is a fibration (isofibration) and so the homotopy fiber over every point is given by the 1-categorical pullback
If there is no such that then fiber is empty set. If there is such then the fiber is the groupoid with that one object and all morphisms in 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 are (-1)-truncated objects and the map from homotopy fiber of to those of is their (-1)-truncation.
Next, the homotopy fibers of over a point are the groupoids whose objects are pairs and whose morphisms are pairs
Notice first that the above is 0-truncated: an automorphism of is of the form such that and so there is precisely one such, namely the equivalence class of .
Notice second that the homotopy fibers of itself have the same form, only that appears itself, not as its equivalence class. Also if two objects in the homotopy fiber of are connected by a morphism, then by construction so they are in the homotopy fiber of and hence the latter is indeed the 0-truncation of the former.
The factroization of prop. 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 -image factorization in homotopy type theory is in
A construction of -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 January 29, 2023 at 19:09:43. See the history of this page for a list of all contributions to it.