[proofplan]
The spherical $\mathbb Z/2$-index is monotone because an equivariant map from $Y$ to a sphere can be precomposed with the given equivariant map $X\to Y$. For the cohomological $\mathbb Z/2$-index, the equivariant map descends to a continuous map between orbit spaces, and the orbit double cover over $X/(\mathbb Z/2)$ is the pullback of the orbit double cover over $Y/(\mathbb Z/2)$. Naturality of the first Stiefel-Whitney class then identifies the Stiefel-Whitney class of $X$ with the pullback of the one for $Y$, so nonvanishing of a power for $X$ forces nonvanishing of the corresponding power for $Y$.
[/proofplan]
[step:Precompose a spherical-index witness for $Y$ with the equivariant map from $X$]
Let $\tau_X:X\to X$ and $\tau_Y:Y\to Y$ denote the free involutions defining the $\mathbb Z/2$-actions. For each integer $r\geq 0$, let $a_r:S^r\to S^r$ denote the antipodal involution. Thus a map $u:Z\to S^r$ from a $\mathbb Z/2$-space $Z$ with involution $\tau_Z:Z\to Z$ is $\mathbb Z/2$-equivariant precisely when
\begin{align*}
u(\tau_Z(z))=a_r(u(z))
\end{align*}
for every $z\in Z$.
If $\operatorname{ind}_{\mathbb Z/2}(Y)=\infty$, then the inequality
\begin{align*}
\operatorname{ind}_{\mathbb Z/2}(X)\leq \operatorname{ind}_{\mathbb Z/2}(Y)
\end{align*}
holds by the order convention for $\infty$. Suppose instead that $\operatorname{ind}_{\mathbb Z/2}(Y)=m<\infty$. By definition of the spherical $\mathbb Z/2$-index, there exists a continuous $\mathbb Z/2$-equivariant map
\begin{align*}
g:Y\to S^m.
\end{align*}
Define the composite map
\begin{align*}
h:X\to S^m
\end{align*}
by the rule $h(x):=g(f(x))$ for every $x\in X$. The map $h$ is continuous as a [composition of continuous maps](/theorems/4960). For every $x\in X$, using equivariance of $f$ and then equivariance of $g$ gives
\begin{align*}
h(\tau_X(x))=g(f(\tau_X(x)))=g(\tau_Y(f(x)))=a(g(f(x)))=a(h(x)).
\end{align*}
Thus $h:X\to S^m$ is $\mathbb Z/2$-equivariant. Hence $X$ admits an equivariant map to $S^m$, so
\begin{align*}
\operatorname{ind}_{\mathbb Z/2}(X)\leq m=\operatorname{ind}_{\mathbb Z/2}(Y).
\end{align*}
[guided]
The spherical index measures the least dimension of a sphere that receives an equivariant map. Therefore, to prove
\begin{align*}
\operatorname{ind}_{\mathbb Z/2}(X)\leq \operatorname{ind}_{\mathbb Z/2}(Y),
\end{align*}
we should start with a sphere that already receives an equivariant map from $Y$ and then use the given map $X\to Y$ to produce one from $X$.
Let $\tau_X:X\to X$ and $\tau_Y:Y\to Y$ be the free involutions defining the two $\mathbb Z/2$-actions. For each integer $r\geq 0$, let $a_r:S^r\to S^r$ be the antipodal map. If $\operatorname{ind}_{\mathbb Z/2}(Y)=\infty$, the desired inequality is immediate in the extended order. Now assume $\operatorname{ind}_{\mathbb Z/2}(Y)=m<\infty$. By the definition of the spherical $\mathbb Z/2$-index, there is a continuous $\mathbb Z/2$-equivariant map
\begin{align*}
g:Y\to S^m.
\end{align*}
Define
\begin{align*}
h:X\to S^m
\end{align*}
by $h(x):=g(f(x))$ for every $x\in X$. This is the only natural construction available: first send $x$ into $Y$ by $f$, and then send the result into the sphere by $g$.
We verify equivariance explicitly. Since $f$ is $\mathbb Z/2$-equivariant,
\begin{align*}
f(\tau_X(x))=\tau_Y(f(x)).
\end{align*}
Since $g$ is $\mathbb Z/2$-equivariant,
\begin{align*}
g(\tau_Y(y))=a_m(g(y))
\end{align*}
for every $y\in Y$. Applying these two identities with $y=f(x)$ gives
\begin{align*}
h(\tau_X(x))=g(f(\tau_X(x)))=g(\tau_Y(f(x)))=a_m(g(f(x)))=a_m(h(x)).
\end{align*}
Thus $h$ is a continuous $\mathbb Z/2$-equivariant map from $X$ to $S^m$. Consequently the least possible sphere dimension for $X$ is at most $m$, and therefore
\begin{align*}
\operatorname{ind}_{\mathbb Z/2}(X)\leq m=\operatorname{ind}_{\mathbb Z/2}(Y).
\end{align*}
[/guided]
[/step]
[step:Descend the equivariant map to a map between orbit spaces]
Let
\begin{align*}
q_X:X\to X/(\mathbb Z/2)
\end{align*}
and
\begin{align*}
q_Y:Y\to Y/(\mathbb Z/2)
\end{align*}
be the quotient maps. Since $f$ is $\mathbb Z/2$-equivariant, it sends each $\mathbb Z/2$-orbit in $X$ into a single $\mathbb Z/2$-orbit in $Y$. Therefore there is a unique continuous map
\begin{align*}
\bar f:X/(\mathbb Z/2)\to Y/(\mathbb Z/2)
\end{align*}
characterized by $\bar f(q_X(x)):=q_Y(f(x))$ for every $x\in X$ and satisfying
\begin{align*}
\bar f\circ q_X=q_Y\circ f.
\end{align*}
The map is well-defined because if $q_X(x)=q_X(x')$, then either $x'=x$ or $x'=\tau_X(x)$, and hence
\begin{align*}
q_Y(f(x'))=q_Y(f(\tau_X(x)))=q_Y(\tau_Y(f(x)))=q_Y(f(x)).
\end{align*}
[/step]
[step:Identify the Stiefel-Whitney class of $X$ as a pullback]
Let
\begin{align*}
\pi_X:X\to X/(\mathbb Z/2)
\end{align*}
and
\begin{align*}
\pi_Y:Y\to Y/(\mathbb Z/2)
\end{align*}
denote the principal $\mathbb Z/2$-bundles given by the orbit projections. Let
\begin{align*}
w_X:=w_1(\pi_X)\in H^1(X/(\mathbb Z/2);\mathbb Z/2)
\end{align*}
and
\begin{align*}
w_Y:=w_1(\pi_Y)\in H^1(Y/(\mathbb Z/2);\mathbb Z/2)
\end{align*}
be their first Stiefel-Whitney classes.
The commutative identity $\bar f\circ \pi_X=\pi_Y\circ f$ identifies $\pi_X$ with the pullback principal $\mathbb Z/2$-bundle $\bar f^*\pi_Y$ over $X/(\mathbb Z/2)$. Explicitly, define
\begin{align*}
\Phi:X\to \bar f^*Y
\end{align*}
by $\Phi(x):=(\pi_X(x),f(x))$, where
\begin{align*}
\bar f^*Y=\{(b,y)\in X/(\mathbb Z/2)\times Y: \bar f(b)=\pi_Y(y)\}.
\end{align*}
The defining equality $\bar f(\pi_X(x))=\pi_Y(f(x))$ shows that $\Phi(x)$ lies in $\bar f^*Y$. On the fiber over $\pi_X(x)$, the two points of $X$ are $x$ and $\tau_X(x)$ by freeness, and equivariance gives their images $f(x)$ and $\tau_Y(f(x))$, which are exactly the two points in the corresponding fiber of $Y$ by freeness of the $\mathbb Z/2$-action on $Y$. Thus $\Phi$ is a fiberwise bijective equivariant bundle map. To see that it is an isomorphism of double covers, choose a trivializing [open set](/page/Open%20Set) $V\subset X/(\mathbb Z/2)$ for the principal bundle $\pi_X$ and for the pullback bundle $\bar f^*\pi_Y$. Over $V$, both bundles are identified with $V\times \mathbb Z/2$, and equivariance forces the local expression of $\Phi$ to have the form $(b,\epsilon)\mapsto (b,\epsilon_0(b)\epsilon)$ for a function $\epsilon_0:V\to \mathbb Z/2$. Since $\mathbb Z/2$ is discrete and $\Phi$ is continuous, this local expression is a homeomorphism with inverse $(b,\epsilon)\mapsto (b,\epsilon_0(b)^{-1}\epsilon)$. These local inverses agree on overlaps, so $\Phi$ is an isomorphism of double covers. By naturality of the first Stiefel-Whitney class for pullback double covers, applied to the map $\bar f:X/(\mathbb Z/2)\to Y/(\mathbb Z/2)$ and the double cover $\pi_Y:Y\to Y/(\mathbb Z/2)$,
\begin{align*}
w_X=\bar f^*w_Y.
\end{align*}
Since $\bar f^*:H^*(Y/(\mathbb Z/2);\mathbb Z/2)\to H^*(X/(\mathbb Z/2);\mathbb Z/2)$ is a graded ring homomorphism, for every integer $k\geq 0$ we have
\begin{align*}
w_X^k=(\bar f^*w_Y)^k=\bar f^*(w_Y^k).
\end{align*}
[guided]
The cohomological index is controlled by the first Stiefel-Whitney class of the orbit double cover, so the key question is: how are the two orbit double covers related by $f$?
Let
\begin{align*}
\pi_X:X\to X/(\mathbb Z/2)
\end{align*}
and
\begin{align*}
\pi_Y:Y\to Y/(\mathbb Z/2)
\end{align*}
be the orbit projection maps. By the principal-bundle hypothesis in the theorem statement, these orbit projections are principal $\mathbb Z/2$-bundles, equivalently double covers with deck group $\mathbb Z/2$. Define
\begin{align*}
w_X:=w_1(\pi_X)\in H^1(X/(\mathbb Z/2);\mathbb Z/2)
\end{align*}
and
\begin{align*}
w_Y:=w_1(\pi_Y)\in H^1(Y/(\mathbb Z/2);\mathbb Z/2).
\end{align*}
The descended map $\bar f:X/(\mathbb Z/2)\to Y/(\mathbb Z/2)$ satisfies
\begin{align*}
\bar f\circ \pi_X=\pi_Y\circ f.
\end{align*}
This equation says that the double cover of $X/(\mathbb Z/2)$ obtained from $X$ is the pullback of the double cover of $Y/(\mathbb Z/2)$ along $\bar f$. To make the identification explicit, define
\begin{align*}
\Phi:X\to \bar f^*Y
\end{align*}
by $\Phi(x):=(\pi_X(x),f(x))$, where
\begin{align*}
\bar f^*Y=\{(b,y)\in X/(\mathbb Z/2)\times Y: \bar f(b)=\pi_Y(y)\}.
\end{align*}
The equality $\bar f(\pi_X(x))=\pi_Y(f(x))$ verifies that $\Phi(x)$ belongs to the pullback space. Why is this an isomorphism on fibers? Fix $x\in X$. Since the action on $X$ is free, the fiber of $\pi_X$ over $\pi_X(x)$ consists exactly of $x$ and $\tau_X(x)$. Since $f$ is equivariant, these two points are sent to $f(x)$ and $\tau_Y(f(x))$. Since the action on $Y$ is free, those are exactly the two points in the fiber of $\pi_Y$ over $\pi_Y(f(x))$. Thus $\Phi$ is a fiberwise bijective equivariant bundle map. This is enough to identify the two double covers, but we spell out the topological point. On any open set $V\subset X/(\mathbb Z/2)$ over which both principal $\mathbb Z/2$-bundles are trivial, the two bundles are written as $V\times \mathbb Z/2$. In these coordinates an equivariant map over $V$ must be $(b,\epsilon)\mapsto (b,\epsilon_0(b)\epsilon)$ for a function $\epsilon_0:V\to \mathbb Z/2$. Because $\mathbb Z/2$ is discrete and the map is continuous, this formula has the continuous inverse $(b,\epsilon)\mapsto (b,\epsilon_0(b)^{-1}\epsilon)$. The local inverses agree with the same global formula on overlaps, so $\Phi$ is an isomorphism of double covers and identifies $\pi_X$ with $\bar f^*\pi_Y$.
Therefore naturality of the first Stiefel-Whitney class for pullback double covers applies to the map $\bar f:X/(\mathbb Z/2)\to Y/(\mathbb Z/2)$ and the double cover $\pi_Y:Y\to Y/(\mathbb Z/2)$. It gives
\begin{align*}
w_1(\pi_X)=\bar f^*w_1(\pi_Y).
\end{align*}
With the abbreviations $w_X=w_1(\pi_X)$ and $w_Y=w_1(\pi_Y)$, this becomes
\begin{align*}
w_X=\bar f^*w_Y.
\end{align*}
Now we pass from classes to powers. The induced map on cohomology
\begin{align*}
\bar f^*:H^*(Y/(\mathbb Z/2);\mathbb Z/2)\to H^*(X/(\mathbb Z/2);\mathbb Z/2)
\end{align*}
is a graded ring homomorphism, so it preserves cup products. Hence, for every integer $k\geq 0$,
\begin{align*}
w_X^k=(\bar f^*w_Y)^k=\bar f^*(w_Y^k).
\end{align*}
This identity is the monotonicity mechanism: every power of the Stiefel-Whitney class on $X$ is pulled back from the corresponding power on $Y$.
[/guided]
[/step]
[step:Use pullback of Stiefel-Whitney powers to compare cohomological indices]
If $\operatorname{coind}_{\mathbb Z/2}(Y)=\infty$, the desired inequality is immediate. Suppose $\operatorname{coind}_{\mathbb Z/2}(Y)=m<\infty$. By definition of the cohomological $\mathbb Z/2$-index, this means that
\begin{align*}
w_Y^{m}\neq 0
\end{align*}
if $m\geq 0$, and
\begin{align*}
w_Y^{m+1}=0.
\end{align*}
Using the identity from the previous step,
\begin{align*}
w_X^{m+1}=\bar f^*(w_Y^{m+1})=\bar f^*(0)=0.
\end{align*}
If $k>m$, then $k=m+1+\ell$ for some integer $\ell\geq 0$, and the cup-product ring structure gives
\begin{align*}
w_X^k=w_X^{m+1}\smile w_X^\ell=0\smile w_X^\ell=0.
\end{align*}
Therefore no nonzero power of $w_X$ can occur in degree larger than $m$, so
\begin{align*}
\operatorname{coind}_{\mathbb Z/2}(X)\leq m=\operatorname{coind}_{\mathbb Z/2}(Y).
\end{align*}
Together with the spherical-index comparison proved above, this completes the proof.
[/step]
