DaoFP Chapter 20 Solutions

solution

Solutions to the exercises of DaoFP, Chapter 20: DaoFP Chapter 20 Exercises. Index: Map of Content.

Solution 20.1.1

proof — Exercise 20.1.1

${\mathcal{C}}^{\mathrm{op}}(a,b):=\mathcal{C}(b,a)$. Composition ${\mathcal{C}}^{\mathrm{op}}(b,c)\otimes {\mathcal{C}}^{\mathrm{op}}(a,b)\to {\mathcal{C}}^{\mathrm{op}}(a,c)$ is $\mathcal{C}(c,b)\otimes \mathcal{C}(b,a)\stackrel{\gamma }{\to }\mathcal{C}(b,a)\otimes \mathcal{C}(c,b)\stackrel{{\circ }_{\mathcal{C}}}{\to }\mathcal{C}(c,a)$ — the symmetry $\gamma$ of $\mathcal{V}$ swaps the factors so that $\mathcal{C}$‘s composition applies; the unit $j_a:I\to {\mathcal{C}}^{\mathrm{op}}(a,a)=\mathcal{C}(a,a)$ is $\mathcal{C}$‘s unit. Associativity and unit laws follow from those of $\mathcal{C}$ and the coherence of $\gamma$; this is why $\mathcal{V}$ must be symmetric to form opposites.

Sources: DaoFP Exercise 20.1.1; 7 Sketches Exercise 2.63.

Solution 20.1.2

proof — Exercise 20.1.2

Given $f:I\to \mathcal{C}(a,b)$ and $g:I\to \mathcal{C}(b,c)$, define $g{\circ }_{0}f:=I\cong I\otimes I\stackrel{g\otimes f}{\to }\mathcal{C}(b,c)\otimes \mathcal{C}(a,b)\stackrel{\circ }{\to }\mathcal{C}(a,c)$; the identity is $j_a:I\to \mathcal{C}(a,a)$. Associativity follows from the associativity pentagon for $\circ$ together with the coherence of $I\otimes I\cong I$; the unit laws from the unit triangles of $\mathcal{C}$ and the unitors of $\mathcal{V}$. For $\mathcal{V}=\mathbf{Set}$ (with $I=1$) this recovers $\mathcal{C}$ itself; for $\mathcal{V}=\mathbf{Bool}$ it turns a preorder’s truth values into hom-sets of size $0$ or $1$; for a Lawvere Metric Space the underlying category has an arrow $a\to b$ iff $d(a,b)=0$.

Sources: DaoFP Exercise 20.1.2; 7 Sketches §2.3.

Solution 20.2.1

example — Exercise 20.2.1

A $\mathbf{Bool}$-functor $F:P\to Q$ is a function on objects with $P(a,b)\le Q(Fa,Fb)$ in $\mathbf{Bool}$, i.e. $a\le b\Rightarrow Fa\le Fb$ — a Monotone Map (7 Sketches Example 2.70: $\mathbf{Bool}$-functors are monotone maps, Cost-functors are Lipschitz maps).

Sources: DaoFP Exercise 20.2.1; 7 Sketches §2.4.2.

Solution 20.2.2

proof — Exercise 20.2.2

Its action on internal homs must be a map $[a,a^{\prime }]\otimes [b,b^{\prime }]\to [a\otimes b,a^{\prime }\otimes b^{\prime }]$. By the currying adjunction such a map corresponds to $[a,a^{\prime }]\otimes [b,b^{\prime }]\otimes a\otimes b\to a^{\prime }\otimes b^{\prime }$; rearrange with the symmetry to $([a,a^{\prime }]\otimes a)\otimes ([b,b^{\prime }]\otimes b)$ and apply the evaluation counits $\epsilon \otimes \epsilon$. Preservation of composition and identities follows from the corresponding properties of evaluation.

Sources: DaoFP Exercise 20.2.2.

Solution 20.6.1

proof — Exercise 20.6.1

Map out to an arbitrary $d$: $\mathcal{D}({\mathrm{colim}}^{\mathrm{Hom}}P,d)\cong [({\mathcal{C}}^{\mathrm{op}}\times \mathcal{C}{)}^{\mathrm{op}},\mathbf{Set}]({\mathcal{C}}^{\mathrm{op}}(-,=),\mathcal{D}(P(-,=),d))\cong {\int }_{⟨c,c^{\prime }⟩}\mathbf{Set}(\mathcal{C}(c^{\prime },c),\mathcal{D}(P⟨c,c^{\prime }⟩,d))$. By Fubini and ninja Yoneda over $c^{\prime }$ this is ${\int }_c\mathcal{D}(P⟨c,c⟩,d)\cong \mathcal{D}({\int }^{c}P⟨c,c⟩,d)$ (co-continuity of hom). Since $d$ is arbitrary, the Yoneda trick gives ${\mathrm{colim}}^{\mathrm{Hom}}P\cong {\int }^{c}P⟨c,c⟩$.

Sources: DaoFP Exercise 20.6.1.

Solution 20.6.2

proof — Exercise 20.6.2

$\mathcal{C}(x,{\int }_{j}Wj⋔Dj)\cong {\int }_j\mathcal{C}(x,Wj⋔Dj)$ (continuity) $\cong {\int }_j\mathbf{Set}(Wj,\mathcal{C}(x,Dj))$ (power) $\cong [\mathcal{J},\mathbf{Set}](W,\mathcal{C}(x,D-))$ (natural transformations as an end) $\cong \mathcal{C}(x,{\lim }^{W}D)$; conclude by Yoneda. Dually $\mathcal{C}({\int }^{j}Wj\cdot Dj,x)\cong {\int }_j\mathbf{Set}(Wj,\mathcal{C}(Dj,x))\cong [{\mathcal{J}}^{\mathrm{op}},\mathbf{Set}](W,\mathcal{C}(D-,x))\cong \mathcal{C}({\mathrm{colim}}^{W}D,x)$ using the copower.

Sources: DaoFP Exercise 20.6.2.

Solution 20.7.1

proof — Exercise 20.7.1

Map out to arbitrary $d$: $\mathcal{C}(({\mathrm{Lan}}_{P}F)e,d)\cong \mathcal{C}({\int }^c\mathcal{B}(Pc,e)\cdot Fc,d)\cong {\int }_c\mathcal{C}(\mathcal{B}(Pc,e)\cdot Fc,d)$ (co-continuity) $\cong {\int }_c\mathbf{Set}(\mathcal{B}(Pc,e),\mathcal{C}(Fc,d))$ (copower) $\cong [{\mathcal{E}}^{\mathrm{op}},\mathbf{Set}](\mathcal{B}(P-,e),\mathcal{C}(F-,d))\cong \mathcal{C}({\mathrm{colim}}^{\mathcal{B}(P-,e)}F,d)$ by the definition of the weighted colimit. Yoneda finishes the argument; in the enriched setting this formula is taken as the definition.

Sources: DaoFP Exercise 20.7.1.