Suppose we are working with a collection of topological spaces for which there are a product functor $F:Set\to Set:X\to X\times I$ and an exponential functor $G:Set\to Set: X\to X^I$ such that $F\dashv G.$ In such a collection of spaces, the map $i : A \to X$ has the Homotopy Extension property if, for every space $Y$, the following extension problem has a unique solution $\tilde H$, represented by the dashed line. That is, the square shown below is a pushout.
I am trying to give a careful proof of the fact that there is a solution to the above diagram if and only if there is a solution to the following one:
where $p_0(g)=g(0)$ and $h=GH\circ \eta_A$ and $\phi:= G\tilde H\circ \eta_X$ is the unlabeled morphism along the dotted line in the second diagram.
The second diagram is the one given in an exercise which asked me to prove that the pushout of a cofibration is a cofibration. I was able to do the exercise, but since I am more familiar with the first diagram as regards HEP, I want to see that they are equivalent and I think it's a pure category theory argument. I know we need to use the isomorphism defined by the adjunction, with the naturality square
\begin{array}{ccc} \hom( X\times I,Y) & \rightarrow & \hom (X,Y^I) \\ \downarrow & & \downarrow \\ \hom(A\times I,Y) & \rightarrow & \hom(A,Y^I) \end{array}
from which we get $(\tilde H\circ (i\times id))^I\circ \eta_A=i\circ \tilde H^I\circ \eta_X $ but I can't see how to unravel this. Is my approach correct? How should I continue?
Best Answer
As Noel Lundström pointed out in his comment, the square in the first diagram is not a pushout diagram because the homotopy extension property does not require that $\tilde H$ is unique. If you require uniqueness, then for example $\{0\} \hookrightarrow I$ would be not a cofibration. By the way, in the bottom right corner of a pushout square you would not find $X \times I$, but the adjunction space $X \cup_{i_0} A \times I$ which can be identified with $X \times \{0\} \cup A \times I$ if $A$ is closed in $X$.
You correctly invoke the "adjunction isomorphism" $\phi : \hom(X \times I,Y) \to \hom(X,Y^I)$ which is known as the exponential law. There mere existence of some natural bijection $\phi$ is not sufficient for our purposes, we need the fact that $\big(\phi(G)(x)\big)(t) = G(x,t)$. This implies the essential formula $$p_0 \circ \phi(G) = G \circ i_0$$ because $(p_0 \circ \phi(G))(x) = p_0(\phi(G)(x)) = \big(\phi(G)(x)\big)(0) = G(x,0) = (G \circ i_0)(x)$.
The maps $H$ in the first diagram and $h$ in the second diagram are related by $\phi(H) = h$, and so will be the fillers.
Let $\tilde H$ be a filler in the first diagram. Define $\tilde h = \phi(\tilde H) : X \to Y^I$. Since $\tilde H \circ (i \times id_I) = H$, we get $\tilde h \circ i = \phi(\tilde H) \circ i = \phi(\tilde H \circ (i \times id_I)) = \phi(H) = h$ by naturality. Moreover, $p_0 \circ \tilde h = p_0 \circ \phi(\tilde H) = \tilde H \circ i_0 = f$. Hence $\tilde h$ is a filler for the second diagram.
Let $\tilde h$ be a filler in the second diagram. Define $\tilde H = \phi^{-1}(\tilde h) : X \times I \to Y$. Then $\phi(\tilde H \circ (i \times id_I)) = \phi(\tilde H) \circ i = \tilde h \circ i = h = \phi(H)$ by naturality and we conclude $\tilde H \circ (i \times id_I) = H$. Moreover, $\tilde H \circ i_0 = \phi^{-1}(\tilde h) \circ i_0 = p_0 \circ \phi(\phi^{-1}(\tilde h)) = p_0 \circ \tilde h = f$. Hence $\tilde H$ is a filler for the first diagram.