Derivar la unidad adyacente de counit

Question

Como ejercicio (2.4.12#5) en Pierce's Teoría de categorías básica para informáticos Estoy tratando de derivar la transformación natural unitaria $\eta : I_{\textbf{C}} \xrightarrow{\cdot} G \circ F$ dada la transformación contable $\epsilon : F \circ G \xrightarrow{\cdot} I_{\textbf{D}}$ y dos functores adjuntos $F : \textbf{C} \rightarrow \textbf{D} \dashv G : \textbf{D} \rightarrow \textbf{C}$

Me imagino que necesito algo que tome $X \rightarrow G(F(X))$ para cualquier X.

Para cualquier Y, si proporciono una flecha $g : F(X) \rightarrow Y$ , $\epsilon$ garantiza la existencia de una flecha única $g^* : X \rightarrow G(Y)$ satisfaciendo $\epsilon_Y \circ F(g^*) = g$

Así que considero $Y = F(X)$ y seleccione la flecha $id_{F(X)}$ esto garantiza un único $id_{F(X)}^* : X \rightarrow G(F(X))$ tal que $\epsilon_{F(X)} \circ F(id_{F(X)}^*) = id_{F(X)}$ .

Este $id_{F(X)}^*$ tiene el tipo adecuado para ser $\eta_X$ e intuitivamente $id_{F(X)}^*$ es un candidato sospechosamente bueno. Por desgracia, no he tenido suerte convirtiendo esa intuición en una prueba.

Para demostrar que $id_{F(X)}^*$ funciona como $\eta_X$ Necesito demostrar que para cualquier $f : X \rightarrow G(Y)$ hay un único $f^\# : F(X) \rightarrow Y$ satisfaciendo $G(f^\#) \circ id_{F(X)}^* = f$ .

Aquí es donde estoy atascado: He pasado por varios caminos aquí, y siempre termino con pilas functor profundas como $G(F(G(F(X))))$ que me cuesta reducir sin pérdida de generalidad. Estoy teniendo problemas para encontrar una manera de generar una flecha $F(X) \rightarrow Y$ de una flecha $X \rightarrow G(Y)$ sin invocar el $\eta$ (que es lo que intento derivar).

Estoy seguro de que me estoy olvidando de una ley adjoint crucial que hace que esto sea fácil. ¿Puedes indicarme la dirección correcta?

Answer 1

¡Estabas allí!

El mapeo que necesitas mapea un morfismo $f:X\to GY$ a $$f^\# := \varepsilon_Y\circ Ff\,.$$ Demuestre que es inverso a $g\mapsto g^*$ y que estos construyen un isomorfismo natural $\hom(X,GY)\to\hom(FX,Y)$ por lo que ya crear una adjunción. Demostrar que su contador es $\varepsilon$ .

---

Para demostrar explícitamente la propiedad requerida, parece que hay que trabajar más:

• Demostrar que $\eta:=X\mapsto 1_{FX}^*$ es una transformación natural.

Entonces, por naturalidad, tenemos $\ G(f^\#)\circ\eta_X=G\varepsilon_Y\circ GFf\circ\eta_X= G\varepsilon_Y\circ \eta_{GY}\circ f$ .

• Demostrar la identidad familiar $G\varepsilon_Y\circ \eta_{GY} = 1_{GY}$ .
• Y aún así, la singularidad de esa propiedad necesitaría una prueba ..