WORK IN PROGRESS!
Here we use the fact that (the cone \boxed{ \pi : \leftcat{1_{(l \downarrow \rightadj R)} }\lim \Rightarrow \leftcat{1_{(l \downarrow \rightadj R)} }: \leftcat{(l \downarrow \rightadj R)} \to \leftcat{(l \downarrow \rightadj R)} }) is (a natural transformation).
Hence (the following triangles) commute for all (\rightcat r \leftcat{[\lambda]}\in \leftcat{(l \downarrow \rightadj R)}) and (\rightcat f as shown):
\boxed{ \begin{array} {c|cccccc|cccccc} \leftcat{1_{(l \downarrow \rightadj R)} } & \kern0em & \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} & {} \rlap{ \kern-1em \xrightarrow[\smash{\kern15em}]{\textstyle \rlap{\pi_{\rightcat r[\lambda]}} } } &&& \rightcat r \leftcat{[\lambda]} & \kern0em & \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} & {} \rlap{ \rightcat{ \kern-1em \xrightarrow[\smash{\kern15em}]{\textstyle f } } } &&& \rightcat r \leftcat{[\lambda]} \\ \llap{\pi} \Big\Uparrow & && \llap{ \pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }} } \nwarrow & \pi_{\pi_{\rightcat r \leftcat{[\lambda]}}} & \nearrow \rlap{\pi_{\rightcat r[\lambda]}} && && \llap{ \pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }} } \nwarrow & \pi_{\rightcat f} & \nearrow \rlap{ \pi_{\rightcat r[\lambda]} } \\ \leftcat{ 1_{(l \downarrow \rightadj R)} \lim_{(l \downarrow \rightadj R) } } & & && \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} & & && && \leftcat{ 1_{(l \downarrow \rightadj R)} \lim_{(l \downarrow \rightadj R)} } \\ \end{array} }
To reiterate, (the two triangles above) commute for all (\rightcat r \leftcat{[\lambda]}\in \leftcat{(l \downarrow \rightadj R)}) and (\rightcat f as shown) because (\rightcat\pi is a cone).
Using (naturality of \pi at \pi_{\rightcat r \leftcat{[\lambda]}}), i.e. \pi_{\pi_{\rightcat r \leftcat{[\lambda]}}}, plus
(the uniqueness clause in the universal property of \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)}),
we get that \pi_{\rightcat{ (\black Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] }} = 1_{ \leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} }.
This, plus (naturality of \pi at \rightcat f), i.e. \pi_{\rightcat f},
gives \rightcat f = \pi_{\rightcat r[\lambda]}.
This in turn gives us that
\leftcat{1_{(l \downarrow \rightadj R)} }\lim_{(l \downarrow \rightadj R)} is
(an initial object in {(l \downarrow \rightadj R)}},
which is equivalent to
\rightcat{ (Q\lim_\calR) } \leftcat{ \big[\overline{\lambda}\big] } being
(a universal arrow from \leftcat l to \rightadj\calR)
which is equivalent to
\rightcat{ (Q\lim_\calR) } being (a left adjoint \leftcat l \leftadj L for \leftcat l) with (\leftcat{ \overline{\lambda} } its unit).
<hr />
\boxed{ \begin{array} {c|c|c} \kern2em & \kern2em & \kern2em \\ xx & yy & zz \\ \end{array} }
\boxed{ \begin{array} {} && r \\ & \llap{\pi_r} \nearrow & \pi_{\pi_r} & \nwarrow \rlap{\pi_r} \\ \leftcat l\leftadj L & {} \rlap{ \kern-1em \xrightarrow[\pi_{\leftcat l\leftadj L}] {\kern8em} } &&& \leftcat l\leftadj L \\ \end{array} }
No comments:
Post a Comment