The cokernel of a Cauchy–Riemann operator is the kernel of its conjugated formal adjoint

Proved

CauchyRiemannIndex.cokernel_eq_kernel_adjoint

by Mazecto · Oct 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

cauchy-riemannconley-zehnder-indexfredholm-indexsobolev-spacessymplectic-geometry

Let $1<p<\infty$ , let $S^\pm$ be continuous loops of symmetric matrices and let $S:\mathbb{R}\times S^1\to\mathbb{R}^{2n\times2n}$ be continuous with $S(s,\cdot)\to S^\pm$ uniformly as $s\to\pm\infty$ ; $D_S=\partial_s+J_0\partial_t+S(s,t)$ . Assume that the asymptotic operators $A^\pm=-J_0\partial_t-S^\pm(t)$ are nondegenerate. Let $1/p+1/q=1$ , let $C$ be complex conjugation on $\mathbb{C}^n=\mathbb{R}^{2n}$ and $\bar S(s,t)=-C\,S(s,t)^{\mathsf T}C$ . Then the cokernel $L^p/\operatorname{im}(D_S:W^{1,p}\to L^p)$ is finite-dimensional, and

\dim\operatorname{coker}\big(D_S:W^{1,p}\to L^p\big)=\dim\ker\big(D_{\bar S}:W^{1,q}\to L^q\big).

Formalization Note $p$ is in ℝ≥0∞ with Fact (1 ≤ p), $1<p$ and $p\ne\infty$ . The hypotheses on $S$ are IsSymLoop S± and IsAsymptoticTo S Splus Sminus. Nondegeneracy is IsNondegenerate S±: $\det(\mathrm{Id}-\Psi(1))\ne0$ for the fundamental solution $\Psi$ . $C$ is conjMat n; $q$ is in ℝ≥0∞ with Fact (1 ≤ q) and 1 / p + 1 / q = 1. $D_{\bar S}=-C\,D_S^*\,C$ , where $D_S^*$ is the formal adjoint of $D_S$ .

Preamble

import Definitions.Def_CauchyRiemannIndex_Setting
import Mathlib.Analysis.Calculus.ContDiff.Basic

Formal statement

namespace CauchyRiemannIndex

open MeasureTheory Matrix Filter Topology
open scoped ENNReal NNReal ContDiff RealInnerProductSpace

/-- Wendl, Lemma 4.17, Proposition 4.18 and Theorem 4.20 (pp. 76–79), on the cylinder: let `D_S`
be asymptotic to nondegenerate loops `S±` of symmetric matrices, `1 < p < ∞` and
`1/p + 1/q = 1`. The cokernel of `D_S : W^{1,p} → L^p` is finite-dimensional, and its dimension
is that of the kernel of the conjugated formal adjoint `D_{S̄} : W^{1,q} → L^q`,
`S̄(s, t) = -C S(s, t)ᵀ C`, where `C` is complex conjugation on `ℂⁿ = ℝ²ⁿ`. -/
theorem cokernel_eq_kernel_adjoint (n : ℕ) (p : ℝ≥0∞) [Fact (1 ≤ p)] (hp : 1 < p) (hp' : p ≠ ⊤)
    (Splus Sminus : ℝ → Mat n) (hSplus : IsSymLoop Splus) (hSminus : IsSymLoop Sminus)
    (S : ℝ × ℝ → Mat n) (hS : IsAsymptoticTo S Splus Sminus) (hplus : IsNondegenerate Splus) (hminus : IsNondegenerate Sminus)
    (q : ℝ≥0∞) [Fact (1 ≤ q)] (hpq : 1 / p + 1 / q = 1) :
    FiniteDimensional ℝ (LpCyl n p ⧸ crRange p S) ∧
      Module.finrank ℝ (LpCyl n p ⧸ crRange p S) =
        Module.finrank ℝ (crKernel q (fun x => -(conjMat n * (S x)ᵀ * conjMat n))) := by
  sorry

end CauchyRiemannIndex

Source

C. Wendl, Lectures on Symplectic Field Theory, arXiv:1612.01009, https://arxiv.org/abs/1612.01009, Lecture 4, Lemma 4.17, Proposition 4.18 and Theorem 4.20, pp. 76–79

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `CauchyRiemannIndex.cokernel_eq_kernel_adjoint`

Setting. $n$ ; $p,q\in[1,\infty]$ (both with Fact (1 ≤ ·)); loops $S^\pm$ ; a coefficient $S$ .

Hypotheses.

$1<p<\infty$ and $1/p+1/q=1$ in $\mathbb R_{\ge0}^\infty$ , so $q=p/(p-1)\in(1,\infty)$ .
$S^\pm$ are symmetric loops.
IsAsymptoticTo S S⁺ S⁻.
$S^\pm$ are nondegenerate.

Definitions used.

crRange p S $=D_S(W^{1,p})\subseteq L^p$ .
LpCyl n p ⧸ crRange p S is the algebraic cokernel.
crKernel q S̄ is the kernel of $D_{\bar S}=\partial_s+J_0\partial_t+\bar S$ on $W^{1,q}$ , with $\bar S(s,t)=-C\,S(s,t)^T C$ and $C=$ conjMat $=\mathrm{diag}(I,-I)$ .

Conclusion.

\dim_{\mathbb R}\big(L^p/D_S(W^{1,p})\big)<\infty\quad\text{and}\quad \dim\big(L^p/D_S(W^{1,p})\big)=\dim\ker\big(D_{\bar S}:W^{1,q}\to L^q\big).

Degenerate cases. For $n=0$ it is trivial. The first conjunct makes the left finrank genuine, not the junk $0$ . The right finrank would be junk $0$ if $\ker D_{\bar S}$ were infinite-dimensional, but it is not: $\bar S$ is asymptotic to $-CS^\pm C$ , which are symmetric and nondegenerate (conjugate loops). So by the semi-Fredholm property its kernel is finite-dimensional.

Remarks. Check of the conjugation. The $L^2$ -formal adjoint is $D_S^*=-\partial_s+J_0\partial_t+S^T$ . For $\zeta=C\xi$ , using $CJ_0=-J_0C$ and $C^2=1$ :

-C\,D_S^*\xi=\partial_s\zeta+J_0\partial_t\zeta-CS^TC\zeta=D_{\bar S}\zeta .

So $\xi\mapsto C\xi$ is a pointwise isometric isomorphism $\ker D_S^*\cong\ker D_{\bar S}$ , preserving $L^q$ and $W^{1,q}$ . With no $s$ -reflection needed, the sign and transpose conventions are correct.

Soundness checks.

1 / p + 1 / q = 1 is ENNReal arithmetic. With $1<p<\infty$ it pins $q$ to the conjugate exponent, with no junk; even $p=1$ would force $q=\infty$ , but $p>1$ is assumed. The lambda fun x => -(conjMat n * (S x)ᵀ * conjMat n) is the correct $\bar S$ , and its transpose binds to S x. The Fact (1 ≤ q) instance is consistent with hpq. finrank on both sides is in $\mathbb N$ , so the equation is between naturals.
Not vacuous. It is true: the range is closed (semi-Fredholm), so $(L^p/\mathrm{range})^*\cong\mathrm{range}^\perp\subseteq L^q$ . The annihilator equals the weak kernel of $D_S^*$ , which lies in $W^{1,q}$ by regularity, and that is $\cong\ker D_{\bar S}$ . Finite-dimensionality follows from that of $\ker D_{\bar S}$ , and the dual of a finite-dimensional space has the same dimension.

Verdict: no mis-formalization observed

Human review

Endorsed by Shuze Chen · Oct 14, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 14, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

The cokernel of a Cauchy–Riemann operator is the kernel of its conjugated formal adjoint

Read-back: CauchyRiemannIndex.cokernel_eq_kernel_adjoint

Read-back: `CauchyRiemannIndex.cokernel_eq_kernel_adjoint`