7.6 Orthogonal factorization

In set theory, 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 generalization of injections.

Definition 7.6.1.

A function $f\mathrm{:}A\mathrm{\to }B$ is $n$-truncatedif the fiber ${\mathrm{fib}}_f\mathit{}\mathrm{(}b\mathrm{)}$ is an $n$-type for all $b\mathrm{:}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\to \mathrm{𝟏}$ is $n$-truncated.Moreover, $n$-truncated maps could equivalently be defined recursively, like $n$-types.

Lemma 7.6.2.

For any $n\mathrm{\ge }\mathrm{-}\mathrm{2}$, a function $f\mathrm{:}A\mathrm{\to }B$ is $\mathrm{(}n\mathrm{+}\mathrm{1}\mathrm{)}$-truncated if and only if for all $x\mathrm{,}y\mathrm{:}A$, the map ${\mathrm{ap}}_f\mathrm{:}\mathrm{(}x\mathrm{=}y\mathrm{)}\mathrm{\to }\mathrm{(}f\mathrm{(}x\mathrm{)}\mathrm{=}f\mathrm{(}y\mathrm{)}\mathrm{)}$ is $n$-truncated.In particular, $f$ is $\mathrm{(}\mathrm{-}\mathrm{1}\mathrm{)}$-truncated if and only if it is an embedding in the sense of §4.6 (http://planetmath.org/46surjectionsandembeddings).

Proof.

Note that for any $(x,p),(y,q):{\mathrm{𝖿𝗂𝖻}}_f(b)$, we have

$\left((x,p)=(y,q)\right)$$={\displaystyle \sum _{r:x=y}}(p={\mathrm{𝖺𝗉}}_f(r)q)$

$={\displaystyle \sum _{r:x=y}}({\mathrm{𝖺𝗉}}_f(r)=p{q}^{-1})$

$={\mathrm{𝖿𝗂𝖻}}_{{\mathrm{𝖺𝗉}}_f}(p{q}^{-1}).$

Thus, any path space in any fiber of $f$ is a fiber of ${\mathrm{𝖺𝗉}}_f$.On the other hand, choosing $b:\equiv f(y)$ and $q:\equiv {\mathrm{𝗋𝖾𝖿𝗅}}_{f(y)}$ we see that any fiber of ${\mathrm{𝖺𝗉}}_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\mathrm{:}A\mathrm{\to }B$ be a function. The $n$-imageof $f$ is defined as

$${\mathrm{𝗂𝗆}}_n(f):\equiv \sum _{b:B}\parallel {\mathrm{𝖿𝗂𝖻}}_f(b){\parallel }_n.$$

When $n\mathrm{=}\mathrm{-}\mathrm{1}$, we write simply $\mathrm{im}\mathit{}\mathrm{(}f\mathrm{)}$ and call it the image of $f$.

Lemma 7.6.4.

For any function $f\mathrm{:}A\mathrm{\to }B$, the canonical function $\stackrel{\mathrm{~}}{f}\mathrm{:}A\mathrm{\to }{\mathrm{im}}_n\mathit{}\mathrm{(}f\mathrm{)}$ is $n$-connected.Consequently, any function factors as an $n$-connected function followed by an $n$-truncated function.

Proof.

Note that $A\simeq {\sum }_{(b:B)}{\mathrm{𝖿𝗂𝖻}}_f(b)$. The function $\tilde{f}$ is the function on total spaces induced by the canonical fiberwise transformation

$$\prod _{b:B}({\mathrm{𝖿𝗂𝖻}}_f(b)\to \parallel {\mathrm{𝖿𝗂𝖻}}_f(b){\parallel }_n).$$

Since each map ${\mathrm{𝖿𝗂𝖻}}_f(b)\to \parallel {\mathrm{𝖿𝗂𝖻}}_f(b){\parallel }_n$ is $n$-connected by Corollary 7.5.8 (http://planetmath.org/75connectedness#Thmprecor2), $\tilde{f}$ is $n$-connected by Lemma 7.5.13 (http://planetmath.org/75connectedness#Thmprelem8).Finally, the projection ${\mathrm{𝗉𝗋}}_1:{\mathrm{𝗂𝗆}}_n(f)\to B$ is $n$-truncated, since its fibers are equivalent 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 diagram of functions

HoTT_fig_7.6.1.png

with $H:h_1\circ g_1\sim h_2\circ g_2$, where $g_1$ and $g_2$ are $n$-connected and where $h_1$ and $h_2$ are $n$-truncated.Then there is an equivalence

$$E(H,b):{\mathrm{𝖿𝗂𝖻}}_{h_1}(b)\simeq {\mathrm{𝖿𝗂𝖻}}_{h_2}(b)$$

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

$$\overline{E}(H,a):E(H,h_1(g_1(a)))(g_1(a),{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(g_1(a))})=(g_2(a),H{(a)}^{-1}).$$

Proof.

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

${\mathrm{𝖿𝗂𝖻}}_{h_1}(b)$$\simeq {\displaystyle \sum _{w:{\mathrm{𝖿𝗂𝖻}}_{h_1}(b)}}\parallel {\mathrm{𝖿𝗂𝖻}}_{g_1}({\mathrm{𝗉𝗋}}_{1}w){\parallel }_n$(since $g_{1}$ is $n$-connected)

$\simeq {\parallel {\displaystyle \sum _{w:{\mathrm{𝖿𝗂𝖻}}_{h_1}(b)}}{\mathrm{𝖿𝗂𝖻}}_{g_1}({\mathrm{𝗉𝗋}}_{1}w)\parallel }_n$(by Corollary 7.3.10 (http://planetmath.org/73truncationshmprecor2), since $h_{1}$ is $n$-truncated)

$\simeq \parallel {\mathrm{𝖿𝗂𝖻}}_{h_1\circ g_1}(b){\parallel }_n$(by http://planetmath.org/node/87774Exercise 4.4)

and likewise for $h_2$ and $g_2$.Also, since we have a homotopy $H:h_1\circ g_1\sim h_2\circ g_2$, there is an obvious equivalence ${\mathrm{𝖿𝗂𝖻}}_{h_1\circ g_1}(b)\simeq {\mathrm{𝖿𝗂𝖻}}_{h_2\circ g_2}(b)$.Hence we obtain

$${\mathrm{𝖿𝗂𝖻}}_{h_1}(b)\simeq {\mathrm{𝖿𝗂𝖻}}_{h_2}(b)$$

for any $b:B$. By analyzing the underlying functions, we get the following representation of what happens to the element$(g_1(a),{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(g_1(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 $\overline{E}(H,a)$.

$(g_1(a),{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(g_1(a))})$$\stackrel{=}{\mapsto }((g_1(a),{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(g_1(a))}),|(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{g_1(a)}){|}_n)$

$\mapsto |((g_1(a),{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(g_1(a))}),(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{g_1(a)})){|}_n$

$\mapsto |(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(g_1(a))}){|}_n$

$\stackrel{=}{\mapsto }|(a,H{(a)}^{-1}){|}_n$

$\mapsto |((g_2(a),H{(a)}^{-1}),(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{g_2(a)})){|}_n$

$\mapsto ((g_2(a),H{(a)}^{-1}),|(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{g_2(a)}){|}_n)$

$\mapsto (g_2(a),H{(a)}^{-1})$

The first equality is because for general $b$, the map${\mathrm{𝖿𝗂𝖻}}_{h_1}(b)\to {\sum }_{(w:{\mathrm{𝖿𝗂𝖻}}_{h_1}(b))}\parallel {\mathrm{𝖿𝗂𝖻}}_{g_1}({\mathrm{𝗉𝗋}}_{1}w){\parallel }_n$inserts the center of contraction for ${\parallel {\mathrm{𝖿𝗂𝖻}}_{g_1}({\mathrm{𝗉𝗋}}_{1}w)\parallel }_n$ supplied by the assumption that $g_1$ is $n$-truncated; whereas in the case in question this type has the obvious inhabitant $|(a,{\mathrm{𝗋𝖾𝖿𝗅}}_{g_1(a)}){|}_n$, which by contractibility must be equal to the center.The second propositional equality is because the equivalence ${\mathrm{𝖿𝗂𝖻}}_{h_1\circ g_1}(b)\simeq {\mathrm{𝖿𝗂𝖻}}_{h_2\circ g_2}(b)$ concatenates the second components with $H{(a)}^{-1}$, and we have $H{(a)}^{-1}\mathrm{𝗋𝖾𝖿𝗅}=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\mathrm{:}A\mathrm{\to }B$, the space ${\mathrm{fact}}_n\mathit{}\mathrm{(}f\mathrm{)}$ defined by

$$\sum _{(X:𝒰)}\sum _{(g:A\to X)}\sum _{(h:X\to B)}(h\circ g\sim f)\times {\mathrm{𝖼𝗈𝗇𝗇}}_n(g)\times {\mathrm{𝗍𝗋𝗎𝗇𝖼}}_n(h).$$

is contractible.Its center of contraction is the element

$$({\mathrm{𝗂𝗆}}_n(f),\tilde{f},{\mathrm{𝗉𝗋}}_1,\theta ,\phi ,\psi ):{\mathrm{𝖿𝖺𝖼𝗍}}_n(f)$$

arising from Lemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2),where $\theta \mathrm{:}{\mathrm{pr}}_{\mathrm{1}}\mathrm{\circ }\stackrel{\mathrm{~}}{f}\mathrm{\sim }f$ is the canonical homotopy, where $\phi$ is the proof ofLemma 7.6.4 (http://planetmath.org/76orthogonalfactorization#Thmprelem2), and where $\psi$ is the obvious proof that ${\mathrm{pr}}_{\mathrm{1}}\mathrm{:}{\mathrm{im}}_n\mathit{}\mathrm{(}f\mathrm{)}\mathrm{\to }B$ has $n$-truncated fibers.

Proof.

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

$$(X_1,g_1,h_1,H_1,{\phi }_1,{\psi }_1)\mathit{\hspace{1em}\hspace{1em}}\text{and}\mathit{\hspace{1em}\hspace{1em}}(X_2,g_2,h_2,H_2,{\phi }_2,{\psi }_2)$$

of $f$. Then we have the pointwise-concatenated homotopy

$$H:\equiv (\lambda a.H_1(a)H_2^{-1}(a)):(h_1\circ g_1\sim h_2\circ g_2).$$

By univalence and the characterization of paths and transport in $\mathrm{\Sigma }$-types, function types, and path types, it suffices to show that

1. there is an equivalence $e:X_1\simeq X_2$,

2. there is a homotopy $\zeta :e\circ g_1\sim g_2$,

3. there is a homotopy $\eta :h_2\circ e\sim h_1$,

4. for any $a:A$ we have ${\mathrm{𝖺𝗉}}_{h_2}{(\zeta (a))}^{-1}\eta (g_1(a))H_1(a)=H_2(a)$.

We prove these four assertions in that order.

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

   $$E(H):\prod _{b:B}{\mathrm{𝖿𝗂𝖻}}_{h_1}(b)\simeq {\mathrm{𝖿𝗂𝖻}}_{h_2}(b).$$

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

   $$\left(\sum _{b:B}{\mathrm{𝖿𝗂𝖻}}_{h_1}(b)\right)\simeq \left(\sum _{b:B}{\mathrm{𝖿𝗂𝖻}}_{h_2}(b)\right).$$

   Of course, we also have the equivalences $X_1\simeq {\sum }_{(b:B)}{\mathrm{𝖿𝗂𝖻}}_{h_1}(b)$ and $X_2\simeq {\sum }_{(b:B)}{\mathrm{𝖿𝗂𝖻}}_{h_2}(b)$ from Lemma 4.8.2 (http://planetmath.org/48theobjectclassifier#Thmprelem2).This gives us our equivalence $e:X_1\simeq X_2$; the reader may verify that the underlying function of $e$ is given by

   $$e(x)\equiv {\mathrm{𝗉𝗋}}_1(E(H,h_1(x))(x,{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(x)})).$$

2. By Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3), we may choose$\zeta (a):\equiv {\mathrm{𝖺𝗉}}_{{\mathrm{𝗉𝗋}}_1}(\overline{E}(H,a)):e(g_1(a))=g_2(a)$.

3. For every $x:X_1$, we have

   $${\mathrm{𝗉𝗋}}_2(E(H,h_1(x))(x,{\mathrm{𝗋𝖾𝖿𝗅}}_{h_1(x)})):h_2(e(x))=h_1(x),$$

   giving us a homotopy $\eta :h_2\circ e\sim h_1$.

4. By the characterization of paths in fibers (Lemma 4.2.5 (http://planetmath.org/42halfadjointequivalences#Thmprelem2)), the path $\overline{E}(H,a)$ from Lemma 7.6.5 (http://planetmath.org/76orthogonalfactorization#Thmprelem3) gives us$\eta (g_1(a))={\mathrm{𝖺𝗉}}_{h_2}(\zeta (a))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\mathrm{:}A\mathrm{\to }B$ be $n$-connected and $m\mathrm{:}C\mathrm{\to }D$ be $n$-truncated.Then the map

$$\phi :(B\to C)\to \sum _{(h:A\to C)}\sum _{(k:B\to D)}(m\circ h\sim k\circ e)$$

is an equivalence.

Sketch of proof.

For any $(h,k,H)$ in the codomain, let $h=h_2\circ h_1$ and $k=k_2\circ k_1$, where $h_1$ and $k_1$ are $n$-connected and $h_2$ and $k_2$ are $n$-truncated.Then $f=(m\circ h_2)\circ h_1$ and $f=k_2\circ (k_1\circ e)$ are both $n$-factorizations of $m\circ h=k\circ e$.Thus, there is a unique equivalence between them.It is straightforward (if a bit tedious) to extract from this that ${\mathrm{𝖿𝗂𝖻}}_{\phi }((h,k,H))$ is contractible.∎

We end by showing that images are stable under pullback.

Lemma 7.6.8.

Suppose that the square

HoTT_fig_7.6.2.png

is a pullback square and let $b:B$. Then ${\mathrm{𝖿𝗂𝖻}}_f(b)\simeq {\mathrm{𝖿𝗂𝖻}}_g(h(b))$.

Proof.

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

HoTT_fig_7.6.3.png

is the pullback of the left square if and only if it is the pullback of the outer rectangle, while ${\mathrm{𝖿𝗂𝖻}}_f(b)$ is the pullback of the square on the left and ${\mathrm{𝖿𝗂𝖻}}_g(h(b))$ is the pullback of the outer rectangle.∎

Theorem 7.6.9.

Consider functions $f\mathrm{:}A\mathrm{\to }B$, $g\mathrm{:}C\mathrm{\to }D$ and the diagram

HoTT_fig_7.6.4.png

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.

Proof.

Assuming the outer square is a pullback, we have equivalences

$B{\times }_D{\mathrm{𝗂𝗆}}_n(g)$$\equiv {\displaystyle \sum _{(b:B)}}{\displaystyle \sum _{(w:{\mathrm{𝗂𝗆}}_n(g))}}h(b)={\mathrm{𝗉𝗋}}_{1}w$

$\simeq {\displaystyle \sum _{(b:B)}}{\displaystyle \sum _{(d:D)}}{\displaystyle \sum _{(w:\parallel {\mathrm{𝖿𝗂𝖻}}_g(d){\parallel }_n)}}h(b)=d$

$\simeq {\displaystyle \sum _{b:B}}\parallel {\mathrm{𝖿𝗂𝖻}}_g(h(b)){\parallel }_n$

$\simeq {\displaystyle \sum _{b:B}}\parallel {\mathrm{𝖿𝗂𝖻}}_f(b){\parallel }_n$(by Theorem 7.6.9 (http://planetmath.org/76orthogonalfactorization#Thmprethm3))

$\equiv {\mathrm{𝗂𝗆}}_n(f).$$\mathit{∎}$