Solution (source code)

= Solution

Write $f_x$ for the <linear isometry> specified at $x$. Choose a cofinal sequence $V_i$ from the indexing family $I$, and write the target part of the supplied <subordinate flag for a family of linear isometries> as $W_i$. After a cofinal enlargement it has
$$
V_i\subset V_{i+1},\qquad W_i\subset W_{i+1},\qquad f_x(V_i)\subset W_i\quad(x\in X).
$$
Both flags exhaust their <universe for spectra>. Compactness of the parameter space ensures that a finite target stage can contain all images of each fixed source stage.

Let $\xi_i$ be the <vector bundle> on $X$ with fiber
$$
(\xi_i)_x=W_i\ominus f_x(V_i).
$$
Here $\ominus$ is the <orthogonal complement> in the indicated ambient subspace. Its rank is $\dim W_i-\dim V_i$. Let $\operatorname{Th}(\xi_i)$ be its <Thom space>, the disk bundle modulo its sphere bundle, so that every fiber is compactified and all its points at infinity become the single basepoint. For the zero bundle this convention gives $\operatorname{Th}(0_X)=X_+$. Define a target <indexed prespectrum> on the flag by
$$
P(W_i)=\operatorname{Th}(\xi_i)\wedge E(V_i).
$$
The <smash product> here is of <based spaces>, not yet the derived <smash product of spectra>.

To specify all structure maps, for $i\le j$ use the continuous fiberwise orthogonal isomorphism
$$
(W_j\ominus W_i)\oplus(\xi_i)_x\cong(\xi_j)_x\oplus f_x(V_j\ominus V_i).
$$
Both sides identify with the complement of $f_x(V_i)$ in $W_j$. In particular this is the isometry obtained by orthogonally projecting onto $f_x(V_j\ominus V_i)$ and its complement; it is not an assertion that the displayed summands coincide separately. Pass to fiberwise <one-point compactifications>, identify the last summand with $V_j\ominus V_i$ using $f_x^{-1}$, and apply the source structure map. This defines
$$
S^{W_j\ominus W_i}\wedge P(W_i)\longrightarrow P(W_j).
$$
More explicitly, decompose $z+w\in W_j\ominus f_x(V_i)$, where $z\in W_j\ominus W_i$ and $w\in(\xi_i)_x$, as $w'+f_x(v)$ with $w'\in(\xi_j)_x$ and $v\in V_j\ominus V_i$. Send its pair with $e\in E(V_i)$ to the pair $(w',\sigma_{V_i,V_j}(v,e))$ over $x$. The notation for finite vectors extends to the compactifications, sending infinities and basepoints to the basepoint. Orthogonal decomposition and associativity of the source structure maps prove the prespectrum identities.

Extend the <indexed prespectrum> from the cofinal flag to the target indexing family and apply <spectrification> $L$. The point-set definition is
$$
\boxed{X\ltimes_f E=LP.}
$$
On a <map of topological spectra> $u:E\to E'$ it is induced at stage $i$ by $1_{\operatorname{Th}(\xi_i)}\wedge u(V_i)$. Thus the prescribed isometry family, indexing family and flag have all been used. A common cofinal refinement identifies the resulting objects in the <stable homotopy category>; the point-set model retains the chosen flag. If $f$ is a constant standard inclusion, the complement bundles are trivial and this recovers the usual reindexed $X_+\wedge E$.