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.

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.
• Matrix.natCast_rank_eq_rank_toLin': the natural matrix rank agrees with linear-map rank.

References

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

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 Matrix.natCast_rank_eq_rank_toLin' {K : Type u_1} {m : Type u_2} {n : Type u_3} [Field K] [Fintype n] [DecidableEq n] (M : Matrix m n K) : ↑M.rank = (toLin' M).rank

The natural rank of a finite matrix agrees with the cardinal rank of its linear map.