Whiskering a natural isomorphism yields a natural isomorphism I have been reading Peter Smith's Gentle Intro to Category Theory and I don't understand this proof.


*

*I think I understand the idea of whiskering in general, but in Smith's example I am not too sure what the $X$ is: is $X$ an arrow from $\mathscr C$ and being fed into the composition $J \alpha$? eg. if we are imposing $J \alpha$ on $J\circ F$, then $J\circ F_X$ is being mapped to $J\circ G_X$?

*I got lost at 'these components are all isomorphisms'; I see how $J\alpha$ comes about (not so much about $J\alpha_X$, but that's Q1 above), and one of a prior theorems proved that functor preserves isomorphisms, but I don't see how $J\alpha_X$'s are all isomorphisms. (Perhaps because I am not too sure what it is)
Could anyone help please? Thank you so much! (If anyone could please also add a few comments on the proof on the whole to aid understanding that would be really helpful)



 A: $\alpha : F \Rightarrow G$ is a natural transformation and $X$ is some object of $\mathscr C$: remember that a natural transformation is a family of morphisms, indexed over the objects of the domain, so really we're parameterising over all objects $X \in \mathscr C$. The whiskering $J \alpha : \mathscr C \Rightarrow \mathscr E$ is also a natural transformation, which is formed by applying $J : \mathscr D \to \mathscr E$ to each $\alpha_X : FX \to GX$ to get a family of morphisms $J (\alpha_X) : JFX \to JGX$. We usually simply write this as $J \alpha_X$.
Now let us assume $\alpha : F \Rightarrow G$ is a natural isomorphism, which means that each morphism $\alpha_X : FX \to GX$ is an isomorphism. The whiskering $(J \alpha)_X : JFX \to JGX$ is formed by applying $J$ to each $\alpha_X$. As you point out, applying functors preserves isomorphisms (more generally, they preserve commutative diagrams), so if $\alpha_X$ is an isomorphism, then so is $J(\alpha_X)$. This is the statement of Theorem 107: whiskering a natural isomorphism by any functor gives you another natural isomorphism.
A: Here $X$ is an object of $\mathcal C$. 
Remember that a natural transformation [isomorphism] $\alpha:F\to G$ is a collection of arrows [isomorphisms] $\alpha_X:F(X)\to G(X)$ for $X\in Ob\,\mathcal C$ (the 'components of $\alpha$'), satisfying a commutativity condition for each arrow in $\mathcal C$.
So, the components of $J\alpha$ are $J(\alpha_X)$, which are isomorphisms if all $\alpha_X$ are.
Similarly, the components of $\beta F$ are $\beta_{F(X)}$.
Finally, you would want to convince yourself that these collections indeed satisfy the commutativity conditions. 
A: Not at all a formal answer, but I will try to give some intuition : 
A natural transformation is a way to relate two functors $F \Rightarrow G$. Note that there is a directionality to it : you can transform $F$ into $G$, but nothing ensures that you can transform $G$ back into $F$. When you can transform back the way I just said, the natural transformation is called a natural isomorphism.
Now what the whiskering says is that if you can transform $F$ into $G$ (ie, if you have $\alpha : F \Rightarrow G$), then you can always transform $J\circ F$ into $J\circ G$ (ie, you get $J\alpha$). Or in other words, you can also transform $F$ into $G$ inside the expression $J\circ F$. Now what the property that you want to prove says that provided you can transform $G$ back to $F$, you can also do it inside the expression $J\circ G$ to get back to $J\circ F$.
This should be reminiscent of the concept of functor : Whenever you have a functor you can apply it either to objects of the category, like a usual set function, but also you can also apply it on morphisms (ie., ways to relate objects). In our example, if we take a look at the composition with $J$, you can apply it either to the functor $F$ or $G$ (objects in the category of functors), to get $JF$ of $JG$, or to the natural transformation $\alpha$ (morphism in the category of functor). I don't want to expand to much on this, but hopefully you can see how the situations are parallel - And in fact, the given property can be understood as being a special case of the fact that every functor sends isomorphisms to isomorphisms, in this particular instance of the functor "composition with J".
