What is nLab's yoneda-like argument of dinatural transformation's bijection with natural transformations $\hom(x, y) \to \hom(F(y, x), G(x, y))$?

Question

$\newcommand{\C}{\mathbf{C}}$ $\newcommand{\Cop}{\mathbf{C^\text{op}}}$ $\newcommand{\D}{\mathbf{D}}$ $\newcommand{\dinat}{\stackrel{\cdot}{\to}}$ $\newcommand{\F}{\operatorname{F}}$ $\newcommand{\G}{\operatorname{G}}$ $\newcommand{\hom}{\text{hom}}$ $\newcommand{\id}{\text{id}}$

For two locally small categories $\C$ and $\D$ and two functors $\F, \G : \Cop \times \C \to \D$ the nLab site about dinatural transformations states that:

By a yoneda-like argument, dinatural transformations $\alpha: \F \dinat \G$ are in bijection with natural transformations $\eta_{x,y}:\hom(x, y) \to \hom(\F(y, x), \G(x, y))$. The corresponding transformations are related by $$\eta_{x, y}(f) = \G(x, f)\ \alpha_x\ \F(f, x) = \G(f, y)\ \alpha_y\ \F(y, f)$$ $$\alpha_x = \eta_{x, x}(id)$$

1. How can the naturality of $\G(x, f)\ \alpha_x\ \F(f, x) = \G(f, y)\ \alpha_y\ \F(y, f)$ be proven from the dinaturality of $\alpha$ and
2. How can the dinaturality of $\eta_{x, x}(id)$ be proven from the naturality of $\eta$?

Answer 1

$\require{AMScd}$There is an isomorphism $$ \tag{$\heartsuit$}\text{Dinat}(F,G)\cong\int_X {\bf D}(FXX,GXX)$$ where $ {\bf D}(F,G)$ is defined as $$\begin{CD} {\bf D}(F,G):{\bf C}^{op}\times {\bf C} @>>>({\bf C}^{op}\times {\bf C})^{op}\times ({\bf C}^{op}\times {\bf C}) @>F^{op}\times G>> {\bf D}^{op}\times {\bf D} @>\hom>> {\bf Set} \end{CD}$$ in which the first functor $(X,Y)\mapsto (Y,X,X,Y)$ duplicates, swaps and rebrackets. This because the dinaturality condition amounts exactly to the equation that characterizes the equalizer as the RHS of $(\heartsuit)$.

On the other hand,the same object on RHS rewrites (if you want to see it that way, by Yoneda) as $$\int_X {\bf D}(FXX,GXX) \cong \int_{XY}{\bf Set}\big({\bf C}(X,Y),{\bf D}(F,G)(X,Y)\big)=\int_{XY}{\bf Set}\big({\bf C}(X,Y),{\bf D}(FYX,GXY)\big)$$ which is the set of natural transformations $\hom_{\bf C}\Rightarrow {\bf D}(F,G)$.

Answer 2

The naturality of $\eta : \mathrm{hom}(x, y) \to \mathrm{hom}(F(y, x), G(x, y))$ means that, for every pair of morphisms $f : w \to x$, $g : y \to z$, we have

$$ \eta_{w,z} \circ \mathrm{hom}(f, g) = \mathrm{hom}(F(g, f), G(f, g)) \circ \eta_{x,y} $$

that is, for every $u : x \to y$,

$$ \eta_{w,z}(g \circ u \circ f) = G(f, g) \circ \eta_{x,y}(u) \circ F(g, f) $$

Instantiating $\eta_{x,y}(u)$ with $G(\mathrm{id}_x, u) \circ \alpha_x \circ F(u, \mathrm{id}_x)$, we must check that

$$ G(\mathrm{id}_w, guf) \circ \alpha_w \circ F(guf, \mathrm{id}_w) = G(f, g) \circ G(\mathrm{id}_x, u) \circ \alpha_x \circ F(u, \mathrm{id}_x) \circ F(g, f) $$

which follows from $G(\mathrm{id}_w, f) \circ \alpha_w \circ F(f, \mathrm{id}_w) = G(f, \mathrm{id}_x) \circ \alpha_x \circ F(\mathrm{id}_x, f)$ and functoriality.

In the other direction, dinaturality of $\alpha_x = \eta_{x,x}(\mathrm{id}_x)$ means that for every $f : x \to y$,

$$ G(\mathrm{id}_x, f) \circ \eta_{x,x}(\mathrm{id}_x) \circ F(f, \mathrm{id}_x) = G(f, \mathrm{id}_y) \circ \eta_{y,y}(\mathrm{id}_y) \circ F(\mathrm{id}_y, f) $$

which is immediate from the naturality of $\eta$ as both are equal to $\eta_{x,y}(f)$.