From af31d03a9baadc8523838b46d30165a4c9d142cd Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 10:08:02 -0400 Subject: [PATCH 1/8] Sync blueprint with CompactOperators.lean and FourierHolomorphic.lean (M3a/M3b) Add the "Compact perturbations of the identity" subsection (Riesz-Schauder Fredholm theorem and its supporting lemmas) and the new "Fourier-coefficient recursion" section covering periodIntegral_eq_of_periodic, the holSection/ holCoeff machinery, and the exact dimension count dim H^0(L_k) = k, dim H^1(L_k) = 0. Update the theta-sections status note and chapter intro accordingly. Co-Authored-By: Claude Sonnet 4.6 --- blueprint/src/content.tex | 137 ++++++++++++++++++++++++++++++++++++-- 1 file changed, 130 insertions(+), 7 deletions(-) diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 99f599b..4b72f19 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -355,9 +355,11 @@ \chapter{Examples} triple; the two-torus example (Section~\ref{sec:torus}) is a complete, finitely summable, even spectral triple with vanishing index. Sections~\ref{sec:shift} and~\ref{sec:magnetic-dirac} give two further examples with \emph{nonzero} Fredholm index, $-1$ and $k$ respectively, completing -the index arc $0, -1, k$. Section~\ref{sec:theta-sections} begins connecting the abstract -flux-$k$ model of Section~\ref{sec:magnetic-dirac} back to genuine geometry, by exhibiting $k$ -independent holomorphic sections of the degree-$k$ line bundle on the square torus. +the index arc $0, -1, k$. Sections~\ref{sec:theta-sections} and~\ref{sec:fourier-holomorphic} +connect the abstract flux-$k$ model of Section~\ref{sec:magnetic-dirac} back to genuine +geometry: together they give a complete, purely algebraic dimension count +$\dim H^0(L_k) = k$, $\dim H^1(L_k) = 0$ for the degree-$k$ line bundle on the square torus, +with no index theorem and no $L^2$ analysis. \section{Block-diagonal operators on \texorpdfstring{$\ell^2$}{l2}} \label{sec:diagonal-operators} @@ -684,15 +686,17 @@ \section{The flux-\texorpdfstring{$k$}{k} magnetic Dirac model} \section{Theta sections on the square torus} \label{sec:theta-sections} -\textbf{Status: partial (lower bound only).} This section proves the lower-bound half of the +\textbf{Status: complete (lower bound).} This section proves the lower-bound half of the square-torus flux-$k$ Landau-level computation directly on the geometric side: $k$ explicit holomorphic theta sections for the degree-$k$ line bundle on the square torus $\mathbb{C} / (\mathbb{Z} + i \mathbb{Z})$ are exhibited and shown linearly independent, giving $\dim \ker D^{+} \geq k$ for the \emph{geometric} Dirac operator twisted by the degree-$k$ bundle (as opposed to the magnetic-translation model of Section~\ref{sec:magnetic-dirac}). The matching -upper bound $\dim \ker D^{+} \leq k$, the vanishing of the cokernel, and the resulting -identification of the geometric index with the model index $k$ -(Theorem~\ref{thm:fredholmIndex-magneticDirac}) are deferred; see +upper bound $\dim \ker D^{+} \leq k$ and the vanishing of the cokernel are completed in +Section~\ref{sec:fourier-holomorphic}. The resulting identification of the geometric index +with the model index $k$ (Theorem~\ref{thm:fredholmIndex-magneticDirac}) — which additionally +needs the $L^2$-to-holomorphic bridge (elliptic regularity for $\bar\partial$, not in Mathlib) +and the unitary equivalence to the magnetic model — is deferred; see \texttt{SpectralTriples/docs/INDEX\_PAIRING.md} for the roadmap. \begin{definition}[Explicit degree-$k$ theta sections] @@ -746,3 +750,122 @@ \section{Theta sections on the square torus} eigenvalues $\omega_k^{0}, \dots, \omega_k^{k-1}$ (the $k$ distinct $k$-th roots of unity), hence independent. \end{theorem} + +\section{The Fourier-coefficient recursion: an exact dimension count} +\label{sec:fourier-holomorphic} + +\textbf{Status: complete (M3a, M3b).} This section completes the dimension count begun in +Section~\ref{sec:theta-sections} (M2) by an entirely algebraic route, with \emph{no index +theorem and no $L^2$ analysis}: the upper bound $\dim H^0(L_k) \leq k$ (M3a) and the +cokernel vanishing $\dim H^1(L_k) = 0$ (M3b). Both rest on a single new analytic lemma not in +Mathlib — the \emph{contour shift} — from which a Fourier-coefficient recursion is derived +algebraically. See \texttt{SpectralTriples/docs/INDEX\_PAIRING.md} for the full roadmap; the +remaining gap (M3c/M4: the $L^2$-to-holomorphic bridge and the unitary equivalence to the +magnetic model of Section~\ref{sec:magnetic-dirac}) is the genuinely analytic frontier and is +not addressed here. + +\begin{theorem}[Contour shift] + \label{thm:periodIntegral-eq-of-periodic} + \lean{SpectralTriples.periodIntegral_eq_of_periodic} + \leanok + For an entire $1$-periodic function $f$, the period integral $\int_0^1 f(x+iy)\,dx$ does not + depend on the height $y$. (Cauchy--Goursat on the rectangle $[0,1] \times [y_1,y_2]$: the two + vertical sides cancel by periodicity, leaving the two horizontal integrals equal.) +\end{theorem} + +\begin{definition}[Holomorphic sections of the degree-$k$ line bundle] + \label{def:holSection} + \lean{SpectralTriples.holSection} + \leanok + $H^0(L_k)$: the space of entire functions $f$ with $f(z+1) = f(z)$ and the degree-$k$ + automorphy factor $f(z+i) = e^{-\pi i k(2z+i)} f(z)$ — the same quasi-periodicity conditions + satisfied by the theta sections of Definition~\ref{def:thetaSection}. +\end{definition} + +\begin{definition}[Fourier coefficient of a periodic holomorphic function] + \label{def:holCoeff} + \lean{SpectralTriples.holCoeff} + \leanok + For a $1$-periodic function $f$, the Fourier coefficient $a_m = \int_0^1 f(x)\, + e^{-2\pi i m x}\,dx$, computed on the real period. +\end{definition} + +\begin{lemma}[The Fourier-coefficient recursion] + \label{lem:holCoeff-recursion} + \lean{SpectralTriples.holCoeff_recursion} + \leanok + \uses{def:holSection, def:holCoeff, thm:periodIntegral-eq-of-periodic} + For $f \in H^0(L_k)$, the Fourier coefficients satisfy + \[ + a_{m+k} = e^{-\pi(2m+k)} \, a_m. + \] + Comparing Fourier coefficients of the degree-$k$ automorphy relation, via the contour shift + (Theorem~\ref{thm:periodIntegral-eq-of-periodic}) relating $f$'s Fourier coefficients on + different horizontal lines, turns the quasi-periodicity condition into this purely algebraic + recursion: the whole coefficient sequence is determined by $(a_0, \dots, a_{k-1})$. +\end{lemma} + +\begin{theorem}[Fourier completeness: vanishing coefficients imply $f = 0$] + \label{thm:eq-zero-of-holCoeff-eq-zero} + \lean{SpectralTriples.eq_zero_of_holCoeff_eq_zero} + \leanok + \uses{def:holCoeff} + If $f$ is entire and $1$-periodic with all Fourier coefficients $a_m = 0$, then $f = 0$: + lifting $f$ to the circle, Mathlib's Fourier completeness gives $f$ vanishes on $\mathbb{R}$, + and the identity theorem for the entire function $f$ then gives $f \equiv 0$ on $\mathbb{C}$. +\end{theorem} + +\begin{theorem}[The upper bound: $\dim H^0(L_k) \leq k$] + \label{thm:holSection-finrank-le} + \lean{SpectralTriples.holSection_finrank_le} + \leanok + \uses{lem:holCoeff-recursion, thm:eq-zero-of-holCoeff-eq-zero} + The restriction map $f \mapsto (a_0, \dots, a_{k-1})$ is an injective linear map + $H^0(L_k) \to \mathbb{C}^k$: by the recursion (Lemma~\ref{lem:holCoeff-recursion}), + $a_0 = \cdots = a_{k-1} = 0$ forces every Fourier coefficient to vanish, hence $f = 0$ by + Theorem~\ref{thm:eq-zero-of-holCoeff-eq-zero}. Injectivity gives $\dim H^0(L_k) \leq k$. +\end{theorem} + +\begin{theorem}[The exact count: $\dim H^0(L_k) = k$] + \label{thm:holSection-finrank-eq} + \lean{SpectralTriples.holSection_finrank_eq} + \leanok + \uses{thm:holSection-finrank-le, thm:thetaSection-linearIndependent} + Combining the upper bound of Theorem~\ref{thm:holSection-finrank-le} (M3a) with the lower + bound of Theorem~\ref{thm:thetaSection-linearIndependent} (M2, the theta sections span a + $k$-dimensional subspace) gives $\dim H^0(L_k) = k$ exactly — a complete dimension theorem + with no index theorem and no $L^2$ analysis. +\end{theorem} + +\begin{definition}[Holomorphic sections of the degree-$(-k)$ line bundle] + \label{def:holSectionNeg} + \lean{SpectralTriples.holSectionNeg} + \leanok + $H^0(L_{-k})$: the same definition as $H^0(L_k)$ (Definition~\ref{def:holSection}) but with + the opposite-sign automorphy factor $f(z+i) = e^{\pi i k(2z+i)} f(z)$. By Serre duality this + represents $H^1(L_k)$, the cokernel of the degree-$k$ Dirac operator. +\end{definition} + +\begin{lemma}[Parseval decay of Fourier coefficients] + \label{lem:holCoeff-tendsto-atTop-zero} + \lean{SpectralTriples.holCoeff_tendsto_atTop_zero} + \leanok + \uses{def:holCoeff} + For any entire $1$-periodic $f$, the Fourier coefficients $a_m \to 0$ as $m \to \infty$ (and + as $m \to -\infty$): a consequence of $\ell^2$-summability of $|a_m|^2$ (Parseval, via the + $L^2$ lift to the circle). +\end{lemma} + +\begin{theorem}[The cokernel vanishes: $\dim H^0(L_{-k}) = 0$] + \label{thm:holSectionNeg-eq-bot} + \lean{SpectralTriples.holSectionNeg_eq_bot, SpectralTriples.holSectionNeg_finrank_eq_zero} + \leanok + \uses{def:holSectionNeg, lem:holCoeff-recursion, lem:holCoeff-tendsto-atTop-zero, + thm:eq-zero-of-holCoeff-eq-zero} + $H^0(L_{-k}) = 0$ for $k > 0$ (equivalently $\dim H^1(L_k) = 0$, the cokernel-vanishing half + of $\operatorname{index} = k$, via Serre duality $h^1(L_k) = h^0(L_k^{-1})$). The + opposite-sign automorphy gives the opposite-sign recursion $a_{m+k} = e^{\pi(2m+k)} a_m$, + whose growth factor has modulus $> 1$; this clashes with the Parseval decay of + Lemma~\ref{lem:holCoeff-tendsto-atTop-zero} unless every coefficient is already $0$, and then + Theorem~\ref{thm:eq-zero-of-holCoeff-eq-zero} gives $f = 0$. +\end{theorem} From 0408535fc96188d971f2954bbe2514153183dc28 Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 10:08:12 -0400 Subject: [PATCH 2/8] Deduplicate the closed-range cokernel argument MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Examples/Shift.lean proved finrank_quotient_range_eq_orthogonal by hand for H over ℂ, while CompactOperators.lean's isFredholm_one_sub independently derived the same underlying fact (quotient by a closed-range submodule is linearly equivalent to its orthogonal complement) inline, for general RCLike 𝕜. Extract the shared fact as Submodule.quotientEquivOrthogonal (plus the finrank and FiniteDimensional-transfer corollaries) in CompactOperators.lean, generalized to RCLike 𝕜, and have both call sites reuse it. Also backfills scripts/axiom_report.lean, which never picked up CompactOperators.lean's tracked declarations (IsCompactOperator.adjoint, isFredholm_one_sub, etc.) after the chiral-fredholm merge. Co-Authored-By: Claude Sonnet 4.6 --- SpectralTriples/CompactOperators.lean | 30 ++++++++++++++++++++++++--- SpectralTriples/Examples/Shift.lean | 18 ++++------------ audit/axiom-report.txt | 9 +++++++- scripts/axiom_report.lean | 10 ++++++++- 4 files changed, 48 insertions(+), 19 deletions(-) diff --git a/SpectralTriples/CompactOperators.lean b/SpectralTriples/CompactOperators.lean index 1636a9d..2f2fbb5 100644 --- a/SpectralTriples/CompactOperators.lean +++ b/SpectralTriples/CompactOperators.lean @@ -185,6 +185,32 @@ theorem adjoint {K : H →L[𝕜] H} (hK : IsCompactOperator K) : end IsCompactOperator +namespace Submodule + +/-- For a submodule of a Hilbert space with an orthogonal projection (e.g. one with closed +range), the quotient by it is linearly equivalent to its orthogonal complement. -/ +noncomputable def quotientEquivOrthogonal (K : Submodule 𝕜 H) [K.HasOrthogonalProjection] : + (H ⧸ K) ≃ₗ[𝕜] Kᗮ := + Submodule.quotientEquivOfIsCompl K Kᗮ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection + +omit [CompleteSpace H] in +/-- The quotient by a submodule with an orthogonal projection has the same finite dimension as +its orthogonal complement. -/ +theorem finrank_quotient_eq_finrank_orthogonal (K : Submodule 𝕜 H) [K.HasOrthogonalProjection] : + Module.finrank 𝕜 (H ⧸ K) = Module.finrank 𝕜 Kᗮ := + (K.quotientEquivOrthogonal).finrank_eq + +omit [CompleteSpace H] in +/-- The quotient by a submodule with an orthogonal projection is finite-dimensional whenever +its orthogonal complement is. -/ +theorem finiteDimensional_quotient_of_finiteDimensional_orthogonal (K : Submodule 𝕜 H) + [K.HasOrthogonalProjection] [FiniteDimensional 𝕜 Kᗮ] : + FiniteDimensional 𝕜 (H ⧸ K) := + FiniteDimensional.of_injective (K.quotientEquivOrthogonal).toLinearMap + (K.quotientEquivOrthogonal).injective + +end Submodule + namespace SpectralTriples.Fredholm /-- **Fredholm-ness of compact perturbations of the identity** (the structural part of the @@ -344,10 +370,8 @@ theorem isFredholm_one_sub {K : H →L[𝕜] H} (hK : IsCompactOperator K) : exact (ContinuousLinearMap.adjoint K).finite_dimensional_eigenspace hKadj 1 one_ne_zero haveI hcokerfd : FiniteDimensional 𝕜 (LinearMap.range T.toLinearMap)ᗮ := by rw [T.orthogonal_range]; exact hNadjfd - have hequiv := Submodule.quotientEquivOfIsCompl (LinearMap.range T.toLinearMap) - (LinearMap.range T.toLinearMap)ᗮ Submodule.isCompl_orthogonal_of_hasOrthogonalProjection haveI : FiniteDimensional 𝕜 (H ⧸ LinearMap.range T.toLinearMap) := - FiniteDimensional.of_injective hequiv.toLinearMap hequiv.injective + (LinearMap.range T.toLinearMap).finiteDimensional_quotient_of_finiteDimensional_orthogonal exact ⟨hNfd, hclosed_T, ‹FiniteDimensional 𝕜 (H ⧸ LinearMap.range T.toLinearMap)›⟩ end SpectralTriples.Fredholm diff --git a/SpectralTriples/Examples/Shift.lean b/SpectralTriples/Examples/Shift.lean index 07e8aa1..e0440a5 100644 --- a/SpectralTriples/Examples/Shift.lean +++ b/SpectralTriples/Examples/Shift.lean @@ -9,6 +9,7 @@ module public import Mathlib.Analysis.InnerProductSpace.l2Space public import Mathlib.LinearAlgebra.FiniteDimensional.Basic public import SpectralTriples.Fredholm +public import SpectralTriples.CompactOperators /-! # The unilateral shift on `ℓ²(ℕ)` @@ -190,19 +191,6 @@ theorem range_shift_orthogonal_finrank : rw [range_shift_orthogonal] exact finrank_span_singleton e0_ne_zero -/-- For a closed range in a Hilbert space, the quotient cokernel has the same dimension as the -orthogonal-complement cokernel. -/ -theorem finrank_quotient_range_eq_orthogonal {H : Type*} [NormedAddCommGroup H] - [InnerProductSpace ℂ H] [CompleteSpace H] (T : H →L[ℂ] H) - (hclosed : IsClosed (LinearMap.range (T : H →ₗ[ℂ] H) : Set H)) : - Module.finrank ℂ (H ⧸ LinearMap.range (T : H →ₗ[ℂ] H)) - = Module.finrank ℂ (LinearMap.range (T : H →ₗ[ℂ] H))ᗮ := by - let K : Submodule ℂ H := LinearMap.range (T : H →ₗ[ℂ] H) - change Module.finrank ℂ (H ⧸ K) = Module.finrank ℂ ↥Kᗮ - haveI : CompleteSpace K := hclosed.completeSpace_coe - exact (Submodule.quotientEquivOfIsCompl K Kᗮ - Submodule.isCompl_orthogonal_of_hasOrthogonalProjection).finrank_eq - /-- The range of the unilateral shift is closed. -/ theorem isClosed_range_shift : IsClosed (LinearMap.range (shift : H →ₗ[ℂ] H) : Set H) := by @@ -222,9 +210,11 @@ theorem isClosed_range_shift : /-- The forward unilateral shift on `ℓ²(ℕ)` is Fredholm of index `-1`. -/ theorem fredholmIndex_shift : SpectralTriples.Fredholm.index (shift : H →ₗ[ℂ] H) = -1 := by + haveI : CompleteSpace (LinearMap.range (shift : H →ₗ[ℂ] H)) := + isClosed_range_shift.completeSpace_coe unfold SpectralTriples.Fredholm.index rw [shift_ker_eq_bot, finrank_bot, - finrank_quotient_range_eq_orthogonal shift isClosed_range_shift, + (LinearMap.range (shift : H →ₗ[ℂ] H)).finrank_quotient_eq_finrank_orthogonal, range_shift_orthogonal_finrank] norm_num diff --git a/audit/axiom-report.txt b/audit/axiom-report.txt index a2ab0ff..7668e09 100644 --- a/audit/axiom-report.txt +++ b/audit/axiom-report.txt @@ -25,6 +25,14 @@ 'SpectralTriples.Fredholm.index' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.Fredholm.isFredholm_of_bijective' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.Fredholm.index_of_bijective' depends on axioms: [propext, Classical.choice, Quot.sound] +'IsCompactOperator.exists_finiteRank_norm_sub_lt' depends on axioms: [propext, Classical.choice, Quot.sound] +'ContinuousLinearMap.finiteDimensional_range_adjoint' depends on axioms: [propext, Classical.choice, Quot.sound] +'IsCompactOperator.adjoint' depends on axioms: [propext, Classical.choice, Quot.sound] +'Submodule.finrank_quotient_eq_finrank_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound] +'Submodule.finiteDimensional_quotient_of_finiteDimensional_orthogonal' depends on axioms: [propext, + Classical.choice, + Quot.sound] +'SpectralTriples.Fredholm.isFredholm_one_sub' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.Dkernel' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.index' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.finiteDimensional_Dkernel' depends on axioms: [propext, Classical.choice, Quot.sound] @@ -62,7 +70,6 @@ 'SpectralTriples.Torus.isFinitelySummableSpectralTriple' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.Torus.index_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.Shift.shift' depends on axioms: [propext, Classical.choice, Quot.sound] -'SpectralTriples.Shift.finrank_quotient_range_eq_orthogonal' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.Shift.fredholmIndex_shift' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.MagneticDirac.magneticDirac' depends on axioms: [propext, Classical.choice, Quot.sound] 'SpectralTriples.MagneticDirac.magneticDirac_ker_finrank' depends on axioms: [propext, Classical.choice, Quot.sound] diff --git a/scripts/axiom_report.lean b/scripts/axiom_report.lean index 4e9a98a..80a6918 100644 --- a/scripts/axiom_report.lean +++ b/scripts/axiom_report.lean @@ -55,6 +55,15 @@ open LinearPMap #print axioms SpectralTriples.Fredholm.isFredholm_of_bijective #print axioms SpectralTriples.Fredholm.index_of_bijective +-- CompactOperators.lean — compact operators on Hilbert space are Riesz–Schauder Fredholm +-- perturbations of the identity (not yet in Mathlib). +#print axioms IsCompactOperator.exists_finiteRank_norm_sub_lt +#print axioms ContinuousLinearMap.finiteDimensional_range_adjoint +#print axioms IsCompactOperator.adjoint +#print axioms Submodule.finrank_quotient_eq_finrank_orthogonal +#print axioms Submodule.finiteDimensional_quotient_of_finiteDimensional_orthogonal +#print axioms SpectralTriples.Fredholm.isFredholm_one_sub + -- Index.lean — the graded-kernel index of an even spectral triple. #print axioms SpectralTriples.Dkernel #print axioms SpectralTriples.index @@ -105,7 +114,6 @@ open LinearPMap -- Examples/Shift.lean — the unilateral shift on ℓ²(ℕ): a Fredholm operator of index −1. #print axioms SpectralTriples.Shift.shift -#print axioms SpectralTriples.Shift.finrank_quotient_range_eq_orthogonal #print axioms SpectralTriples.Shift.fredholmIndex_shift -- Examples/MagneticDirac.lean — flux-k magnetic Dirac model: index = k, with magnetic translations. From 1f4161e4164627995b61bbded1b081549775b2ab Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 10:52:00 -0400 Subject: [PATCH 3/8] Generalize the diagonal-operator domain/self-adjointness argument Circle.lean and Torus.lean each proved, by hand, that their respective diagonal Dirac operator (scalar eigenvalues vs. 2x2 Hermitian spinor blocks) is self-adjoint on its maximal H^1 domain, via an essentially identical argument: symmetry from the blocks being Hermitian, domain density via testing against single-mode basis vectors, and the adjoint-domain inclusion by testing the adjoint relation against the same vectors. Extract this as a generic construction in DiagonalOperator.lean (lpDiag.diracDomain/diracDirac/diracDirac_isSelfAdjoint, parametrized by any family of symmetric blocks B i : G i ->l[k] G i), and have both Circle.lean and Torus.lean instantiate it instead of duplicating the proof. All public names and statements are preserved exactly (diracDomain, mem_diracDomain_iff, diracDirac, diracDirac_apply, diracDirac_isSelfAdjoint), so every downstream theorem (resolvent compactness, representation, grading, index_eq_zero) is unaffected -- verified axiom-clean, and the regenerated axiom report is byte-identical to the existing golden file. Co-Authored-By: Claude Sonnet 4.6 --- SpectralTriples/DiagonalOperator.lean | 137 ++++++++++++++++++++++++- SpectralTriples/Examples/Circle.lean | 130 +++++------------------- SpectralTriples/Examples/Torus.lean | 139 ++++---------------------- 3 files changed, 180 insertions(+), 226 deletions(-) diff --git a/SpectralTriples/DiagonalOperator.lean b/SpectralTriples/DiagonalOperator.lean index a1da530..5d05abd 100644 --- a/SpectralTriples/DiagonalOperator.lean +++ b/SpectralTriples/DiagonalOperator.lean @@ -8,6 +8,7 @@ module public import Mathlib.Analysis.InnerProductSpace.l2Space public import Mathlib.Analysis.Normed.Operator.Compact.Basic +public import Mathlib.Analysis.InnerProductSpace.LinearPMap /-! # Block-diagonal operators on `ℓ²` @@ -40,7 +41,7 @@ exactly such block-diagonal operators with block norms `→ 0`. namespace lpDiag open scoped Topology -open Filter +open Filter LinearPMap variable {α 𝕜 : Type*} [RCLike 𝕜] {G : α → Type*} [∀ i, NormedAddCommGroup (G i)] [∀ i, InnerProductSpace 𝕜 (G i)] @@ -217,4 +218,138 @@ theorem isCompactOperator_diagL (T : ∀ i, G i →L[𝕜] G i) {C : ℝ} (hC0 : exact tendsto_one_div_add_atTop_nhds_zero_nat exact isCompactOperator_of_tendsto htends (Filter.Eventually.of_forall hcompact) +/-! ### The unbounded block-diagonal Dirac operator + +Given a family of *symmetric* (Hermitian) blocks `B i : G i →ₗ[𝕜] G i`, this section builds the +associated unbounded "diagonal Dirac operator" on its maximal domain in `ℓ²(α; G)`, and proves +it is self-adjoint. This is the analytic core shared by the `S¹` and `T²` Dirac examples: the +circle's scalar multiplication by `n` and the torus's `2×2` spinor blocks are both instances of +a symmetric block family, differing only in the fibre `G i` and the block `B i`. -/ + +variable [∀ i, CompleteSpace (G i)] [DecidableEq α] + +/-- The maximal domain of the unbounded block-diagonal operator with blocks `B`: those `a` for +which `i ↦ B i (aᵢ)` is again square-summable. -/ +def diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) : Submodule 𝕜 (lp G 2) where + carrier := {a | Memℓp (fun i => B i (a i)) 2} + zero_mem' := by + have hzero : (fun i => B i ((0 : lp G 2) i)) = 0 := by + funext i; simp only [lp.coeFn_zero, Pi.zero_apply, _root_.map_zero] + simp only [Set.mem_setOf_eq, hzero]; exact zero_memℓp + add_mem' := fun {a b} ha hb => by + have heq : (fun i => B i ((a + b) i)) = (fun i => B i (a i)) + fun i => B i (b i) := by + funext i; simp only [lp.coeFn_add, Pi.add_apply, _root_.map_add] + rw [Set.mem_setOf_eq, heq]; exact ha.add hb + smul_mem' := fun c a ha => by + have heq : (fun i => B i ((c • a) i)) = c • fun i => B i (a i) := by + funext i; simp only [lp.coeFn_smul, Pi.smul_apply, _root_.map_smul] + rw [Set.mem_setOf_eq, heq]; exact ha.const_smul c + +omit [∀ i, CompleteSpace (G i)] [DecidableEq α] in +theorem mem_diracDomain_iff (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) : + a ∈ diracDomain B ↔ Memℓp (fun i => B i (a i)) 2 := Iff.rfl + +/-- Coordinatewise application of the blocks, as an element of `ℓ²(α; G)`, given a proof the +result is square-summable. -/ +noncomputable def applyDirac (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) + (h : Memℓp (fun i => B i (a i)) 2) : lp G 2 := + ⟨fun i => B i (a i), h⟩ + +omit [∀ i, CompleteSpace (G i)] [DecidableEq α] in +@[simp] theorem coe_applyDirac (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) (h) (i : α) : + (applyDirac B a h) i = B i (a i) := rfl + +/-- The unbounded block-diagonal operator on `ℓ²(α; G)` with blocks `B`, on its maximal domain +`diracDomain B`. -/ +noncomputable def diracDirac (B : ∀ i, G i →ₗ[𝕜] G i) : lp G 2 →ₗ.[𝕜] lp G 2 where + domain := diracDomain B + toFun := + { toFun := fun a => applyDirac B (a : lp G 2) ((mem_diracDomain_iff B _).mp a.2) + map_add' := fun a b => by + refine lp.ext (funext fun i => ?_) + simp only [coe_applyDirac, Submodule.coe_add, lp.coeFn_add, Pi.add_apply, + _root_.map_add] + map_smul' := fun c a => by + refine lp.ext (funext fun i => ?_) + simp only [coe_applyDirac, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply, + _root_.map_smul, RingHom.id_apply] } + +@[simp] theorem diracDirac_apply (B : ∀ i, G i →ₗ[𝕜] G i) (a : diracDomain B) (i : α) : + (diracDirac B a) i = B i ((a : lp G 2) i) := rfl + +/-- The block-diagonal operator is symmetric (formally self-adjoint) when each block is. -/ +theorem diracDirac_isFormalAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) : + (diracDirac B).IsFormalAdjoint (diracDirac B) := by + intro x y + rw [lp.inner_eq_tsum, lp.inner_eq_tsum] + refine tsum_congr fun i => ?_ + rw [diracDirac_apply, diracDirac_apply] + exact hB i _ _ + +/-- Each single-mode vector lies in the maximal domain. -/ +theorem single_mem_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : + (lp.single 2 i v : lp G 2) ∈ diracDomain B := by + rw [mem_diracDomain_iff] + have hfun : (fun q => B q ((lp.single 2 i v : lp G 2) q)) + = ⇑(lp.single 2 i (B i v) : lp G 2) := by + funext q + rcases eq_or_ne q i with h | h + · subst h; simp [lp.single_apply] + · simp [lp.single_apply, h, _root_.map_zero] + rw [hfun] + exact lp.memℓp _ + +/-- The image of a single-mode vector under the diagonal operator. -/ +theorem diracDirac_single (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : + diracDirac B ⟨lp.single 2 i v, single_mem_diracDomain B i v⟩ + = (lp.single 2 i (B i v) : lp G 2) := by + refine lp.ext (funext fun q => ?_) + rcases eq_or_ne q i with h | h + · subst h; simp [diracDirac_apply, lp.single_apply] + · simp [diracDirac_apply, lp.single_apply, h, _root_.map_zero] + +/-- The maximal domain is dense: it contains every single-mode vector. -/ +theorem dense_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) : + Dense ((diracDirac B).domain : Set (lp G 2)) := by + change Dense (diracDomain B : Set (lp G 2)) + have horth : (diracDomain B : Submodule 𝕜 (lp G 2))ᗮ = ⊥ := by + rw [Submodule.eq_bot_iff] + intro y hy + refine lp.ext (funext fun i => ?_) + refine ext_inner_left 𝕜 fun v => ?_ + have h0 : inner 𝕜 (lp.single 2 i v : lp G 2) y = 0 := hy _ (single_mem_diracDomain B i v) + rw [lp.inner_single_left] at h0 + rw [h0, lp.coeFn_zero, Pi.zero_apply, inner_zero_right] + have htop : (diracDomain B).topologicalClosure = ⊤ := + (Submodule.topologicalClosure_eq_top_iff (K := diracDomain B)).mpr horth + rw [dense_iff_closure_eq, ← Submodule.topologicalClosure_coe, htop, Submodule.top_coe] + +/-- The block-diagonal operator with symmetric blocks is contained in its adjoint. -/ +theorem diracDirac_le_adjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) : + diracDirac B ≤ (diracDirac B)† := + (diracDirac_isFormalAdjoint B hB).le_adjoint (dense_diracDomain B) + +/-- **The block-diagonal operator with symmetric blocks is self-adjoint.** The proof mirrors the +circle/torus self-adjointness arguments: symmetry gives `D ≤ D†`, and testing the adjoint +relation against each single-mode vector shows `D†.domain ⊆ diracDomain B`. -/ +theorem diracDirac_isSelfAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) : + IsSelfAdjoint (diracDirac B) := by + rw [LinearPMap.isSelfAdjoint_def] + have hfa : (diracDirac B)†.IsFormalAdjoint (diracDirac B) := + LinearPMap.adjoint_isFormalAdjoint (dense_diracDomain B) + have hdomle : (diracDirac B)†.domain ≤ diracDomain B := by + intro y hy + rw [mem_diracDomain_iff] + have hcoe : (fun i => B i (y i)) = ⇑((diracDirac B)† ⟨y, hy⟩) := by + funext i + refine (ext_inner_right 𝕜 fun v => ?_).symm + have key := hfa ⟨y, hy⟩ ⟨lp.single 2 i v, single_mem_diracDomain B i v⟩ + rw [lp.inner_single_right, diracDirac_single, lp.inner_single_right] at key + rw [key] + exact (hB i (y i) v).symm + rw [hcoe]; exact lp.memℓp _ + have heq : (diracDirac B).domain = (diracDirac B)†.domain := + le_antisymm (diracDirac_le_adjoint B hB).1 hdomle + exact (LinearPMap.eq_of_le_of_domain_eq (diracDirac_le_adjoint B hB) heq).symm + end lpDiag diff --git a/SpectralTriples/Examples/Circle.lean b/SpectralTriples/Examples/Circle.lean index 0fc633b..f0791f9 100644 --- a/SpectralTriples/Examples/Circle.lean +++ b/SpectralTriples/Examples/Circle.lean @@ -76,123 +76,41 @@ eigenvalue is the real number `n`. These are real (hence `D` is symmetric) and s `|n| → ∞` (hence `D` has compact resolvent). -/ def diracEigen : ℤ → ℝ := fun n => (n : ℝ) +/-- The scalar block at Fourier mode `n`: multiplication by the real eigenvalue `n`, as an +instance of the generic symmetric-block-diagonal machinery of `lpDiag`. -/ +noncomputable def diracBlock (n : ℤ) : ℂ →ₗ[ℂ] ℂ := (diracEigen n : ℂ) • LinearMap.id + +@[simp] theorem diracBlock_apply (n : ℤ) (v : ℂ) : + diracBlock n v = (diracEigen n : ℂ) * v := + smul_eq_mul _ _ + +/-- Each scalar block is symmetric, since its eigenvalue is real. -/ +theorem diracBlock_isSymmetric (n : ℤ) : (diracBlock n).IsSymmetric := by + intro x y + simp only [diracBlock_apply, RCLike.inner_apply, map_mul, Complex.conj_ofReal] + ring + /-- The maximal domain of the circle Dirac operator: the `H¹` Sobolev space `{ a ∈ ℓ²(ℤ) : Σ n² |aₙ|² < ∞ }`, i.e. those `a` for which `n ↦ n · aₙ` is again in `ℓ²(ℤ)`. This is the domain on which the diagonal Dirac operator `(D a)ₙ = n · aₙ` will be defined. -/ -def diracDomain : Submodule ℂ L2 where - carrier := {a | Memℓp (fun n => (diracEigen n : ℂ) * a n) 2} - zero_mem' := by - simp only [Set.mem_setOf_eq, lp.coeFn_zero, Pi.zero_apply, mul_zero] - exact zero_memℓp - add_mem' := by - intro a b ha hb - simp only [Set.mem_setOf_eq, lp.coeFn_add, Pi.add_apply, mul_add] at * - exact ha.add hb - smul_mem' := by - intro c a ha - simp only [Set.mem_setOf_eq, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul] at * - have hrw : (fun n => (diracEigen n : ℂ) * (c * a n)) - = c • fun n => (diracEigen n : ℂ) * a n := by - funext n; simp only [Pi.smul_apply, smul_eq_mul]; ring - rw [hrw]; exact ha.const_smul c +noncomputable def diracDomain : Submodule ℂ L2 := lpDiag.diracDomain diracBlock theorem mem_diracDomain_iff (a : L2) : - a ∈ diracDomain ↔ Memℓp (fun n => (diracEigen n : ℂ) * a n) 2 := Iff.rfl - -/-- Coordinatewise multiplication by the eigenvalue sequence `(n)`, as an element of `ℓ²(ℤ)`, -given a proof that the result is square-summable. -/ -def applyDirac (a : L2) (h : Memℓp (fun n => (diracEigen n : ℂ) * a n) 2) : L2 := - ⟨fun n => (diracEigen n : ℂ) * a n, h⟩ - -@[simp] theorem coe_applyDirac (a : L2) (h) (n : ℤ) : - (applyDirac a h) n = (diracEigen n : ℂ) * a n := rfl + a ∈ diracDomain ↔ Memℓp (fun n => (diracEigen n : ℂ) * a n) 2 := by + simp only [diracDomain, lpDiag.mem_diracDomain_iff, diracBlock_apply] /-- The circle Dirac operator `D = -i d/dθ` as an unbounded `LinearPMap`: diagonal on the Fourier basis, `(D a)ₙ = n · aₙ`, with domain the `H¹` Sobolev space `diracDomain`. -/ -noncomputable def diracDirac : L2 →ₗ.[ℂ] L2 where - domain := diracDomain - toFun := - { toFun := fun a => applyDirac (a : L2) ((mem_diracDomain_iff _).mp a.2) - map_add' := fun a b => by - ext n - simp only [coe_applyDirac, Submodule.coe_add, lp.coeFn_add, Pi.add_apply, mul_add] - map_smul' := fun c a => by - ext n - simp only [coe_applyDirac, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply, - smul_eq_mul, RingHom.id_apply, mul_left_comm] } +noncomputable def diracDirac : L2 →ₗ.[ℂ] L2 := lpDiag.diracDirac diracBlock @[simp] theorem diracDirac_apply (a : diracDomain) (n : ℤ) : - (diracDirac a) n = (diracEigen n : ℂ) * (a : L2) n := rfl + (diracDirac a) n = (diracEigen n : ℂ) * (a : L2) n := by + simp only [diracDirac, lpDiag.diracDirac_apply, diracBlock_apply] -/-- The circle Dirac operator is symmetric (formally self-adjoint): `⟪D x, y⟫ = ⟪x, D y⟫` -on its domain, because its eigenvalues are real. -/ -theorem diracDirac_isFormalAdjoint : diracDirac.IsFormalAdjoint diracDirac := by - intro x y - rw [lp.inner_eq_tsum, lp.inner_eq_tsum] - refine tsum_congr fun n => ?_ - simp only [diracDirac_apply, RCLike.inner_apply, map_mul, Complex.conj_ofReal] - ring - -/-- Each Fourier basis vector `eₙ = lp.single 2 n 1` lies in the `H¹` domain (it has finite -support, so `m ↦ m · (eₙ)ₘ = n · eₙ` is square-summable). -/ -theorem single_mem_diracDomain (n : ℤ) : (lp.single 2 n (1 : ℂ) : L2) ∈ diracDomain := by - rw [mem_diracDomain_iff] - have hfun : (fun m => (diracEigen m : ℂ) * (lp.single 2 n (1 : ℂ) : L2) m) - = (diracEigen n : ℂ) • (⇑(lp.single 2 n (1 : ℂ) : L2) : ℤ → ℂ) := by - funext m - rcases eq_or_ne m n with h | h - · subst h; simp [lp.single_apply] - · simp [lp.single_apply, h] - rw [hfun] - exact (lp.memℓp _).const_smul _ - -/-- The `H¹` domain is dense in `ℓ²(ℤ)`: it contains every Fourier basis vector, so its -orthogonal complement is trivial. -/ -theorem dense_diracDomain : Dense (diracDirac.domain : Set L2) := by - change Dense (diracDomain : Set L2) - have horth : (diracDomain : Submodule ℂ L2)ᗮ = ⊥ := by - rw [Submodule.eq_bot_iff] - intro y hy - refine lp.ext (funext fun n => ?_) - have h0 : inner ℂ (lp.single 2 n (1 : ℂ) : L2) y = 0 := hy _ (single_mem_diracDomain n) - rw [lp.inner_single_left] at h0 - simpa [RCLike.inner_apply, lp.coeFn_zero] using h0 - have htop : diracDomain.topologicalClosure = ⊤ := - (Submodule.topologicalClosure_eq_top_iff (K := diracDomain)).mpr horth - rw [dense_iff_closure_eq, ← Submodule.topologicalClosure_coe, htop, Submodule.top_coe] - -/-- The circle Dirac operator is contained in its adjoint (symmetry ⇒ `D ≤ D†`). -/ -theorem diracDirac_le_adjoint : diracDirac ≤ diracDirac† := - diracDirac_isFormalAdjoint.le_adjoint dense_diracDomain - -/-- **The circle Dirac operator is self-adjoint.** Since it is symmetric (so `D ≤ D†`), it -suffices that `D†.domain ⊆ D.domain`: for `y ∈ D†.domain`, testing the adjoint relation against -each Fourier basis vector `eₙ` gives `(D† y)ₙ = n · yₙ`, so `n ↦ n · yₙ` is square-summable and -`y` lies in the `H¹` domain. -/ -theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac := by - rw [isSelfAdjoint_def] - have hfa : diracDirac†.IsFormalAdjoint diracDirac := adjoint_isFormalAdjoint dense_diracDomain - have hdomle : diracDirac†.domain ≤ diracDomain := by - intro y hy - rw [mem_diracDomain_iff] - have hcoe : (fun n => (diracEigen n : ℂ) * y n) = ⇑(diracDirac† ⟨y, hy⟩) := by - funext n - have key := hfa ⟨y, hy⟩ ⟨lp.single 2 n (1 : ℂ), single_mem_diracDomain n⟩ - have hDe : diracDirac ⟨lp.single 2 n (1 : ℂ), single_mem_diracDomain n⟩ - = (diracEigen n : ℂ) • (lp.single 2 n (1 : ℂ) : L2) := by - refine lp.ext (funext fun m => ?_) - simp only [diracDirac_apply, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul] - rcases eq_or_ne m n with h | h - · subst h; rfl - · simp [lp.single_apply, h] - rw [lp.inner_single_right, hDe, inner_smul_right, lp.inner_single_right] at key - have key2 := congrArg (starRingEnd ℂ) key - simp [RCLike.inner_apply, map_mul, Complex.conj_ofReal] at key2 - exact key2.symm - rw [hcoe]; exact lp.memℓp _ - have heq : diracDirac.domain = diracDirac†.domain := - le_antisymm diracDirac_le_adjoint.1 hdomle - exact (LinearPMap.eq_of_le_of_domain_eq diracDirac_le_adjoint heq).symm +/-- **The circle Dirac operator is self-adjoint.** An instance of the generic +`lpDiag.diracDirac_isSelfAdjoint` for symmetric block families. -/ +theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac := + lpDiag.diracDirac_isSelfAdjoint diracBlock diracBlock_isSymmetric /-- `i` lies in the resolvent set of the circle Dirac operator: it is self-adjoint and `Im i = 1 ≠ 0`, so the basic criterion applies. -/ diff --git a/SpectralTriples/Examples/Torus.lean b/SpectralTriples/Examples/Torus.lean index d0c523d..f917016 100644 --- a/SpectralTriples/Examples/Torus.lean +++ b/SpectralTriples/Examples/Torus.lean @@ -98,52 +98,6 @@ noncomputable def diracBlock (p : ℤ × ℤ) : Spinor →ₗ[ℂ] Spinor := !![0, (p.1 : ℂ) - (p.2 : ℂ) * Complex.I; (p.1 : ℂ) + (p.2 : ℂ) * Complex.I, 0] -/-- The maximal domain of the torus Dirac operator: the `H¹` Sobolev space, those `a` for which -`p ↦ D₍ₚ₎ (aₚ)` is again square-summable (equivalently `Σ (m²+n²) ‖aₚ‖² < ∞`). -/ -def diracDomain : Submodule ℂ H where - carrier := {a | Memℓp (fun p => diracBlock p (a p)) 2} - zero_mem' := by - have : (fun p => diracBlock p ((0 : H) p)) = 0 := by - funext p; simp only [lp.coeFn_zero, Pi.zero_apply, _root_.map_zero] - simp only [Set.mem_setOf_eq, this]; exact zero_memℓp - add_mem' := fun {a b} ha hb => by - have heq : (fun p => diracBlock p ((a + b) p)) - = (fun p => diracBlock p (a p)) + fun p => diracBlock p (b p) := by - funext p; simp only [lp.coeFn_add, Pi.add_apply, _root_.map_add] - rw [Set.mem_setOf_eq, heq]; exact ha.add hb - smul_mem' := fun c a ha => by - have heq : (fun p => diracBlock p ((c • a) p)) = c • fun p => diracBlock p (a p) := by - funext p; simp only [lp.coeFn_smul, Pi.smul_apply, _root_.map_smul] - rw [Set.mem_setOf_eq, heq]; exact ha.const_smul c - -theorem mem_diracDomain_iff (a : H) : - a ∈ diracDomain ↔ Memℓp (fun p => diracBlock p (a p)) 2 := Iff.rfl - -/-- Coordinatewise application of the Dirac blocks, as an element of `ℓ²(ℤ²; ℂ²)`, given a -proof that the result is square-summable. -/ -noncomputable def applyDirac (a : H) (h : Memℓp (fun p => diracBlock p (a p)) 2) : H := - ⟨fun p => diracBlock p (a p), h⟩ - -@[simp] theorem coe_applyDirac (a : H) (h) (p : ℤ × ℤ) : - (applyDirac a h) p = diracBlock p (a p) := rfl - -/-- The torus Dirac operator as an unbounded `LinearPMap`: block-diagonal on the Fourier -lattice, `(D a)₍ₘ,ₙ₎ = D₍ₘ,ₙ₎ (a₍ₘ,ₙ₎)`, with domain the `H¹` Sobolev space `diracDomain`. -/ -noncomputable def diracDirac : H →ₗ.[ℂ] H where - domain := diracDomain - toFun := - { toFun := fun a => applyDirac (a : H) ((mem_diracDomain_iff _).mp a.2) - map_add' := fun a b => by - refine lp.ext (funext fun p => ?_) - simp only [coe_applyDirac, Submodule.coe_add, lp.coeFn_add, Pi.add_apply, _root_.map_add] - map_smul' := fun c a => by - refine lp.ext (funext fun p => ?_) - simp only [coe_applyDirac, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply, - _root_.map_smul, RingHom.id_apply] } - -@[simp] theorem diracDirac_apply (a : diracDomain) (p : ℤ × ℤ) : - (diracDirac a) p = diracBlock p ((a : H) p) := rfl - /-- Each Dirac block is self-adjoint on the spinor fibre: the matrix `2π·!![0, m-in; m+in, 0]` is Hermitian. -/ theorem diracBlock_isSymmetric (p : ℤ × ℤ) : (diracBlock p).IsSymmetric := by @@ -152,80 +106,27 @@ theorem diracBlock_isSymmetric (p : ℤ × ℤ) : (diracBlock p).IsSymmetric := fin_cases i <;> fin_cases j <;> simp [Matrix.conjTranspose_apply, Matrix.smul_apply, Complex.conj_ofReal, sub_eq_add_neg] -/-- The torus Dirac operator is symmetric (formally self-adjoint): `⟪D a, b⟫ = ⟪a, D b⟫` on its -domain, because each spinor block is self-adjoint. -/ -theorem diracDirac_isFormalAdjoint : diracDirac.IsFormalAdjoint diracDirac := by - intro a b - rw [lp.inner_eq_tsum, lp.inner_eq_tsum] - refine tsum_congr fun p => ?_ - rw [diracDirac_apply, diracDirac_apply] - exact diracBlock_isSymmetric p _ _ - -/-- Each `lp.single (m, n) v` (a single spinor in one Fourier mode) lies in the `H¹` domain: it -has finite support, so `q ↦ D₍q₎ (single₍q₎)` is supported on `{(m, n)}` and square-summable. -/ -theorem single_mem_diracDomain (p : ℤ × ℤ) (v : Spinor) : - (lp.single 2 p v : H) ∈ diracDomain := by - rw [mem_diracDomain_iff] - have hfun : (fun q => diracBlock q ((lp.single 2 p v : H) q)) - = ⇑(lp.single 2 p (diracBlock p v) : H) := by - funext q - rcases eq_or_ne q p with h | h - · subst h; simp [lp.single_apply] - · simp [lp.single_apply, h, _root_.map_zero] - rw [hfun] - exact lp.memℓp _ +/-- The maximal domain of the torus Dirac operator: the `H¹` Sobolev space, those `a` for which +`p ↦ D₍ₚ₎ (aₚ)` is again square-summable (equivalently `Σ (m²+n²) ‖aₚ‖² < ∞`). An instance of +the generic symmetric-block-diagonal machinery of `lpDiag`. -/ +noncomputable def diracDomain : Submodule ℂ H := lpDiag.diracDomain diracBlock -/-- The image `D (single (m, n) v) = single (m, n) (D₍ₘ,ₙ₎ v)`: the block-diagonal operator acts -on a single-mode vector by its block in that mode. -/ -theorem diracDirac_single (p : ℤ × ℤ) (v : Spinor) : - diracDirac ⟨lp.single 2 p v, single_mem_diracDomain p v⟩ - = (lp.single 2 p (diracBlock p v) : H) := by - refine lp.ext (funext fun q => ?_) - rcases eq_or_ne q p with h | h - · subst h; simp [diracDirac_apply, lp.single_apply] - · simp [diracDirac_apply, lp.single_apply, h, _root_.map_zero] - -/-- The `H¹` domain is dense in `ℓ²(ℤ²; ℂ²)`: it contains every single-mode spinor, so its -orthogonal complement is trivial. -/ -theorem dense_diracDomain : Dense (diracDirac.domain : Set H) := by - change Dense (diracDomain : Set H) - have horth : (diracDomain : Submodule ℂ H)ᗮ = ⊥ := by - rw [Submodule.eq_bot_iff] - intro y hy - refine lp.ext (funext fun p => ?_) - refine ext_inner_left ℂ fun v => ?_ - have h0 : inner ℂ (lp.single 2 p v : H) y = 0 := hy _ (single_mem_diracDomain p v) - rw [lp.inner_single_left] at h0 - rw [h0, lp.coeFn_zero, Pi.zero_apply, inner_zero_right] - have htop : diracDomain.topologicalClosure = ⊤ := - (Submodule.topologicalClosure_eq_top_iff (K := diracDomain)).mpr horth - rw [dense_iff_closure_eq, ← Submodule.topologicalClosure_coe, htop, Submodule.top_coe] - -/-- The torus Dirac operator is contained in its adjoint (symmetry ⇒ `D ≤ D†`). -/ -theorem diracDirac_le_adjoint : diracDirac ≤ diracDirac† := - diracDirac_isFormalAdjoint.le_adjoint dense_diracDomain - -/-- **The torus Dirac operator is self-adjoint.** It is symmetric (so `D ≤ D†`); it remains to -show `D†.domain ⊆ D.domain`. For `y ∈ D†.domain`, testing the adjoint relation against each -single-mode spinor `single (m, n) v` and using self-adjointness of the block gives -`(D† y)₍ₘ,ₙ₎ = D₍ₘ,ₙ₎ (y₍ₘ,ₙ₎)`, so `q ↦ D₍q₎ (y₍q₎)` is square-summable and `y ∈ H¹`. -/ -theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac := by - rw [isSelfAdjoint_def] - have hfa : diracDirac†.IsFormalAdjoint diracDirac := adjoint_isFormalAdjoint dense_diracDomain - have hdomle : diracDirac†.domain ≤ diracDomain := by - intro y hy - rw [mem_diracDomain_iff] - have hcoe : (fun p => diracBlock p (y p)) = ⇑(diracDirac† ⟨y, hy⟩) := by - funext p - refine (ext_inner_right ℂ fun v => ?_).symm - have key := hfa ⟨y, hy⟩ ⟨lp.single 2 p v, single_mem_diracDomain p v⟩ - rw [lp.inner_single_right, diracDirac_single, lp.inner_single_right] at key - rw [key] - exact (diracBlock_isSymmetric p (y p) v).symm - rw [hcoe]; exact lp.memℓp _ - have heq : diracDirac.domain = diracDirac†.domain := - le_antisymm diracDirac_le_adjoint.1 hdomle - exact (LinearPMap.eq_of_le_of_domain_eq diracDirac_le_adjoint heq).symm +theorem mem_diracDomain_iff (a : H) : + a ∈ diracDomain ↔ Memℓp (fun p => diracBlock p (a p)) 2 := + lpDiag.mem_diracDomain_iff diracBlock a + +/-- The torus Dirac operator as an unbounded `LinearPMap`: block-diagonal on the Fourier +lattice, `(D a)₍ₘ,ₙ₎ = D₍ₘ,ₙ₎ (a₍ₘ,ₙ₎)`, with domain the `H¹` Sobolev space `diracDomain`. -/ +noncomputable def diracDirac : H →ₗ.[ℂ] H := lpDiag.diracDirac diracBlock + +@[simp] theorem diracDirac_apply (a : diracDomain) (p : ℤ × ℤ) : + (diracDirac a) p = diracBlock p ((a : H) p) := + lpDiag.diracDirac_apply diracBlock a p + +/-- **The torus Dirac operator is self-adjoint.** An instance of the generic +`lpDiag.diracDirac_isSelfAdjoint` for symmetric block families. -/ +theorem diracDirac_isSelfAdjoint : IsSelfAdjoint diracDirac := + lpDiag.diracDirac_isSelfAdjoint diracBlock diracBlock_isSymmetric /-- `i` lies in the resolvent set of the torus Dirac operator: it is self-adjoint and `Im i = 1 ≠ 0`, so the basic criterion applies. -/ From 153854fc79bb4c6c643d0a56adcde1407199a119 Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 14:13:49 -0400 Subject: [PATCH 4/8] Scope [DecidableEq alpha] to only where lp.single needs it It was declared at the top of the whole lpDiag.diracDirac section, so every earlier lemma (diracDomain, diracDirac_apply, diracDirac_isFormalAdjoint, etc., none of which touch lp.single) picked it up as an unused hypothesis. Move it down to right before single_mem_diracDomain, where it's first actually needed, and add the now-possible omit clauses for CompleteSpace on lemmas that don't need adjoint/density machinery either. Co-Authored-By: Claude Sonnet 4.6 --- SpectralTriples/DiagonalOperator.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/SpectralTriples/DiagonalOperator.lean b/SpectralTriples/DiagonalOperator.lean index 5d05abd..23fd6ea 100644 --- a/SpectralTriples/DiagonalOperator.lean +++ b/SpectralTriples/DiagonalOperator.lean @@ -226,7 +226,7 @@ it is self-adjoint. This is the analytic core shared by the `S¹` and `T²` Dira circle's scalar multiplication by `n` and the torus's `2×2` spinor blocks are both instances of a symmetric block family, differing only in the fibre `G i` and the block `B i`. -/ -variable [∀ i, CompleteSpace (G i)] [DecidableEq α] +variable [∀ i, CompleteSpace (G i)] /-- The maximal domain of the unbounded block-diagonal operator with blocks `B`: those `a` for which `i ↦ B i (aᵢ)` is again square-summable. -/ @@ -245,7 +245,7 @@ def diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) : Submodule 𝕜 (lp G 2) wher funext i; simp only [lp.coeFn_smul, Pi.smul_apply, _root_.map_smul] rw [Set.mem_setOf_eq, heq]; exact ha.const_smul c -omit [∀ i, CompleteSpace (G i)] [DecidableEq α] in +omit [∀ i, CompleteSpace (G i)] in theorem mem_diracDomain_iff (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) : a ∈ diracDomain B ↔ Memℓp (fun i => B i (a i)) 2 := Iff.rfl @@ -255,7 +255,7 @@ noncomputable def applyDirac (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) (h : Memℓp (fun i => B i (a i)) 2) : lp G 2 := ⟨fun i => B i (a i), h⟩ -omit [∀ i, CompleteSpace (G i)] [DecidableEq α] in +omit [∀ i, CompleteSpace (G i)] in @[simp] theorem coe_applyDirac (B : ∀ i, G i →ₗ[𝕜] G i) (a : lp G 2) (h) (i : α) : (applyDirac B a h) i = B i (a i) := rfl @@ -274,9 +274,11 @@ noncomputable def diracDirac (B : ∀ i, G i →ₗ[𝕜] G i) : lp G 2 →ₗ.[ simp only [coe_applyDirac, Submodule.coe_smul, lp.coeFn_smul, Pi.smul_apply, _root_.map_smul, RingHom.id_apply] } +omit [∀ i, CompleteSpace (G i)] in @[simp] theorem diracDirac_apply (B : ∀ i, G i →ₗ[𝕜] G i) (a : diracDomain B) (i : α) : (diracDirac B a) i = B i ((a : lp G 2) i) := rfl +omit [∀ i, CompleteSpace (G i)] in /-- The block-diagonal operator is symmetric (formally self-adjoint) when each block is. -/ theorem diracDirac_isFormalAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) : (diracDirac B).IsFormalAdjoint (diracDirac B) := by @@ -286,6 +288,9 @@ theorem diracDirac_isFormalAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i rw [diracDirac_apply, diracDirac_apply] exact hB i _ _ +variable [DecidableEq α] + +omit [∀ i, CompleteSpace (G i)] in /-- Each single-mode vector lies in the maximal domain. -/ theorem single_mem_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : (lp.single 2 i v : lp G 2) ∈ diracDomain B := by @@ -299,6 +304,7 @@ theorem single_mem_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G rw [hfun] exact lp.memℓp _ +omit [∀ i, CompleteSpace (G i)] in /-- The image of a single-mode vector under the diagonal operator. -/ theorem diracDirac_single (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : diracDirac B ⟨lp.single 2 i v, single_mem_diracDomain B i v⟩ From 8c60310ceac7e2b586d94d4d94ad6e5a42a2a698 Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 14:18:53 -0400 Subject: [PATCH 5/8] Eliminate the DecidableEq lint warnings properly open scoped Classical (my previous fix) is itself flagged by the project's own style linter: it silently fills in decidability for every declaration that follows, which can hide statements that would be better off explicit. The linter's own suggestion is the right fix: declarations whose *statement* mentions lp.single (single_mem_diracDomain, diracDirac_single) take [DecidableEq alpha] as an explicit hypothesis; declarations that only need it inside their *proof* (dense_diracDomain, diracDirac_isSelfAdjoint) use the `classical` tactic instead, so the hypothesis never leaks into their type. diracDirac_le_adjoint needed neither, once decidability isn't pulled in via a blanket `variable`. No remaining linter warnings in the file; axiom report unchanged (Classical. choice was already a dependency everywhere in this development). Co-Authored-By: Claude Sonnet 4.6 --- SpectralTriples/DiagonalOperator.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/SpectralTriples/DiagonalOperator.lean b/SpectralTriples/DiagonalOperator.lean index 23fd6ea..9b44c68 100644 --- a/SpectralTriples/DiagonalOperator.lean +++ b/SpectralTriples/DiagonalOperator.lean @@ -288,11 +288,9 @@ theorem diracDirac_isFormalAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i rw [diracDirac_apply, diracDirac_apply] exact hB i _ _ -variable [DecidableEq α] - omit [∀ i, CompleteSpace (G i)] in /-- Each single-mode vector lies in the maximal domain. -/ -theorem single_mem_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : +theorem single_mem_diracDomain [DecidableEq α] (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : (lp.single 2 i v : lp G 2) ∈ diracDomain B := by rw [mem_diracDomain_iff] have hfun : (fun q => B q ((lp.single 2 i v : lp G 2) q)) @@ -306,7 +304,7 @@ theorem single_mem_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G omit [∀ i, CompleteSpace (G i)] in /-- The image of a single-mode vector under the diagonal operator. -/ -theorem diracDirac_single (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : +theorem diracDirac_single [DecidableEq α] (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : diracDirac B ⟨lp.single 2 i v, single_mem_diracDomain B i v⟩ = (lp.single 2 i (B i v) : lp G 2) := by refine lp.ext (funext fun q => ?_) @@ -317,6 +315,7 @@ theorem diracDirac_single (B : ∀ i, G i →ₗ[𝕜] G i) (i : α) (v : G i) : /-- The maximal domain is dense: it contains every single-mode vector. -/ theorem dense_diracDomain (B : ∀ i, G i →ₗ[𝕜] G i) : Dense ((diracDirac B).domain : Set (lp G 2)) := by + classical change Dense (diracDomain B : Set (lp G 2)) have horth : (diracDomain B : Submodule 𝕜 (lp G 2))ᗮ = ⊥ := by rw [Submodule.eq_bot_iff] @@ -340,6 +339,7 @@ circle/torus self-adjointness arguments: symmetry gives `D ≤ D†`, and testin relation against each single-mode vector shows `D†.domain ⊆ diracDomain B`. -/ theorem diracDirac_isSelfAdjoint (B : ∀ i, G i →ₗ[𝕜] G i) (hB : ∀ i, (B i).IsSymmetric) : IsSelfAdjoint (diracDirac B) := by + classical rw [LinearPMap.isSelfAdjoint_def] have hfa : (diracDirac B)†.IsFormalAdjoint (diracDirac B) := LinearPMap.adjoint_isFormalAdjoint (dense_diracDomain B) From 4b043565d5ee70345dd1438b3b7e7e0f510a318d Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 19:39:40 -0400 Subject: [PATCH 6/8] Fix stale file:line references in FAITHFULNESS.md and add the new shared lemma The Torus.lean domain/self-adjointness refactor shifted every later declaration by ~98 lines; the new import in DiagonalOperator.lean shifted diagL/norm_diagL_le/ isCompactOperator_diagL by 1. Also adds a row for the new shared lpDiag.diracDirac_isSelfAdjoint lemma that Circle.lean and Torus.lean now both instantiate. Co-Authored-By: Claude Sonnet 4.6 --- audit/FAITHFULNESS.md | 35 ++++++++++++++++++----------------- 1 file changed, 18 insertions(+), 17 deletions(-) diff --git a/audit/FAITHFULNESS.md b/audit/FAITHFULNESS.md index 7fb7248..7186f72 100644 --- a/audit/FAITHFULNESS.md +++ b/audit/FAITHFULNESS.md @@ -64,9 +64,10 @@ representation `π : A →⋆ₐ[𝕜] (H →L[𝕜] H)`. | Object / Claim | Informal content | Lean | Status | |---|---|---|---| -| Block-diagonal operator on `ℓ²` | `(diagL T) a = (i ↦ Tᵢ aᵢ)` for a uniformly bounded block family | `lpDiag.diagL` — `DiagonalOperator.lean:69` | ✓ axiom-clean | -| its operator-norm bound | `‖diagL T‖ ≤ C` when `‖Tᵢ‖ ≤ C` | `lpDiag.norm_diagL_le` — `DiagonalOperator.lean:97` | ✓ axiom-clean | -| **compactness criterion** | block norms `→ 0` (cofinite) + finite-dim fibres ⇒ `diagL T` compact (finite-rank truncations converge in operator norm) | `lpDiag.isCompactOperator_diagL` — `DiagonalOperator.lean:185` | ✓ axiom-clean | +| Block-diagonal operator on `ℓ²` | `(diagL T) a = (i ↦ Tᵢ aᵢ)` for a uniformly bounded block family | `lpDiag.diagL` — `DiagonalOperator.lean:70` | ✓ axiom-clean | +| its operator-norm bound | `‖diagL T‖ ≤ C` when `‖Tᵢ‖ ≤ C` | `lpDiag.norm_diagL_le` — `DiagonalOperator.lean:98` | ✓ axiom-clean | +| **compactness criterion** | block norms `→ 0` (cofinite) + finite-dim fibres ⇒ `diagL T` compact (finite-rank truncations converge in operator norm) | `lpDiag.isCompactOperator_diagL` — `DiagonalOperator.lean:186` | ✓ axiom-clean | +| **unbounded block-diagonal Dirac operator** | given symmetric blocks `B i`, the operator on its maximal `ℓ²` domain is self-adjoint (shared by the `S¹`/`T²` examples below) | `lpDiag.diracDirac_isSelfAdjoint` — `DiagonalOperator.lean:340` | ✓ axiom-clean | ## Index of an even spectral triple (Phase 2 foundations) @@ -97,20 +98,20 @@ Reference: Connes Ch. VI; GBF §9–12 (canonical triple of a spin manifold, her | Object / Claim | Lean | Status | |---|---|---| -| Dirac operator `D` (block-diagonal, unbounded) | `SpectralTriples.Torus.diracDirac` — `Examples/Torus.lean:131` | ✓ axiom-clean | -| `D` self-adjoint | `SpectralTriples.Torus.diracDirac_isSelfAdjoint` — `Examples/Torus.lean:211` | ✓ axiom-clean | -| `i ∈ ρ(D)` | `SpectralTriples.Torus.mem_resolventSet_I` — `Examples/Torus.lean:231` | ✓ axiom-clean | -| `(D − i·1)⁻¹` is compact | `SpectralTriples.Torus.isCompactOperator_resolvent_I` — `Examples/Torus.lean:509` | ✓ axiom-clean | -| grading `γ = σ₃` (CLM) | `SpectralTriples.Torus.grading` — `Examples/Torus.lean:592` | ✓ axiom-clean | -| `γ` self-adjoint | `SpectralTriples.Torus.isSelfAdjoint_grading` — `Examples/Torus.lean:608` | ✓ axiom-clean | -| `γ² = 1` | `SpectralTriples.Torus.grading_mul_self` — `Examples/Torus.lean:612` | ✓ axiom-clean | -| `D γ = −γ D` on `dom D` | `SpectralTriples.Torus.grading_anticomm` — `Examples/Torus.lean:631` | ✓ axiom-clean | -| algebra `ℂ[ℤ²]` (shift `*`-subalgebra) | `SpectralTriples.Torus.algebra` — `Examples/Torus.lean:871` | ✓ axiom-clean | -| representation (inclusion `StarAlgHom`) | `SpectralTriples.Torus.rep` — `Examples/Torus.lean:876` | ✓ axiom-clean | -| **`(A, H, D)` is an odd spectral triple** | `SpectralTriples.Torus.isOddSpectralTriple` — `Examples/Torus.lean:931` | ✓ axiom-clean | -| **`(A, H, D, γ)` is an even spectral triple** | `SpectralTriples.Torus.isEvenSpectralTriple` — `Examples/Torus.lean:984` | ✓ axiom-clean | -| **finitely summable at `i`** | `SpectralTriples.Torus.isFinitelySummableSpectralTriple` — `Examples/Torus.lean:994` | ✓ axiom-clean | -| **index `= 0`** (`Â(T²)·rk`; `ker D = ℂ²` at the zero mode, split `1+1` by `γ`) | `SpectralTriples.Torus.index_eq_zero` — `Examples/Torus.lean:1257` | ✓ axiom-clean | +| Dirac operator `D` (block-diagonal, unbounded) | `SpectralTriples.Torus.diracDirac` — `Examples/Torus.lean:120` | ✓ axiom-clean | +| `D` self-adjoint | `SpectralTriples.Torus.diracDirac_isSelfAdjoint` — `Examples/Torus.lean:128` | ✓ axiom-clean | +| `i ∈ ρ(D)` | `SpectralTriples.Torus.mem_resolventSet_I` — `Examples/Torus.lean:133` | ✓ axiom-clean | +| `(D − i·1)⁻¹` is compact | `SpectralTriples.Torus.isCompactOperator_resolvent_I` — `Examples/Torus.lean:411` | ✓ axiom-clean | +| grading `γ = σ₃` (CLM) | `SpectralTriples.Torus.grading` — `Examples/Torus.lean:494` | ✓ axiom-clean | +| `γ` self-adjoint | `SpectralTriples.Torus.isSelfAdjoint_grading` — `Examples/Torus.lean:510` | ✓ axiom-clean | +| `γ² = 1` | `SpectralTriples.Torus.grading_mul_self` — `Examples/Torus.lean:514` | ✓ axiom-clean | +| `D γ = −γ D` on `dom D` | `SpectralTriples.Torus.grading_anticomm` — `Examples/Torus.lean:533` | ✓ axiom-clean | +| algebra `ℂ[ℤ²]` (shift `*`-subalgebra) | `SpectralTriples.Torus.algebra` — `Examples/Torus.lean:773` | ✓ axiom-clean | +| representation (inclusion `StarAlgHom`) | `SpectralTriples.Torus.rep` — `Examples/Torus.lean:778` | ✓ axiom-clean | +| **`(A, H, D)` is an odd spectral triple** | `SpectralTriples.Torus.isOddSpectralTriple` — `Examples/Torus.lean:833` | ✓ axiom-clean | +| **`(A, H, D, γ)` is an even spectral triple** | `SpectralTriples.Torus.isEvenSpectralTriple` — `Examples/Torus.lean:886` | ✓ axiom-clean | +| **finitely summable at `i`** | `SpectralTriples.Torus.isFinitelySummableSpectralTriple` — `Examples/Torus.lean:896` | ✓ axiom-clean | +| **index `= 0`** (`Â(T²)·rk`; `ker D = ℂ²` at the zero mode, split `1+1` by `γ`) | `SpectralTriples.Torus.index_eq_zero` — `Examples/Torus.lean:1158` | ✓ axiom-clean | *Faithfulness note for the example.* The chosen algebra is the trigonometric polynomials `ℂ[ℤ²]` (Fourier dual of `C(T²)`), represented by the coordinate shift unitaries — the From 9d0ad7e12f04346c38a51372a2c10bd148f95eb4 Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 19:42:07 -0400 Subject: [PATCH 7/8] Stop overclaiming the full Riesz-Schauder theorem for compact perturbations The file/section-level summaries said this proves "the Hilbert-space case of the classical Riesz-Schauder theorem," but the classical theorem's conclusion includes index 0, which isFredholm_one_sub explicitly does not prove (its own docstring already says so). Reword the summaries to match: only the structural Fredholm-ness part (finite kernel, closed range, finite codimension) is proved. Co-Authored-By: Claude Sonnet 4.6 --- SpectralTriples/CompactOperators.lean | 7 ++++--- blueprint/src/content.tex | 10 ++++++---- 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/SpectralTriples/CompactOperators.lean b/SpectralTriples/CompactOperators.lean index 2f2fbb5..9ba5ab3 100644 --- a/SpectralTriples/CompactOperators.lean +++ b/SpectralTriples/CompactOperators.lean @@ -16,9 +16,10 @@ public import Mathlib.Analysis.InnerProductSpace.Spectrum This file proves, for an inner product space `H`, that `1 - K` is a Fredholm linear map (`SpectralTriples.Fredholm.IsFredholm`) whenever `K` is a compact operator on `H`. This is the -Hilbert-space case of the classical Riesz–Schauder theorem; it is not yet in Mathlib (only the -weaker spectral dichotomy `IsCompactOperator.hasEigenvalue_or_mem_resolventSet` is), so we prove -it here from scratch. +structural part of the Hilbert-space case of the classical Riesz–Schauder theorem (finite +kernel, closed range, finite-dimensional cokernel); the further classical fact that the index +is `0` is not proved here. None of this is yet in Mathlib (only the weaker spectral dichotomy +`IsCompactOperator.hasEigenvalue_or_mem_resolventSet` is), so we prove it here from scratch. ## Main results diff --git a/blueprint/src/content.tex b/blueprint/src/content.tex index 4b72f19..1968694 100644 --- a/blueprint/src/content.tex +++ b/blueprint/src/content.tex @@ -217,10 +217,12 @@ \section{Fredholm operators} \subsection{Compact perturbations of the identity} \label{subsec:compact-perturbations} -This subsection proves the Hilbert-space case of the classical Riesz--Schauder theorem: -$1 - K$ is Fredholm whenever $K$ is compact. None of this is yet in Mathlib (only the weaker -spectral dichotomy for compact operators is), so it is built here from scratch, as the -analytic ingredient needed to eventually show the chiral Dirac operator $D^{+}$ is Fredholm. +This subsection proves the structural part of the Hilbert-space case of the classical +Riesz--Schauder theorem: $1 - K$ is Fredholm whenever $K$ is compact (finite kernel, closed +range, finite-dimensional cokernel). The further classical fact that the index is $0$ is not +proved here. None of this is yet in Mathlib (only the weaker spectral dichotomy for compact +operators is), so it is built here from scratch, as the analytic ingredient needed to +eventually show the chiral Dirac operator $D^{+}$ is Fredholm. \begin{theorem}[Compact operators are approximable by finite rank] \label{thm:exists-finiteRank-norm-sub-lt} From 8edaea5b37532f4457d0b7d7ec5c7789c707a322 Mon Sep 17 00:00:00 2001 From: Jon Bannon Date: Sat, 20 Jun 2026 19:43:10 -0400 Subject: [PATCH 8/8] Fix missing "and" between author names in the blueprint \and rendered fine in the PDF but plastex's web template dropped the word entirely, showing "Jon Bannon Michael R. Douglas". Spell it out literally so both renderers agree. Co-Authored-By: Claude Sonnet 4.6 --- blueprint/src/print.tex | 2 +- blueprint/src/web.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/blueprint/src/print.tex b/blueprint/src/print.tex index b9a1c18..e60d4ff 100644 --- a/blueprint/src/print.tex +++ b/blueprint/src/print.tex @@ -25,7 +25,7 @@ \input{macros/print} \title{Spectral Triples and the Index Pairing} -\author{Jon Bannon \and Michael R. Douglas} +\author{Jon Bannon and Michael R. Douglas} \begin{document} \maketitle diff --git a/blueprint/src/web.tex b/blueprint/src/web.tex index c64e36b..1344ddc 100644 --- a/blueprint/src/web.tex +++ b/blueprint/src/web.tex @@ -19,7 +19,7 @@ \dochome{https://JonBannon.github.io/SpectralTriples/docs} \title{Spectral Triples and the Index Pairing} -\author{Jon Bannon \and Michael R. Douglas} +\author{Jon Bannon and Michael R. Douglas} \begin{document} \maketitle