Deduplicate redundant proofs: closed-range cokernel argument and diagonal-operator self-adjointness

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
 
@@ -185,6 +186,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 +371,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

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,144 @@ 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)]
+
+/-- 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)] 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)] 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] }
+
+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
+  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 _ _
+
+omit [∀ i, CompleteSpace (G i)] in
+/-- Each single-mode vector lies in the maximal domain. -/
+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))
+      = ⇑(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 _
+
+omit [∀ i, CompleteSpace (G i)] in
+/-- The image of a single-mode vector under the diagonal operator. -/
+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 => ?_)
+  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
+  classical
+  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
+  classical
+  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

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. -/