Strict linear maps with closed range are closed under finite-rank perturbation

Fix 𝕜 a complete nontrivially normed field, and E, F two topological vector spaces over 𝕜. This file contains various results expressing that the set of continuous linear maps u : E →L[𝕜] F which are strict and have closed range is "stable under finite-rank perturbations".

More precisely, we prove the following statements:

• ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict: given a closed subspace A of E of finite codimension, we have that u is strict with closed range if and only if u.domRestrict A is strict with closed range.
• ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid: if u, v : E →L[𝕜] F differ by a finite rank continuous linear map, then u is strict with closed range if and only if v is strict with closed range.
• ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient: given a complemented finite dimensional subspace B of F, we have that u is strict with closed range if and only if B.mkQL ∘L u is strict with closed range.

These three results show up crucially when developing the theory of Fredholm operators between topological vector spaces. Note that none of the results here use the Hahn-Banach theorem, so there is no significant restriction on the field.

Implementation details

This file covers almost exactly the content of N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 1. However, there are two notable changes compared to Bourbaki :

• We treat all topological vector spaces over complete nontrivially normed fields, where Bourbaki restricts to locally convex spaces over ℝ or ℂ. To do so, we have to tweak one statement by assuming that a finite dimensional subspace is complemented, which is always the case when you have Hahn-Banach available.
• We give a different proof, where we reduce the statement to AddMonoidHom.isStrictMap_prodMap_iff. This gives a slightly longer proof, but we claim that it is more natural.

Note that these two changes are independent: the extra generality could have been achieved with Bourbaki's proof.

References

• N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 1

Proof of ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict

Let u : E → F be a continuous linear map, and A a finite codimension closed subspace of E. We want to show that u is strict with closed range if and only if its restriction u.domRestrict A : A → F is strict with closed range.

We do the proof in five steps. Note that we have commented the whole proof, so hopefully you can follow the argument by reading the source code.

Step 1

We prove the theorem under the assumptions that

• u is surjective
• u.ker is disjoint from A (i.e. u is injective on A)
• u.domRestrict A has closed range

The strategy of proof is to decompose both spaces into complementary subspace, with one of the spaces being finite dimensional and u preserving this decomposition.

The result then follows from AddMonoidHom.isStrictMap_prodMap_iff and ContinuousLinearMap.isStrictMap_of_finiteDimensional.

Step 2

We prove the theorem under the assumptions that

• u is surjective
• u.ker is disjoint from A (i.e. u is injective on A)

Step 3

We prove the theorem under the assumptions that

• u has closed range
• u.ker is disjoint from A (i.e. u is injective on A)

Step 4

We prove the theorem under the assumption that u.ker is disjoint from A (i.e. u is injective on A).

Step 5

We now deduce from the previous steps the full strength of the theorem.

theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_restrict {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E) (A_closed : IsClosed ↑A) [A.CoFG] : Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔ Topology.IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed ↑(↑(u.domRestrict A)).range

Let u : E → F be a continuous linear map, and A a closed subspace of E of finite codimension. Then u is strict with closed range if and only if its restriction u.domRestrict A : A → F is strict with closed range.

This is N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 1, Prop. 1.

Consequences

theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_eqOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] (u v : E →L[𝕜] F) (A : Submodule 𝕜 E) [A.CoFG] (h_eqOn : Set.EqOn ⇑u ⇑v ↑A) : Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔ Topology.IsStrictMap ⇑v ∧ IsClosed ↑(↑v).range

If two continuous linear maps u, v : E → F agree on a subspace A of E with finite codimension, then u is strict with closed range if and only if v is strict with closed range.

theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_of_finiteRangeSetoid {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] (u v : E →L[𝕜] F) (h_equiv : ↑u ≈ ↑v) : Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔ Topology.IsStrictMap ⇑v ∧ IsClosed ↑(↑v).range

If two linear maps u, v : E → F differ by a finite rank linear map (recall that this is denoted u.toLinearMap ≈ v.toLinearMap in scope LinearMap.FiniteRangeSetoid), then u is strict with closed range if and only if v is strict with closed range.

This is N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 1, Cor. 1.

theorem ContinuousLinearMap.isStrictMap_isClosed_range_iff_quotient {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3} [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space F] (u : E →L[𝕜] F) (A : Submodule 𝕜 F) [FiniteDimensional 𝕜 ↥A] (A_compl : A.ClosedComplemented) : Topology.IsStrictMap ⇑u ∧ IsClosed ↑(↑u).range ↔ Topology.IsStrictMap ⇑(A.mkQL ∘SL u) ∧ IsClosed ↑(↑(A.mkQL ∘SL u)).range

Let u : E → F be a continuous linear map, and A a complemented finite dimensional subspace of F. Then u is strict with closed range if and only if the induced map E → F ⧸ A is strict with closed range.

This is N. Bourbaki, Théories Spectrales, Chapitre III, § 3, n° 1, Cor. 2.