Rank bounds for finite spans of linear maps #
Rank subadditivity bounds the rank of any linear combination by the sum of rank budgets for its generators. No finite-dimensionality assumption is needed: ranks are cardinals, while the supplied budgets are natural numbers.
theorem
LinearMap.rank_le_sum_of_mem_span
{K : Type u}
{A : Type v}
{B : Type w}
[Field K]
[AddCommGroup A]
[Module K A]
[AddCommGroup B]
[Module K B]
{ι : Type z}
[Fintype ι]
(target : A →ₗ[K] B)
(family : ι → A →ₗ[K] B)
(budget : ι → ℕ)
(targetMem : target ∈ Submodule.span K (Set.range family))
(localBound : ∀ (index : ι), (family index).rank ≤ ↑(budget index))
:
The rank of a linear map in the span of a finite family is at most the sum of any pointwise rank budgets for that family.