Self-adjoint Fredholm operators

This file proves that a self-adjoint Fredholm operator on a Hilbert space has index zero. More generally, the same conclusion holds whenever an operator and its adjoint have the same kernel. The closed range of a Fredholm operator has orthogonal complement equal to the kernel of its adjoint. Orthogonal decomposition therefore identifies the cokernel with that kernel; under the kernel-equality hypothesis, it identifies the cokernel with the original kernel.

Main declarations

• ContinuousLinearMap.IsFredholm.cokerEquivKerOfKerAdjointEq: identify the cokernel with the kernel when the operator and its adjoint have equal kernels.
• ContinuousLinearMap.index_eq_zero_of_ker_adjoint_eq: the corresponding index-zero criterion.
• ContinuousLinearMap.index_eq_zero_of_isSelfAdjoint: a self-adjoint Fredholm operator has index zero.
• ContinuousLinearMap.index_eq_zero_of_isSymmetric: the same result in terms of symmetry of the underlying linear map.

This is the elementary self-adjoint index computation in the Fredholm package needed by the nonlinear-analysis substrate of the analytic Heegaard Floer roadmap. The convention and argument follow McDuff--Salamon, J-holomorphic Curves and Symplectic Topology, Appendix A.1.

noncomputable def ContinuousLinearMap.IsFredholm.cokerEquivKerOfKerAdjointEq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsFredholm) (hker : (↑(ContinuousLinearMap.adjoint T)).ker = (↑T).ker) : (E ⧸ (↑T).range) ≃ₗ[𝕜] ↥(↑T).ker

The cokernel of a Fredholm operator is linearly equivalent to its kernel if the operator and its adjoint have the same kernel.

Equations

• hT.cokerEquivKerOfKerAdjointEq hker = (↑(T.cokerEquivKerAdjoint ⋯)).trans (LinearEquiv.ofEq (↑(ContinuousLinearMap.adjoint T)).ker (↑T).ker hker)

noncomputable def ContinuousLinearMap.IsFredholm.cokerEquivKer {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsFredholm) (hself : IsSelfAdjoint T) : (E ⧸ (↑T).range) ≃ₗ[𝕜] ↥(↑T).ker

The cokernel of a self-adjoint Fredholm operator is linearly equivalent to its kernel.

Equations

• hT.cokerEquivKer hself = hT.cokerEquivKerOfKerAdjointEq ⋯

theorem ContinuousLinearMap.index_eq_zero_of_ker_adjoint_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsFredholm) (hker : (↑(adjoint T)).ker = (↑T).ker) : T.index = 0

A Fredholm operator has index zero if it and its adjoint have the same kernel.

@[simp]

theorem ContinuousLinearMap.index_eq_zero_of_isSelfAdjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsFredholm) (hself : IsSelfAdjoint T) : T.index = 0

A self-adjoint Fredholm operator on a Hilbert space has Fredholm index zero.

@[simp]

theorem ContinuousLinearMap.index_eq_zero_of_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : T.IsFredholm) (hsymm : (↑T).IsSymmetric) : T.index = 0

A symmetric Fredholm operator on a Hilbert space has Fredholm index zero.