Kernels and ranges of adjoints, and the closed-range theorem

The adjoint of a continuous linear map T : E →L[𝕜] F between topological modules over a normed field is precomposition ContinuousLinearMap.precomp 𝕜 T : StrongDual 𝕜 F →L[𝕜] StrongDual 𝕜 E. Annihilators are Mathlib's Submodule.orthogonalBilin for the canonical pairing topDualPairing: for S ≤ E, S.orthogonalBilin (topDualPairing 𝕜 E).flip is the annihilator of S in the dual, and for G ≤ StrongDual 𝕜 E, G.orthogonalBilin (topDualPairing 𝕜 E) is the preannihilator of G in E.

This file proves the unconditional identities ker T* = (range T)ᗮ, range T* ≤ (ker T)ᗮ and, when functionals separate points of F, ker T = (range T*)_⊥. For a bounded operator between Banach spaces it then proves the closed-range theorem: range T is closed iff range T* is closed, in which case range T* = (ker T)ᗮ. It also proves that a bounded map between Banach spaces is bijective iff its transpose is.

The reverse implication only needs the domain to be complete. It goes through the criterion that a map whose adjoint is bounded below is surjective: geometric Hahn–Banach shows that the closure of the image of a ball contains a ball, and Banach's lemma ContinuousLinearMap.exists_preimage_norm_le_of_mem_closure upgrades this to surjectivity. Completeness of the domain cannot be dropped: the inclusion of finitely supported sequences into ℓ² has dense proper range, while its adjoint is surjective.

Main declarations

• ContinuousLinearMap.ker_precomp_eq_orthogonalBilin_range: ker T* = (range T)ᗮ.
• ContinuousLinearMap.ker_eq_orthogonalBilin_range_precomp: ker T = (range T*)_⊥.
• ContinuousLinearMap.range_precomp_eq_orthogonalBilin_ker: if range T is closed, then range T* = (ker T)ᗮ.
• ContinuousLinearMap.surjective_of_norm_le_norm_comp: a map whose adjoint is bounded below is surjective.
• ContinuousLinearMap.isClosed_range_precomp_iff: the closed-range theorem.
• ContinuousLinearMap.bijective_precomp_iff: a map is bijective iff its transpose is.

References

• W. Rudin, Functional Analysis, 2nd ed., Theorems 4.12, 4.14 and 4.15.

theorem ContinuousLinearMap.ker_precomp_eq_orthogonalBilin_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] (T : E →L[𝕜] F) : (↑(precomp 𝕜 T)).ker = Submodule.orthogonalBilin (topDualPairing 𝕜 F).flip (↑T).range

The kernel of the adjoint is the annihilator of the range.

theorem ContinuousLinearMap.range_precomp_le_orthogonalBilin_ker {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] (T : E →L[𝕜] F) : (↑(precomp 𝕜 T)).range ≤ Submodule.orthogonalBilin (topDualPairing 𝕜 E).flip (↑T).ker

The range of the adjoint annihilates the kernel.

theorem ContinuousLinearMap.ker_eq_orthogonalBilin_range_precomp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [SeparatingDual 𝕜 F] (T : E →L[𝕜] F) : (↑T).ker = Submodule.orthogonalBilin (topDualPairing 𝕜 E) (↑(precomp 𝕜 T)).range

When continuous functionals separate the points of F, the kernel of a map is the preannihilator of the range of its adjoint.

theorem ContinuousLinearMap.range_precomp_eq_orthogonalBilin_ker {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (hT : IsClosed ↑(↑T).range) : (↑(precomp 𝕜 T)).range = Submodule.orthogonalBilin (topDualPairing 𝕜 E).flip (↑T).ker

Closed-range theorem, range of the adjoint. If a bounded operator between Banach spaces has closed range, then the range of its adjoint is exactly the annihilator of its kernel.

theorem ContinuousLinearMap.isClosed_range_precomp_of_isClosed_range {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [IsRCLikeNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) (hT : IsClosed ↑(↑T).range) : IsClosed ↑(↑(precomp 𝕜 T)).range

If a bounded operator between Banach spaces has closed range, then so does its adjoint.

theorem ContinuousLinearMap.mem_closure_image_closedBall_of_norm_le_norm_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (S : E →L[𝕜] F) {K : NNReal} (hK : ∀ (g : StrongDual 𝕜 F), ‖g‖ ≤ ↑K * ‖g ∘SL S‖) (y : F) : y ∈ closure (⇑S '' Metric.closedBall 0 (↑K * ‖y‖))

If the adjoint of S is bounded below with constant K, then every y lies in the closure of the image of the closed ball of radius K * ‖y‖.

theorem ContinuousLinearMap.surjective_of_norm_le_norm_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (S : E →L[𝕜] F) {K : NNReal} (hK : ∀ (g : StrongDual 𝕜 F), ‖g‖ ≤ ↑K * ‖g ∘SL S‖) : Function.Surjective ⇑S

A bounded operator on a complete seminormed space whose adjoint is bounded below is surjective.

theorem ContinuousLinearMap.isClosed_range_of_isClosed_range_precomp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (T : E →L[𝕜] F) (h : IsClosed ↑(↑(precomp 𝕜 T)).range) : IsClosed ↑(↑T).range

Closed-range theorem, reverse implication. If the adjoint of a bounded operator on a complete seminormed space has closed range, then the operator has closed range. The codomain need not be complete.

theorem ContinuousLinearMap.isClosed_range_precomp_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : IsClosed ↑(↑(precomp 𝕜 T)).range ↔ IsClosed ↑(↑T).range

Closed-range theorem. A bounded operator between Banach spaces has closed range if and only if its adjoint has closed range.

@[simp]

theorem ContinuousLinearMap.bijective_precomp_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] (T : E →L[𝕜] F) : Function.Bijective ⇑(precomp 𝕜 T) ↔ Function.Bijective ⇑T

A bounded map between Banach spaces is bijective if and only if its Banach transpose is bijective. The transpose here is precomposition on the continuous dual, not the Hilbert adjoint.