Deje $F: \mathbf C \to \mathbf D, G: \mathbf C \to \mathbf E$ ser functors. Suponga que $\mathbf C$ es pequeña, $\mathbf D$ a nivel local es pequeño y $\mathbf E$ es cocomplete. Entonces, puedo calcular la izquierda Kan extensión de $\mathrm{Lan}_F(G)$ como coend: \begin{equation} \mathrm{Lan}_F(G) = \int^c \mathbf D(F(c),-)\cdot G(c). \end{equation} Ahora, suponga que $F$ es totalmente fiel. Entonces, si yo considerara $\mathrm{Lan}_F(G) \circ F$, puedo calcular: \begin{equation} \mathrm{Lan}_F(G) \circ F = \int^c \mathbf D(F(c),F(-)) \cdot G(c) \cong \int^c \mathbf C(c,-) \cdot G(c) \cong G, \end{equation} donde el último isomorfismo viene frome el co-Yoneda lema. Ahora, lo que quiero mostrar no es sólo que $\mathrm{Lan}_F(G) \circ F \cong G$, pero que la unidad de la extensión Kan \begin{equation} \epsilon_G :G \to \mathrm{Lan}_F(G) \circ F \end{equation} es un isomorfismo. Creo que la cadena de isomorphisms en realidad, da la unidad de $\epsilon_G$ (MacLane en X. 4.2 da una fórmula explícita para eso). Hay una "buena" prueba de ello? O, una bonita prueba directa de que $\epsilon$ es un isomorfismo? Yo estoy pensando en algo que evita trivial, pero tediosos cálculos. Esta es la ventaja del uso final y coends, después de todo.
Respuesta
¿Demasiados anuncios?
Hay un truco útil para tratar con esto. El siguiente aparece como Lema 1.3 en [Johnstone y de Moerdijk, mapas Locales de toposes].
La proposición. Dada la contigüidad $$L \dashv R : \mathcal{D} \to \mathcal{C}$$ si $\mathrm{id}_{\mathcal{C}} \cong R L$ (como functors), a continuación, la unidad $\eta : \mathrm{id}_{\mathcal{C}} \Rightarrow R L$ es (también) un isomorfismo natural.
Prueba. Deje $\mu = R \epsilon L$ donde $\epsilon : L R \Rightarrow \mathrm{id}_{\mathcal{D}}$ es el counit. Entonces (por el triángulo de las identidades), tenemos una monada. Podemos transportar esta estructura a lo largo de cualquier natural isomorfismo $\theta : \mathrm{id}_{\mathcal{D}} \Rightarrow R L$, de modo que, por ejemplo, $$\begin{array}{rcl} \mathrm{id}_{\mathcal{C}} & \overset{\theta}{\to} & \mathrm{id}_{\mathcal{C}} \\ {\scriptstyle \eta} \downarrow & & \downarrow {\scriptstyle \eta'} \\ \mathrm{id}_{\mathcal{C}} & \underset{\theta}{\to} & R L \end{array}$$ los desplazamientos. Pero (utilizando connaturalidad) cualquier comonad estructura $(\eta', \mu')$ $\mathrm{id}_{\mathcal{C}}$ debe consistir natural isomorphisms, por lo que podemos deducir que el original $\eta$ $\mu$ son naturales isomorphisms. ◼
