Rank bounds along a pencil

A pencil is an affine line t ↦ A + t • B of matrices or linear maps. Each minor of A + t • B is a polynomial in t, so the condition rank (A + t • B) ≤ p either holds for every t or fails for all but finitely many t: a polynomial with infinitely many roots is zero. This is the one-parameter case of the Zariski closedness of rank bounds in TauCeti.LinearAlgebra.Matrix.Rank.Closed, stated over any field and without coordinates on the source.

Dividing f + t • g by t and letting t → ∞ turns a bound on the pencil into a bound on its direction g. Algebraically, the bound for infinitely many t passes to the reversed pencil g + s • f, where it then holds at s = 0. The same argument tolerates a fixed summand W that is not rescaled: a bound on range (f + t • g) ⊔ W for infinitely many t bounds range g ⊔ W. This is the linear-algebraic heart of the Lefschetz–Whitehead rank estimate, Lemma 2 of Łojasiewicz's triangulation of semianalytic sets, where W is spanned by the derivative in the line parameter.

Main results

• Matrix.rank_add_smul_le_of_infinite: a rank bound on a matrix pencil holding at infinitely many parameters holds at every parameter.
• LinearMap.finrank_range_add_smul_le_of_infinite: the same for a pencil of linear maps into a finite-dimensional space.
• LinearMap.finrank_range_sup_le_of_infinite: a bound on range (f + t • g) ⊔ W at infinitely many t bounds range g ⊔ W.
• LinearMap.finrank_range_lt_of_infinite: if moreover v ∉ range g, then a bound p on range (f + t • g) ⊔ K ∙ v at infinitely many t forces finrank (range g) < p.

References

• S. Łojasiewicz, Triangulation of semi-analytic sets, Ann. Scuola Norm. Sup. Pisa (3) 18 (1964), 449–474, §2, Lemma 2.

theorem Matrix.rank_add_smul_le_of_infinite {m : Type u_1} {n : Type u_2} {K : Type u_3} [Finite m] [Fintype n] [Field K] {A B : Matrix m n K} {p : ℕ} (h : {t : K | (A + t • B).rank ≤ p}.Infinite) (t : K) : (A + t • B).rank ≤ p

Rank bounds along a matrix pencil. If rank (A + t • B) ≤ p for infinitely many scalars t, then it holds for every t: each (p + 1) × (p + 1) minor of A + t • B is a polynomial in t with infinitely many roots, hence zero.

theorem LinearMap.finrank_range_add_smul_le_of_infinite {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] [FiniteDimensional K N] {f g : M →ₗ[K] N} {p : ℕ} (h : {t : K | Module.finrank K ↥(f + t • g).range ≤ p}.Infinite) (t : K) : Module.finrank K ↥(f + t • g).range ≤ p

Rank bounds along a pencil of linear maps. If finrank (range (f + t • g)) ≤ p for infinitely many scalars t, then it holds for every t. The source need not be finite-dimensional: both maps factor through the quotient by ker f ⊓ ker g, which embeds into N × N.

theorem LinearMap.finrank_range_sup_le_of_infinite {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] [FiniteDimensional K N] {f g : M →ₗ[K] N} {W : Submodule K N} {p : ℕ} (h : {t : K | Module.finrank K ↥((f + t • g).range ⊔ W) ≤ p}.Infinite) : Module.finrank K ↥(g.range ⊔ W) ≤ p

Rank bounds pass to the direction of a pencil. If range (f + t • g) ⊔ W has dimension at most p for infinitely many scalars t, then so does range g ⊔ W. For t ≠ 0 the range of f + t • g is that of g + t⁻¹ • f, so the reversed pencil g + s • f satisfies the bound at infinitely many s and hence at s = 0.

theorem LinearMap.finrank_range_lt_of_infinite {K : Type u_1} {M : Type u_2} {N : Type u_3} [Field K] [AddCommGroup M] [Module K M] [AddCommGroup N] [Module K N] [FiniteDimensional K N] {f g : M →ₗ[K] N} {v : N} (hv : v ∉ g.range) {p : ℕ} (h : {t : K | Module.finrank K ↥((f + t • g).range ⊔ K ∙ v) ≤ p}.Infinite) : Module.finrank K ↥g.range < p

The rank drop of a transverse direction. If v ∉ range g and range (f + t • g) ⊔ K ∙ v has dimension at most p for infinitely many scalars t, then finrank (range g) < p.