7.6 Orthogonal factorization

In set theoryMathworldPlanetmath, the surjections and the injections form a unique factorization system: every function factors essentially uniquely as a surjection followed by an injection. We have seen that surjections generalize naturally to n-connected maps, so it is natural to inquire whether these also participate in a factorization system. Here is the corresponding generalizationPlanetmathPlanetmath of injections.

Definition 7.6.1.

A function f:Aβ†’B is n-truncated if the fiber fibf⁒(b) is an n-type for all b:B.

In particular, f is (-2)-truncated if and only if it is an equivalence. And of course, A is an n-type if and only if Aβ†’πŸ is n-truncated. Moreover, n-truncated maps could equivalently be defined recursively, like n-types.

Lemma 7.6.2.

For any nβ‰₯-2, a function f:Aβ†’B is (n+1)-truncated if and only if for all x,y:A, the map apf:(x=y)β†’(f(x)=f(y)) is n-truncated. In particular, f is (-1)-truncated if and only if it is an embedding in the sense of Β§4.6 (http://planetmath.org/46surjectionsandembeddings).


Note that for any (x,p),(y,q):𝖿𝗂𝖻f⁒(b), we have

((x,p)=(y,q)) =βˆ‘r:x=y(p=𝖺𝗉f(r)\centerdotq)

Thus, any path space in any fiber of f is a fiber of 𝖺𝗉f. On the other hand, choosing b:≑f(y) and q:≑𝗋𝖾𝖿𝗅f⁒(y) we see that any fiber of 𝖺𝗉f is a path space in a fiber of f. The result follows, since f is (n+1)-truncated if all path spaces of its fibers are n-types. ∎

We can now construct the factorization, in a fairly obvious way.

Definition 7.6.3.

Let f:A→B be a function. The n-image of f is defined as


When n=-1, we write simply im⁒(f) and call it the image of f.

Lemma 7.6.4.

For any function f:Aβ†’B, the canonical function f~:Aβ†’imn⁒(f) is n-connected. Consequently, any function factors as an n-connected function followed by an n-truncated function.


Note that Aβ‰ƒβˆ‘(b:B)𝖿𝗂𝖻f⁒(b). The function f~ is the function on total spaces induced by the canonical fiberwise transformationPlanetmathPlanetmath


Since each map 𝖿𝗂𝖻f(b)β†’βˆ₯𝖿𝗂𝖻f(b)βˆ₯n is n-connected by Corollary 7.5.8 (http://planetmath.org/75connectedness#Thmprecor2), f~ is n-connected by Lemma 7.5.13 (http://planetmath.org/75connectedness#Thmprelem8). Finally, the projection 𝗉𝗋1:𝗂𝗆n⁒(f)β†’B is n-truncated, since its fibers are equivalentMathworldPlanetmathPlanetmathPlanetmathPlanetmath to the n-truncations of the fibers of f. ∎

In the following lemma we set up some machinery to prove the unique factorization theorem.

Lemma 7.6.5.

Suppose we have a commutative diagramMathworldPlanetmath of functions



with H:h1∘g1∼h2∘g2, where g1 and g2 are n-connected and where h1 and h2 are n-truncated. Then there is an equivalence


for any b:B, such that for any a:A we have an identification


Let b:B. Then we have the following equivalences:

𝖿𝗂𝖻h1⁒(b) β‰ƒβˆ‘w:𝖿𝗂𝖻h1⁒(b)βˆ₯𝖿𝗂𝖻g1(𝗉𝗋1w)βˆ₯n (since $g_{1}$ is $n$-connected)
≃βˆ₯βˆ‘w:𝖿𝗂𝖻h1⁒(b)𝖿𝗂𝖻g1⁒(𝗉𝗋1⁒w)βˆ₯n (by Corollary 7.3.10 (http://planetmath.org/73truncationshmprecor2), since $h_{1}$ is $n$-truncated)
≃βˆ₯𝖿𝗂𝖻h1∘g1(b)βˆ₯n (by http://planetmath.org/node/87774Exercise 4.4)

and likewise for h2 and g2. Also, since we have a homotopyMathworldPlanetmath H:h1∘g1∼h2∘g2, there is an obvious equivalence 𝖿𝗂𝖻h1∘g1⁒(b)≃𝖿𝗂𝖻h2∘g2⁒(b). Hence we obtain


for any b:B. By analyzing the underlying functions, we get the following representation of what happens to the element (g1⁒(a),𝗋𝖾𝖿𝗅h1⁒(g1⁒(a))) after applying each of the equivalences of which E is composed. Some of the identifications are definitional, but others (marked with a = below) are only propositional; putting them together we obtain E¯⁒(H,a).

(g1⁒(a),𝗋𝖾𝖿𝗅h1⁒(g1⁒(a))) ↦=((g1(a),𝗋𝖾𝖿𝗅h1⁒(g1⁒(a))),|(a,𝗋𝖾𝖿𝗅g1⁒(a))|n)

The first equality is because for general b, the map 𝖿𝗂𝖻h1(b)β†’βˆ‘(w:𝖿𝗂𝖻h1(b))βˆ₯𝖿𝗂𝖻g1(𝗉𝗋1w)βˆ₯n inserts the center of contraction for βˆ₯𝖿𝗂𝖻g1⁒(𝗉𝗋1⁒w)βˆ₯n supplied by the assumptionPlanetmathPlanetmath that g1 is n-truncated; whereas in the case in question this type has the obvious inhabitant |(a,𝗋𝖾𝖿𝗅g1⁒(a))|n, which by contractibility must be equal to the center. The second propositional equality is because the equivalence 𝖿𝗂𝖻h1∘g1⁒(b)≃𝖿𝗂𝖻h2∘g2⁒(b) concatenates the second components with H⁒(a)-1, and we have H⁒(a)-1⁒\centerdot⁒𝗋𝖾𝖿𝗅=H⁒(a)-1. The reader may check that the other equalities are definitional (assuming a reasonable solution to http://planetmath.org/node/87774Exercise 4.4). ∎

Combining Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2),Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3), we have the following unique factorization result:

Theorem 7.6.6.

For each f:Aβ†’B, the space factn⁒(f) defined by


is contractibleMathworldPlanetmath. Its center of contraction is the element


arising from Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2), where ΞΈ:pr1∘f~∼f is the canonical homotopy, where Ο† is the proof of Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2), and where ψ is the obvious proof that pr1:imn⁒(f)β†’B has n-truncated fibers.


By Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2) we know that there is an element of 𝖿𝖺𝖼𝗍n⁒(f), hence it is enough to show that 𝖿𝖺𝖼𝗍n⁒(f) is a mere proposition. Suppose we have two n-factorizations

(X1,g1,h1,H1,Ο†1,ψ1)  and  (X2,g2,h2,H2,Ο†2,ψ2)

of f. Then we have the pointwise-concatenated homotopy


By univalence and the characterizationMathworldPlanetmath of paths and transport in Ξ£-types, function types, and path types, it suffices to show that

  1. 1.

    there is an equivalence e:X1≃X2,

  2. 2.

    there is a homotopy ΢:e∘g1∼g2,

  3. 3.

    there is a homotopy η:h2∘e∼h1,

  4. 4.

    for any a:A we have 𝖺𝗉h2⁒(΢⁒(a))-1⁒\centerdot⁒η⁒(g1⁒(a))⁒\centerdot⁒H1⁒(a)=H2⁒(a).

We prove these four assertions in that order.

  1. 1.

    By Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3), we have a fiberwise equivalence


    This induces an equivalence of total spaces, i.e.Β we have


    Of course, we also have the equivalences X1β‰ƒβˆ‘(b:B)𝖿𝗂𝖻h1⁒(b) and X2β‰ƒβˆ‘(b:B)𝖿𝗂𝖻h2⁒(b) from Lemma 4.8.2 (http://planetmath.org/48theobjectclassifier#Thmprelem2). This gives us our equivalence e:X1≃X2; the reader may verify that the underlying function of e is given by

  2. 2.

    By Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3), we may choose ΞΆ(a):≑𝖺𝗉𝗉𝗋1(EΒ―(H,a)):e(g1(a))=g2(a).

  3. 3.

    For every x:X1, we have


    giving us a homotopy η:h2∘e∼h1.

  4. 4.

    By the characterization of paths in fibers (Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2)), the path E¯⁒(H,a) from Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3) gives us η⁒(g1⁒(a))=𝖺𝗉h2⁒(΢⁒(a))⁒\centerdot⁒H⁒(a)-1. The desired equality follows by substituting the definition of H and rearranging paths.∎

By standard arguments, this yields the following orthogonality principle.

Theorem 7.6.7.

Let e:A→B be n-connected and m:C→D be n-truncated. Then the map


is an equivalence.

Sketch of proof.

For any (h,k,H) in the codomain, let h=h2∘h1 and k=k2∘k1, where h1 and k1 are n-connected and h2 and k2 are n-truncated. Then f=(m∘h2)∘h1 and f=k2∘(k1∘e) are both n-factorizations of m∘h=k∘e. Thus, there is a unique equivalence between them. It is straightforward (if a bit tedious) to extract from this that 𝖿𝗂𝖻φ⁒((h,k,H)) is contractible. ∎

We end by showing that images are stable under pullbackPlanetmathPlanetmath.

Lemma 7.6.8.

Suppose that the square



is a pullback square and let b:B. Then 𝖿𝗂𝖻f⁒(b)≃𝖿𝗂𝖻g⁒(h⁒(b)).


This follows from pasting of pullbacks (http://planetmath.org/node/87643Exercise 2.12), since the type X in the diagram



is the pullback of the left square if and only if it is the pullback of the outer rectangle, while 𝖿𝗂𝖻f⁒(b) is the pullback of the square on the left and 𝖿𝗂𝖻g⁒(h⁒(b)) is the pullback of the outer rectangle. ∎

Theorem 7.6.9.

Consider functions f:A→B, g:C→D and the diagram



If the outer rectangle is a pullback, then so is the bottom square (and hence so is the top square, by http://planetmath.org/node/87643Exercise 2.12). Consequently, images are stable under pullbacks.


Assuming the outer square is a pullback, we have equivalences

BΓ—D𝗂𝗆n⁒(g) β‰‘βˆ‘(b:B)βˆ‘(w:𝗂𝗆n(g))h⁒(b)=𝗉𝗋1⁒w
β‰ƒβˆ‘b:Bβˆ₯𝖿𝗂𝖻f(b)βˆ₯n (by Theorem 7.6.9 (http://planetmath.org/76orthogonalfactorization#Thmprethm3))
≑𝗂𝗆n⁒(f). ∎
Title 7.6 OrthogonalPlanetmathPlanetmath factorization