The Fredholm index of Cauchy–Riemann operators on the cylinder is constant along continuous families with nondegenerate ends

Let $1<p<\infty$ and $n\ge0$. For $\tau\in[0,1]$ let $S_\tau:\mathbb{R}\times S^1\to\mathbb{R}^{2n\times2n}$ be continuous coefficients with $S_\tau(s,\cdot)\to P_\tau$ as $s\to+\infty$ and $S_\tau(s,\cdot)\to M_\tau$ as $s\to-\infty$, uniformly, where $P_\tau,M_\tau$ are continuous loops of symmetric matrices whose asymptotic operators $-J_0\partial_t-P_\tau$ and $-J_0\partial_t-M_\tau$ are nondegenerate. Assume $\tau\mapsto S_\tau$ is continuous in the sup norm: for every $\tau$ and $\varepsilon>0$ there is $\delta>0$ with $|S_\sigma(s,t)_{ij}-S_\tau(s,t)_{ij}|\le\varepsilon$ for all $(s,t)$ and all entries whenever $|\sigma-\tau|<\delta$. Then the Cauchy–Riemann operators $D_{S_\tau}=\partial_s+J_0\partial_t+S_\tau:W^{1,p}(\mathbb{R}\times S^1,\mathbb{R}^{2n})\to L^p(\mathbb{R}\times S^1,\mathbb{R}^{2n})$ satisfy

This is the homotopy invariance of the Fredholm index on the cylinder: the asymptotic loops may move with $\tau$ as long as they stay nondegenerate. It reduces index comparisons to the construction of such families.

Formalization Note The family is S : unitInterval → ℝ × ℝ → Mat n with loops P M : unitInterval → ℝ → Mat n; each S τ satisfies IsAsymptoticTo (S τ) (P τ) (M τ) (positive end first), the loops satisfy IsSymLoop and IsNondegenerate, and the index is crIndex p $=\dim\ker D_S-\dim\operatorname{coker}D_S$ from the setting module. No continuity of the loops in $\tau$ is assumed.