7.3 Truncations


In §3.7 (http://planetmath.org/37propositionaltruncation) we introduced the propositional truncation, which makes the “best approximation” of a type that is a mere proposition, i.e. a (-1)-type. In §6.9 (http://planetmath.org/69truncations) we constructed this truncation as a higher inductive type, and gave one way to generalize it to a 0-truncation. We now explain a better generalizationPlanetmathPlanetmath of this, which truncates any type into an n-type for any n-2; in classical homotopy theory this would be called its nth Postnikov section.

The idea is to make use of (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem# utoref), which states that A is an n-type just when Ωn+1(A,a) is contractibleMathworldPlanetmath for all a:A, and Lemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3), which implies that Ωn+1(A,a)𝖬𝖺𝗉*(𝕊n+1,(A,a)), where 𝕊n+1 is equipped with some basepoint which we may as well call 𝖻𝖺𝗌𝖾. However, contractibility of 𝖬𝖺𝗉*(𝕊n+1,(A,a)) is something that we can ensure directly by giving path constructors.

We might first of all try to define An to be generated by a function ||n:AAn, together with for each r:𝕊n+1An and each x:𝕊n+1, a path sr(x):r(x)=r(𝖻𝖺𝗌𝖾). But this does not quite work, for the same reason that Remark 6.7.1 (http://planetmath.org/67hubsandspokes#Thmprermk1) fails. Instead, we use the full “hub and spoke” construction as in §6.7 (http://planetmath.org/67hubsandspokes).

Thus, for n-1, we take An to be the higher inductive type generated by:

  • a function ||n:AAn,

  • for each r:𝕊n+1An, a hub point h(r):An, and

  • for each r:𝕊n+1An and each x:𝕊n+1, a spoke path sr(x):r(x)=h(r).

The existence of these constructors is now enough to show:

Lemma 7.3.1.

An is an n-type.

Proof.

By (http://planetmath.org/72uniquenessofidentityproofsandhedbergstheorem# utoref), it suffices to show that Ωn+1(An,b) is contractible for all b:An, which by Lemma 6.5.4 (http://planetmath.org/65suspensions#Thmprelem3) is equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath to 𝖬𝖺𝗉*(𝕊n+1,(An,b)). As center of contraction for the latter, we choose the function cb:𝕊n+1An which is constant at b, together with 𝗋𝖾𝖿𝗅b:cb(𝖻𝖺𝗌𝖾)=b.

Now, an arbitrary element of 𝖬𝖺𝗉*(𝕊n+1,(An,b)) consists of a map r:𝕊n+1An together with a path p:r(𝖻𝖺𝗌𝖾)=b. By function extensionality, to show r=cb it suffices to give, for each x:𝕊n+1, a path r(x)=cb(x)b. We choose this to be the composite sr(x)\centerdotsr(𝖻𝖺𝗌𝖾)-1\centerdotp, where sr(x) is the spoke at x.

Finally, we must show that when transported along this equality r=cb, the path p becomes 𝗋𝖾𝖿𝗅b. By transport in path types, this means we need

(sr(𝖻𝖺𝗌𝖾)\centerdotsr(𝖻𝖺𝗌𝖾)-1\centerdotp)-1\centerdotp=𝗋𝖾𝖿𝗅b.

But this is immediate from path operationsMathworldPlanetmath. ∎

(This construction fails for n=-2, but in that case we can simply define A-2:𝟏 for all A. From now on we assume n-1.)

To show the desired universal propertyMathworldPlanetmath of the n-truncation, we need the inductionMathworldPlanetmath principle. We extract this from the constructors in the usual way; it says that given P:An𝒰 together with

  • For each a:A, an element g(a):P(|a|n),

  • For each r:𝕊n+1An and r:(x:𝕊n+1)P(r(x)), an element h(r,r):P(h(r)),

  • For each r:𝕊n+1An and r:(x:𝕊n+1)P(r(x)), and each x:𝕊n+1, a dependent path r(x)=sr(x)Ph(r,r),

there exists a sectionMathworldPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath f:(x:An)P(x) with f(|a|n)g(a) for all a:A. To make this more useful, we reformulate it as follows.

Theorem 7.3.2.

For any type family P:AnU such that each P(x) is an n-type, and any function g:(a:A)P(|a|n), there exists a section f:(x:An)P(x) such that f(|a|n):g(a) for all a:A.

Proof.

It will suffice to construct the second and third data listed above, since g has exactly the type of the first datum. Given r:𝕊n+1An and r:(x:𝕊n+1)P(r(x)), we have h(r):An and sr:(x:𝕊n+1)(r(x)=h(r)). Define t:𝕊n+1P(h(r)) by t(x):sr(x)*(r(x)). Then since P(h(r)) is n-truncated, there exists a point u:P(h(r)) and a contraction v:(x:𝕊n+1)(t(x)=u). Define h(r,r):u, giving the second datum. Then (recalling the definition of dependent paths), v has exactly the type required of the third datum. ∎

In particular, if E is some n-type, we can consider the constant family of types equal to E for every point of A. Thus, every map f:AE can be extended to a map 𝖾𝗑𝗍(f):AnE defined by 𝖾𝗑𝗍(f)(|a|n):f(a); this is the recursion principle for An.

The induction principle also implies a uniqueness principle for functions of this form. Namely, if E is an n-type and g,g:AnE are such that g(|a|n)=g(|a|n) for every a:A, then g(x)=g(x) for all x:An, since the type g(x)=g(x) is an n-type. Thus, g=g. This yields the following universal property.

Lemma 7.3.3 (Universal property of truncations).

Let n-2, A:U and B:n-Type. The following map is an equivalence:

{(AnB)(AB)gg||n
Proof.

Given that B is n-truncated, any f:AB can be extended to a map 𝖾𝗑𝗍(f):AnB. The map 𝖾𝗑𝗍(f)||n is equal to f, because for every a:A we have 𝖾𝗑𝗍(f)(|a|n)=f(a) by definition. And the map 𝖾𝗑𝗍(g||n) is equal to g, because they both send |a|n to g(|a|n). ∎

In categoricalPlanetmathPlanetmath languagePlanetmathPlanetmath, this says that the n-types form a reflective subcategory of the categoryMathworldPlanetmath of types. (To state this fully precisely, one ought to use the language of (,1)-categories.) In particular, this implies that the n-truncation is functorial: given f:AB, applying the recursion principle to the composite A𝑓BBn yields a map fn:AnBn. By definition, we have a homotopyMathworldPlanetmath

𝗇𝖺𝗍nf:a:Afn(|a|n)=|f(a)|n, (7.3.4)

expressing naturality of the maps ||n.

Uniqueness implies functoriality laws such as gfn=gnfn and 𝗂𝖽An=𝗂𝖽An, with attendant coherence laws. We also have higher functoriality, for instance:

Lemma 7.3.5.

Given f,g:AB and a homotopy h:fg, there is an induced homotopy hn:fngn such that the composite

\includegraphicsHoTTfig7.3.1.png (7.3.5)

is equal to ap||n(h(a)).

Proof.

First, we indeed have a homotopy with components 𝖺𝗉||n(h(a)):|f(a)|n=|g(a)|n. Composing on either sides with the paths |f(a)|n=fn(|a|n) and |g(a)|n=gn(|a|n), which arise from the definitions of fn and gn, we obtain a homotopy (fn||n)(gn||n), and hence an equality by function extensionality. But since (||n) is an equivalence, there must be a path fn=gn inducing it, and the coherence laws for function extensionality imply (7.3.5). ∎

The following observation about reflective subcategories is also standard.

Corollary 7.3.7.

A type A is an n-type if and only if ||n:AAn is an equivalence.

Proof.

“If” follows from closureMathworldPlanetmathPlanetmath of n-types under equivalence. On the other hand, if A is an n-type, we can define 𝖾𝗑𝗍(𝗂𝖽A):AnA. Then we have 𝖾𝗑𝗍(𝗂𝖽A)||n=𝗂𝖽A:AA by definition. In order to prove that ||n𝖾𝗑𝗍(𝗂𝖽A)=𝗂𝖽An, we only need to prove that ||n𝖾𝗑𝗍(𝗂𝖽A)||n=𝗂𝖽An||n. This is again true:

\includegraphics

HoTT_fig_7.3.2.png

The category of n-types also has some special properties not possessed by all reflective subcategories. For instance, the reflector -n preserves finite productsPlanetmathPlanetmathPlanetmathPlanetmath.

Theorem 7.3.8.

For any types A and B, the induced map A×BnAn×Bn is an equivalence.

Proof.

It suffices to show that An×Bn has the same universal property as A×Bn. Thus, let C be an n-type; we have

(An×BnC) =(An(BnC))
=(An(BC))
=(A(BC))
=(A×BC)

using the universal properties of Bn and An, along with the fact that BC is an n-type since C is. It is straightforward to verify that this equivalence is given by composing with ||n×||n, as needed. ∎

The following related fact about dependent sums is often useful.

Theorem 7.3.9.

Let P:AU be a family of types. Then there is an equivalence

x:AP(x)nnx:AP(x)n.
Proof.

We use the induction principle of n-truncation several times to construct functions

φ :x:AP(x)nnx:AP(x)n
ψ :x:AP(x)nx:AP(x)nn

and homotopies H:φψ𝗂𝖽 and K:ψφ𝗂𝖽 exhibiting them as quasi-inverses. We define φ by setting φ(|(x,|u|n)|n):|(x,u)|n. We define ψ by setting ψ(|(x,u)|n):|(x,|u|n)|n. Then we define H(|(x,u)|n):𝗋𝖾𝖿𝗅|(x,u)|n and K(|(x,|u|n)|n):𝗋𝖾𝖿𝗅|(x,|u|n)|n. ∎

Corollary 7.3.10.

If A is an n-type and P:AU is any type family, then

a:AP(a)na:AP(a)n
Proof.

If A is an n-type, then the left-hand type above is already an n-type, hence equivalent to its n-truncation; thus this follows from Theorem 7.3.9 (http://planetmath.org/73truncations#Thmprethm3). ∎

We can characterize the path spaces of a truncation using the same method that we used in §2.12 (http://planetmath.org/212coproducts),§2.13 (http://planetmath.org/213naturalnumbers) for coproductsMathworldPlanetmath and natural numbersMathworldPlanetmath (and which we will use in http://planetmath.org/node/87582Chapter 8 to calculate homotopy groupsMathworldPlanetmath). Unsurprisingly, the path spaces in the (n+1)-truncation of A are the n-truncations of the path spaces of A. Indeed, for any x,y:A there is a canonical map

f:x=Ayn(|x|n+1=An+1|y|n+1) (7.3.11)

defined by

f(|p|n):𝖺𝗉||n+1(p).

This definition uses the recursion principle for n, which is correct because An+1 is (n+1)-truncated, so that the codomain of f is n-truncated.

Theorem 7.3.12.

For any A and x,y:A and n-2, the map (7.3.11) is an equivalence; thus we have

x=Ayn(|x|n+1=An+1|y|n+1).
Proof.

The proof is a simple application of the encode-decode method: As in previous situations, we cannot directly define a quasi-inverse to the map (7.3.11) because there is no way to induct on an equality between |x|n+1 and |y|n+1. Thus, instead we generalize its type, in order to have general elements of the type An+1 instead of |x|n+1 and |y|n+1. Define P:An+1An+1n-𝖳𝗒𝗉𝖾 by

P(|x|n+1,|y|n+1):x=Ayn

This definition is correct because x=Ayn is n-truncated, and n-𝖳𝗒𝗉𝖾 is (n+1)-truncated by Theorem 7.1.11 (http://planetmath.org/71definitionofntypes#Thmprethm7). Now for every u,v:An+1, there is a map

𝖾𝗇𝖼𝗈𝖽𝖾:P(u,v)(u=An+1v)

defined for u=|x|n+1 and v=|y|n+1 and p:x=y by

𝖾𝗇𝖼𝗈𝖽𝖾(|p|n):𝖺𝗉|¯|n+1(p).

Since the codomain of 𝖾𝗇𝖼𝗈𝖽𝖾 is n-truncated, it suffices to define it only for u and v of this form, and then it’s just the same definition as before. We also define a function

r:u:An+1P(u,u)

by induction on u, where r(|x|n+1):|𝗋𝖾𝖿𝗅x|n.

Now we can define an inverse map

𝖽𝖾𝖼𝗈𝖽𝖾:(u=An+1v)P(u,v)

by

𝖽𝖾𝖼𝗈𝖽𝖾(p):𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍vP(u,v)(p,r(u)).

To show that the composite

(u=An+1v)𝖽𝖾𝖼𝗈𝖽𝖾P(u,v)𝖾𝗇𝖼𝗈𝖽𝖾(u=An+1v)

is the identity function, by path induction it suffices to check it for 𝗋𝖾𝖿𝗅u:u=u, in which case what we need to know is that 𝖽𝖾𝖼𝗈𝖽𝖾(r(u))=𝗋𝖾𝖿𝗅u. But since this is an n-type, hence also an (n+1)-type, we may assume u|x|n+1, in which case it follows by definition of r and 𝖽𝖾𝖼𝗈𝖽𝖾. Finally, to show that

P(u,v)𝖾𝗇𝖼𝗈𝖽𝖾(u=An+1v)𝖽𝖾𝖼𝗈𝖽𝖾P(u,v)

is the identity function, since this goal is again an n-type, we may assume that u=|x|n+1 and v=|y|n+1 and that we are considering |p|n:P(|x|n+1,|y|n+1) for some p:x=y. Then we have

𝖽𝖾𝖼𝗈𝖽𝖾(𝖾𝗇𝖼𝗈𝖽𝖾(|p|n)) =𝖽𝖾𝖼𝗈𝖽𝖾(𝖺𝗉|¯|n+1(p))
=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍vP(|x|n+1,v)(𝖺𝗉|¯|n+1(p),|𝗋𝖾𝖿𝗅x|n)
=𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍vu=vn(p,|𝗋𝖾𝖿𝗅x|n)
=|𝗍𝗋𝖺𝗇𝗌𝗉𝗈𝗋𝗍v(u=v)(p,𝗋𝖾𝖿𝗅x)|n
=|p|n.

This completesPlanetmathPlanetmathPlanetmathPlanetmathPlanetmathPlanetmath the proof that 𝖾𝗇𝖼𝗈𝖽𝖾 and 𝖽𝖾𝖼𝗈𝖽𝖾 are quasi-inverses. The stated result is then the special case where u=|x|n+1 and v=|y|n+1. ∎

Corollary 7.3.13.

Let n-2 and (A,a) be a pointed type. Then

Ω(A,a)n=Ω((A,a)n+1)
Proof.

This is a special case of the previous lemma where x=y=a. ∎

Corollary 7.3.14.

Let n-2 and k0 and (A,a) a pointed type. Then

Ωk(A,a)n=Ωk((A,a)n+k).
Proof.

By induction on k, using the recursive definition of Ωk. ∎

We also observe that “truncations are cumulative”: if we truncate to an n-type and then to a k-type with kn, then we might as well have truncated directly to a k-type.

Lemma 7.3.15.

Let k,n-2 with kn and A:U. Then Ank=Ak.

Proof.

We define two maps f:AnkAk and g:AkAnk by

f(||a|n|k):|a|k  and  g(|a|k):||a|n|k.

The map f is well-defined because Ak is k-truncated and also n-truncated (because kn), and the map g is well-defined because Ank is k-truncated.

The composition fg:AkAk satisfies (fg)(|a|k)=|a|k, hence fg=𝗂𝖽Ak. Similarly, we have (gf)(||a|n|k)=||a|n|k and hence gf=𝗂𝖽Ank. ∎

Title 7.3 Truncations
\metatable