Stream: Is there code for X?
Yury G. Kudryashov (Mar 29 2021 at 18:18):
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
Heather Macbeth (Mar 29 2021 at 19:30):
I doubt it. The closest is probably the fact that the group of units is open, docs#units.is_open.
Damiano Testa (Mar 29 2021 at 20:03):
In algebraic geometry, this is usually referred to as upper-semicontinuity of kernels :upside_down:
Yury G. Kudryashov (Mar 29 2021 at 20:06):
@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 (Mar 29 2021 at 20:21):
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 (Mar 29 2021 at 20:57):
The statement makes sense (and is true) when
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
Yury G. Kudryashov (Mar 29 2021 at 22:40):
∀ 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
Sebastien Gouezel (Mar 30 2021 at 05:27):
Yes, just for finite
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 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 such that, for all , one has .
Consider now perturbations of , with suitably small. Then, for any , one has . If is small enough, . If , this implies , so , i.e., the family is free.
Last updated: May 16 2021 at 05:21 UTC