The row span of a matrix over arbitrary index types

A matrix whose rows and columns are indexed by arbitrary types has no rank in the sense of linear algebra. Two standard substitutes are the dimension of the span of its rows and the supremum of the ranks of its finite submatrices; this module proves them interchangeable in the bounded form that a rank hypothesis uses, so that no cardinal supremum is needed: the row span has dimension at most n exactly when every finite submatrix has rank at most n (rank_span_rows_le_iff). The same criterion is restated for the row span presented as the range of Finsupp.lift (rank_range_lift_le_iff), which is how the connection matrices of RS/Novel/Skein/ConnectionRank.lean present theirs.

The point of substance is that a finite-dimensional space of functions on κ is separated by finitely many coordinates (exists_finset_separating): that is what makes the row rank of an infinite matrix visible on a single finite submatrix.

Separating a space of functions on finitely many coordinates

theorem RS.exists_finset_separating {K : Type u_1} [Field K] {κ : Type u_2} (U : Submodule K (κ → K)) [FiniteDimensional K ↥U] : ∃ (T : Finset κ), ∀ w ∈ U, (∀ j ∈ T, w j = 0) → w = 0

A finite-dimensional space of functions on κ is separated by finitely many coordinates: some finite T is such that a vector of the space vanishing throughout T is zero.

Finite submatrices and the row span

def RS.submatrixOn {K : Type u_1} {ι : Type u_2} {κ : Type u_3} (M : ι → κ → K) (S : Finset ι) (T : Finset κ) : Matrix (↥S) (↥T) K

The submatrix of M on the rows S and the columns T.

Equations

• RS.submatrixOn M S T = (Matrix.of M).submatrix Subtype.val Subtype.val

theorem RS.rank_span_rows_le_iff {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} (M : ι → κ → K) (n : ℕ) : Module.rank K ↥(Submodule.span K (Set.range M)) ≤ ↑n ↔ ∀ (S : Finset ι) (T : Finset κ), (submatrixOn M S T).rank ≤ n

The row span and the finite submatrices agree in bounded form. The span of the rows of M has dimension at most n exactly when every finite submatrix of M has rank at most n.

theorem RS.range_lift_eq_span_rows {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} (M : ι → κ → K) : ((Finsupp.lift (κ → K) K ι) M).range = Submodule.span K (Set.range M)

The range of Finsupp.lift at M is the span of the rows of M.

theorem RS.rank_range_lift_le_iff {K : Type u_1} [Field K] {ι : Type u_2} {κ : Type u_3} (M : ι → κ → K) (n : ℕ) : Module.rank K ↥((Finsupp.lift (κ → K) K ι) M).range ≤ ↑n ↔ ∀ (S : Finset ι) (T : Finset κ), (submatrixOn M S T).rank ≤ n

The bounded row-rank criterion, for the row span presented as the range of Finsupp.lift.