Rank bounds for finite spans of linear maps

Rank subadditivity bounds the rank of a linear combination by the sum of rank budgets for its generators. The linear maps need not have finite-dimensional domains or codomains. Also extracts a Fin-indexed linearly independent spanning subfamily from any Fin-indexed family over a division ring.

Main results

• LinearMap.rank_smul_le: scalar multiplication does not increase rank.
• LinearMap.rank_le_sum_of_mem_span: a rank budget for a finite span.
• Submodule.exists_linearIndependent_fin_comp: every Fin-indexed family over a division ring contains a Fin-indexed linearly independent subfamily with the same span.

References

• The linear-map span lemmas are ported from LinearAlgebra/Rank.lean in S. Schlesinger, Algebraic circuit formalizations in Complexitylib.
• [OAI26a]

theorem LinearMap.rank_smul_le {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] (c : K) (f : A →ₗ[K] B) : (c • f).rank ≤ f.rank

Scalar multiplication does not increase the rank of a linear map.

theorem LinearMap.rank_le_sum_of_mem_span {K : Type u_1} {A : Type u_2} {B : Type u_3} [Field K] [AddCommGroup A] [Module K A] [AddCommGroup B] [Module K B] {ι : Type u_4} [Fintype ι] (f : A →ₗ[K] B) (family : ι → A →ₗ[K] B) (budget : ι → ℕ) (hmem : f ∈ Submodule.span K (Set.range family)) (hbound : ∀ (i : ι), (family i).rank ≤ ↑(budget i)) : f.rank ≤ ∑ i : ι, ↑(budget i)

A linear map in the span of a finite family has rank at most the sum of any rank budgets for its generators.

theorem Submodule.exists_linearIndependent_fin_comp (K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {h : ℕ} (v : Fin h → V) : ∃ (k : ℕ) (a : Fin k → Fin h), Function.Injective a ∧ span K (Set.range (v ∘ a)) = span K (Set.range v) ∧ LinearIndependent K (v ∘ a)

Every finite family v : Fin h → V over a division ring contains a Fin-indexed linearly independent subfamily v ∘ a with the same span.