Natural transformation

I'm trying to understand what a natural transformation is. To this end, I want to show the following:

For each group $H$ the map $G \mapsto H \times G$ deﬁnes a functor $H \times -:\textbf{Grp} \to \textbf{Grp}$ and for each group homomorphism $f: H \to K$ there is a natural transformation $H \times - \to K \times -$.

The definition of natural transformation is the following: Let $C,D$ be two categories and $F,G: C \to D$ be two functors. Then a natural transformation $\eta$ is a collection of morphisms $(\eta_A)_{A \in \text{Obj}(C)}$ such that for all objects $A,B \in \text{Obj}(C)$ and all morphisms $\alpha : A \to B$ we have $$\eta_B \circ F(\alpha) = G(\alpha) \circ \eta_A$$

Let $f: H \to K$ be a group homomorphism. Then we define $\eta_G$ to be the map $G \times H \to G \times K$, $(g, h) \mapsto (g,f(h))$ and similarly $\eta_{G^\prime}: G^\prime \times H \to G^\prime \times K$, $(g^\prime, h) \mapsto (g^\prime, f(h))$.

Let $\alpha : G \to G^\prime$ be a group homomorphism and let $(g,h) \in G \times H$. Then $\eta_{G^\prime} \circ (\times H (\alpha)) (g,h) = \eta_{G^\prime} (\alpha(g), h) = (\alpha(g), f(h))$.

Also, for $(g, h) \in G \times H$ we have $(\times K (\alpha)) \circ \eta_G ((g,h)) = (\times K (\alpha)) ((g, f(h))) = (\alpha(g), f(h))$.

Hence the diagram commutes and we have a natural transformation $\eta : H \times - \to K \times -$.

Can you tell me if this is correct?

-
A natural transformation is, in a precise sense, a homotopy between two functors. More formally, let $I$ be the interval category $0 \rightarrow 1$ (two objects and an arrow between them). Then a functor $I \times C \to D$ is the same thing as a natural transformation between the functor $0 \times C \to D$ and the functor $1 \times C \to D$. – Qiaochu Yuan Jun 8 '12 at 22:31
@QiaochuYuan +1 for "interval category". Is it a somewhat standard name (in topology maybe) ? MacLane calls it simply "$\mathbf{2}$" – magma Jun 10 '12 at 9:40
@magma: it is a special case of some notions of interval object (ncatlab.org/nlab/show/interval+object). – Qiaochu Yuan Jun 10 '12 at 10:10
I think it would be more precise to say 'we have a natural transformation $\eta : - \times H \to - \times K$' instead, since you "define $\eta_G$ to be the map $G \times H \to G \times K$, $(g, h) \mapsto (g,f(h))$" and the same goes for $\eta_{G'}$. We can only say that $X \times Y$ is isomorphic to $Y \times X$, but they are not really equal. – Bruno Bentzen Dec 30 '15 at 3:12

This looks correct to me. You have $$(g,h)\stackrel{F_H(\alpha)}{\mapsto} (\alpha(g),h)\stackrel{\eta_{\,G\,'}}{\mapsto}(\alpha(g),f(h))$$ and $$(g,h)\stackrel{\eta_{\,G}}{\mapsto}(g,f(h))\stackrel{F_K(\alpha)}{\mapsto}(\alpha(g),f(h))$$ hence $G\times H\xrightarrow{F_H(\alpha)}G'\times H\xrightarrow{\eta_{\,G\,'}}G'\times K$ and $G\times H\xrightarrow{\eta_{\,G}}G\times K\xrightarrow{F_K(\alpha)}G'\times K$ commute (if we were to draw them together in a diagram), i.e. $\eta_{\,G\,'}\circ F_H(\alpha)=F_K(\alpha)\circ\eta_G$, as desired.
(And $F_H(\alpha)$ is $\times H(\alpha)$ and $F_K(\alpha)$ is $\times K(\alpha)$ in your notation.)
There seems to be something strange in your formulas. In the first equation you have: $$(g,h)\stackrel{F_H(\alpha)}{\mapsto} (\alpha(g),h)$$ So $F_H(\alpha)$ does not seem to change the second component of its argument ($(g,h)$ in this case), while in your second formula: $$(g,f(g))\stackrel{F_K(\alpha)}{\mapsto}(\alpha(g),f(h))$$ $F_K(\alpha)$ seems to also act on the second component of its argument ($(g,f(g)$ in this case). So your notation is not consistent, or if you prefer natural in H or K. And it should be, I think. – magma Jun 10 '12 at 10:05