The complementary notion of -truncated object is that of an n-connected object of an (∞,1)-category.
It makes sense for the following to adopt the convention that is called
-truncated if it is empty or contractible – this is a (-1)-groupoid.
-truncated if it is non-empty and contractible – this is a (-2)-groupoid.
(following HTT, p. 6).
To generalize this, let now be an arbitrary (∞,1)-category. For objects in write ∞ Grpd for the (∞,1)-categorical hom-space (if is given as a simplicially enriched category then this is just the SSet-hom-object which is guaranteed to be a Kan complex).
Using this, it shall be useful to slightly reformulate the above as follows:
(-truncated object in an -category)
This is HTT, def. 18.104.22.168.
A 0-truncated object is also called discrete . Notice that this is categorically discrete as in discrete category, not discrete in the sense of topological spaces. An object in an (∞,1)-topos is discrete in this sense if, regarded as an ∞-groupoid with extra structure it has only trivial morphisms.
By the above convention on (-2)-truncated -groupoids, it is only the terminal objects of that are (-2)-truncated.
Similarly, the (-1)-truncated objects are the subterminal objects.
(-truncated morphism in an -category)
A morphism in an (∞,1)-category is -truncated if for all the postcomposition morphism
is -truncated in ∞Grpd.
By the characterization of homotopy fiber of functor categories this is equivalent to saying that is -truncated when it is so regarded as an object of the over (∞,1)-category .
At least if the ambient (∞,1)-category is even an ∞-stack (∞,1)-topos there is an alternative, more intrinsic, characterization of -truncation in terms of categorical homotopy groups in an (∞,1)-topos:
Then for any this is -truncated precisely if all the categorical homotopy groups above degree are trivial.
This is HTT, prop 22.214.171.124.
Notice that this expected statement does require the assumption that is -truncated for some . Without any a priori truncation assumption on , there is no comparable statement about the relaton to categorical homotopy groups. See HTT, remark 126.96.36.199.
This is HTT, lemma 188.8.131.52.
By definition is -truncated if for each object we have that is -truncated in ∞Grpd. Since the hom-functors preserve (∞,1)-limits, we have in particular that in is -truncated if is -truncated for all in ∞Grpd. Therefore it is sufficient to prove the statement for morphisms in ∞Grpd.
So let now be a morphism of ∞-groupoids. We may find a fibration between Kan complexes in sSet that models in the standard model structure on simplicial sets, and by the standard rules for homotopy pullbacks it follows that the object in -Grpd is then modeled by the ordinary pullback in sSet. And the homotopy fibers of over are then given by the ordinary fibers of in .
We write now for , for simplicity. To see the last statement, let and compute the homotopy pullback
as usual by replacing the right vertical morphism by the fibration and then forming the ordinary pullback. This shows that is equivalent to the space of paths in from to . (Use that gluing of path space objects at endpoints of paths produces a new path space, see for instance section 4 of BrownAHT).
If is connected, then choosing any path gives an isomorphism from the the homotopy groups of to those of the loop space . These latter are indeed those of , shifted down in degree by one (as described for instance at fiber sequence).
If is not connected, we can easily reduce to the case that it is.
This is HTT, prop. 184.108.40.206.
Let be an (∞,1)-topos. For all the class of -truncated morphisms in forms the right class in a orthogonal factorization system in an (∞,1)-category. The left class is that of n-connected morphisms in .
This appears as a remark in HTT, Example 220.127.116.11. A construction of the factorization in terms of a model category presentation is in (Rezk, prop. 8.5). See also n-connected/n-truncated factorization system.
Under mild conditions there is for each a universal way to send an arbitrary object to its -truncation . This is a general version of decategorification where n-morphisms are identified if they are connected by an invertible -morphism.
So for instance for ∞Grpd we have .
This is HTT 18.104.22.168.
Indeed, as the notation suggests, is the essential image of under . The image of an object under this operation is the -truncation of .
So -truncated objects form a reflective sub-(∞,1)-category
A left exact functor between -categories with finite limits sends -truncated objects/morphisms to -truncated objects/morphisms.
This is HTT, prop. 22.214.171.124.6.
Follows from the above recursive characterization of -truncated morphisms by the -truncation of their diagonal, which is preserved by the finite limit preserving .
A presentable -functor between locally presentable (∞,1)-categories and commutes with truncation:
This is HTT, prop. 126.96.36.199.
By the above lemma, restricts to a functor on the truncations. So we need to show that the diagram
in (∞,1)Cat can be filled by a 2-cell. To see this, notice that the adjoint (∞,1)-functor of both composite morphisms exists (because that of exists by the adjoint (∞,1)-functor theorem and bcause adjoints of composites are composites of adjoints) and since the bottom morphism is just the restriction of the top morphism and the right adjoints of the vertical morphisms are full inclusions this adjoint diagram
evidently commutes, since it just expresses this restriction.
This appears as HTT, lemma 188.8.131.52.
First notice that the statement is true for ∞Grpd. For instance we can use the example In ∞Grpd and Top, model ∞-groupoids by Kan complexes and notice that then is given by the truncation functor . This is also a right adjoint and as such preserves in particular product in , which are -products in .
From that we deduce that the statement is true for any (∞,1)-category of (∞,1)-presheaves because all relevant operations there are objectwise those in .
So far this shows even that on presheaf -toposes all products (not necessarily finite) are preserved by truncation.
Let be the product of the objects in question taken in . By the above there we have an equivalence
Now applying to this equivalence and using now that preserves the finite product, this gives an equivalence
in . The claim follows now with the above result that .
By the fact that the truncation functor is a left adjoint one obtains canonical morphisms
For any the sequence
is the Postnikov tower in an (∞,1)-category of . See there for more details.
Discussion of -truncation of types in homotopy type theory via higher inductive types is in (Brunerie). This sends a type to an h-level -type. The -truncation in the context is forming the bracket type hProp.
See at n-truncation modality.
This simple relation between -truncation and categorical homotopy groups is almost, but not exactly true in an arbitrary (∞,1)-topos.
Let be an (∞,1)-topos and an -truncated object.
for we have for the categorical homotopy groups ;
if (for ) , then is in fact -truncated.
If is truncated at all (for any value), then it is -truncated precisely if all categorical homotopy groups vanish for .
Notice. If on the other hand is not truncated at all, then all its homotopy groups may be trivial and may still not be equivalent to the terminal object. This means that Whitehead's theorem may fail in a general (∞,1)-topos for untruncated objects. It holds, however, in hypercomplete (∞,1)-toposes.
A morphism is
hence for all points in the essential image of . For not in the essential image we have . In either case it follows that is 0-truncated.
By def. 3 this is the defining condition for to be 0-truncated.
Then is 0-truncated as a morphism in .
We need to check that for any -stack the morphism is 0-truncated in ∞Grpd. We may choose a cofibrant model for in and by assumption that and is fibrant we have that the ordinary hom of simplicial presheaves is the correct derived hom space morphism. This is itself (the nerve of) a faithful functor, hence the statement follows with prop. 9.
An object in ∞Grpd is -truncated precisely if it is an n-groupoid. To some extent this is so by definition. Equivalently, an object in Top is -truncated if it is (in the equivalence class of) a homotopy n-type.
So we have for a reflective sub-(∞,1)-category
where is the subcategory of on those truncated simplicial sets that are truncations of Kan complexes, regarded as a Kan-complex-enriched category by the embedding via .
induces isomorphisms on homotopy groups for .
This shows that is indeed a full sub-(∞,1)-category of on -truncated objects
Moreover, by the fact discussed at Simplicial and derived adjunctions at adjoint (∞,1)-functor we have that the sSet-enriched adjunction on indeed presents a pair of adjoint (∞,1)-functors on ∞Grpd. So indeed presents the left adjoint to the inclusion .
In ordinary category theory we have that a morphism is a monomorphism (as discussed there), precisely if its diagonal is an isomorphism. Embedded into (∞,1)-category this becomes the special case of prop. 2 for : a morphism is (-1)-truncated (hence a monomorphism in an (∞,1)-category), precisely if its diagonal is (-2)-truncated (hence an equivalence in an (∞,1)-category).
is an -truncated morphism, and precisely if it is -truncated is -truncated.
-truncated morphism / n-connected morphism
|homotopy level||n-truncation||homotopy theory||higher category theory||higher topos theory||homotopy type theory|
|h-level 0||(-2)-truncated||contractible space||(-2)-groupoid||true/unit type/contractible type|
|h-level 1||(-1)-truncated||(-1)-groupoid/truth value||mere proposition, h-proposition|
|h-level 2||0-truncated||discrete space||0-groupoid/set||sheaf||h-set|
|h-level 3||1-truncated||homotopy 1-type||1-groupoid/groupoid||(2,1)-sheaf/stack||h-groupoid|
|h-level 4||2-truncated||homotopy 2-type||2-groupoid||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||h-3-groupoid|
The discussion of truncated objects in an -category is in section 5.5.6 of
The discussion of categorical homotopy groups in an (∞,1)-topos is in section 6.5.1.
A classical article that amplifies the expression of Postnikov towers in terms of coskeletons is
Discussion in the context of homotopy type theory is in