Stability under finite-rank perturbation of strict linear maps with closed range

The following statement (Bourbaki, Théories Spectrales, Chapitres 3 à 5, Chapter III, § 3, Prop. 1) is a key step in Bourbaki's approach to the theory of Fredholm operators between arbitrary TVSs.

Let $$E$$ and $$F$$ be topological vector spaces over a nontrivially normed field, $$A$$ a finite-codimension closed subspace of $$E$$. A continuous linear map $$u : E \to F$$ is strict with closed range if and only if its restriction to $$A$$ is strict with closed range.

As a corollary, adding a finite rank operator to a strict operator with closed range yields a strict operator with closed range.

I spent some time Mathlib-ifying the proof, so I thought I may as well lay down these details somewhere.

In what follows $$A$$ is always closed with finite codimension. Recall that any algebraic complement to $$A$$ is then a topological complement (thanks to #38579).

Step 1

If the kernel of $$u$$ is disjoint from $$A$$ and $$u$$ is strict with closed range, then its restriction to $$A$$ is a closed embedding (hence strict with closed range).

Denote by $$\pi : E \to E / \ker u$$ the quotient map. By definition of strictness, $$\tilde{u} : E / \ker u \to F$$ is an embedding. Because its range is closed, it's a closed embedding.

Now, pick $$S$$ an algebraic complement to $$A$$ which contains $$\ker u$$. We know that $$S$$ is also a topological complement of $$A$$.
Hence, the projection $$p$$ on $$A$$ parallel to $$S$$ is continuous. Because it vanishes on $$S$$, hence on $$\ker u$$, it lifts to a map $$\tilde{p} : E / \ker u \to A$$, which is a right inverse for $$\pi|_A$$. It follows that $$\pi|_A$$ is a topological embedding.
Furthermore, its range $$\pi(A)$$ is closed, because $$\pi^{-1}(\pi(A))$$ contains $$A$$ which is closed with finite codimension (see #38461).
So $$\pi|_A$$ is also a closed embedding.

It follows that $$u|_A = \tilde{u} \circ \pi|_A$$ is a closed embedding.

Step 2

If $$u$$ is surjective, if the kernel of $$u$$ is disjoint from $$A$$, and if $$u|_A$$ is strict with closed range, then $$u$$ is strict.

Once again, we pick $$S$$ an algebraic (hence topological) complement to $$A$$ which contains $$\ker u$$. Because the kernel of $$u$$ is fully contained in $$S$$, $$u(S)$$ and $$u(A)$$ are disjoint. By surjectivity, they are algebraic complements in $$F$$, hence topological complements since $$u(S)$$ has finite dimension and $$u(A)$$ is closed.

Because strictness is invariant under composition by homeomorphisms, we are left to prove that the map $$A \times S \to u(A) \times u(S)$$
induced by $$u$$ on each coordinate is strict. #38421 reduces this to strictness of each coordinate. For the first map this is true by assumption.

For the second one, we note that $$u(S)$$ intersects trivially the closed subspace $$u(A)$$. This means that $${0}$$ is closed in $$u(S)$$, so that it is Hausdorff. Then, we use that any continuous linear map to a Hausdorff finite dimensional space is strict.

Step 3

If the kernel of $$u$$ is disjoint from $$A$$, and if $$u|_A$$ is strict with closed range, then $$u$$ is strict with closed range.

Once again, we pick $$S$$ an algebraic (hence topological) complement to $$A$$ which contains $$\ker u$$.
We have $$u(E) = u(A) + u(S)$$ and $$u(S)$$ is finite dimensional, so by #38461 $$u(E)$$ is closed. Replacing $$F$$ by $$u(E)$$ and $$u$$ by its co-restriction to $$u(E)$$, we reduced to step 2.

Step 4

Assume the kernel of $$u$$ is disjoint from $$A$$. Then $$u$$ is strict with closed range if and only if $$u|_A$$ is as well.

This is precisely step 1 + step 3.

Step 5

Going back to the general statement, let $$N := A \cap \ker u$$, $$G := E / N$$, $$\pi : E \to G$$ the projection, $$v : G \to F$$ the map induced by $$u$$, and $$B := \pi(A)$$.

We have :

• $$u(E) = v(G)$$ and $$u(A) = v(B)$$
• $$B$$ has finite codimension in $$A$$
• $$B$$ is closed, because $$A$$ is saturated, hence $$\pi^{-1}(B) = A$$
• $$\pi : E \to G$$ is a quotient map, so strictness of $$v$$ is equivalent to strictness of $$v \circ \pi = u$$.
• $$\pi$$ is an open quotient map, so it's restriction $$\pi' : A = \pi^{-1}(B) \to B$$ is as well. This ensures that strictness of $$v|_B$$ is equivalent to strictness of $$v|_B \circ \pi' = u|_A$$.

Thus we have reduced the statement to step 4.

The issue supplies a five-step proof plan but names no target file or test. Read the linked results in #38579, #38461, and #38421, then inspect closed pull request #39100 before deciding where the formalization belongs. Done means the stated stability theorem and its finite-rank corollary are formalized with appropriate verification.