Rank of a linear map is lower semi continuous

Stream: Is there code for X?

[Yury G. Kudryashov]

Do we have a theorem that says "if f : E →L[k] F has rank n, then any g in some nhd of f has rank at least n"?

[Heather Macbeth]

I doubt it. The closest is probably the fact that the group of units is open, docs#units.is_open.

[Damiano Testa]

In algebraic geometry, this is usually referred to as upper-semicontinuity of kernels :upside_down:

[Yury G. Kudryashov]

@Sebastien Gouezel @Heather Macbeth Is there some meaningful infinite dimensional version of this fact, or it's OK to just work with a matrix?

[Heather Macbeth]

I wonder if something can be stated for Fredholm operators? But in the long term we probably need both the matrix version and the linear map version, so (I think) for now you might as well do whichever is easier.

[Sebastien Gouezel]

The statement makes sense (and is true) when E or F (or both) is infinite dimensional. No need to work with matrices: just take n independent vectors in the image, write them as f v_1, ..., f v_n, and say that g v_1, ..., g v_n remain free when g is close enough to f. You need the fact that being a free family is an open property, which is indeed most easily done with matrices and determinants: take linear forms l_1, ..., l_n such that l_i (w_j) is an invertible matrix, then it remains invertible for w'_j close enough to w_j.

[Yury G. Kudryashov]

This means ∀ n : ℕ, n ≤ dim 𝕜 (range (f x)) → ∀ᶠ y in 𝓝 x, n ≤ dim 𝕜 (range (f y)). I guess, for infinite values of n this is false because it should be possible to make the domain where the first n vectors are linearly independent decrease with n.

[Sebastien Gouezel]

Yes, just for finite n.

My proof sketch above works fine on the reals or the complexes, but not on general fields because it requires Hahn-Banach to produce the linear forms. Here is a better and more direct argument, over any complete nondiscrete normed field. Start from $w_1,\dotsc, w_n$ which are free. On the finite-dimensional space they span, all norms are equivalent by docs#linear_map.continuous_of_finite_dimensional and friends. So, there exists $c>0$ such that, for all $(\lambda_1,\dotsc, \lambda_n)$, one has $c \max |\lambda_i|\leq \|\sum \lambda_i w_i\|$.

Consider now perturbations $w_i+h_i$ of $w_i$, with $\|h_i\|\leq \epsilon$ suitably small. Then, for any $(\lambda_1,\dotsc, \lambda_n)$, one has $\|\sum \lambda_i (w_i+h_i)\|\geq \|\sum \lambda_i w_i\| - n \epsilon \max |\lambda_i| \geq (c - n \epsilon) \max|\lambda_i|$. If $\epsilon$ is small enough, $c-n\epsilon>0$. If $\sum \lambda_i (w_i+h_i) = 0$, this implies $\max|\lambda_i|=0$, so $\lambda_1 = \dotsc = \lambda_n = 0$, i.e., the family $(w_1+h_1, \dotsc, w_n+h_n)$ is free.