Block ranks and cut ranks

The block rank M.blockRank S T of a matrix M over a field is the rank of its block with rows in the set S and columns in the set T: the dimension of the span of the rows of M.submatrix (↑) (↑). It agrees with Matrix.rank of that submatrix (Matrix.blockRank_eq_rank) but needs no Fintype instance on the sets.

The cut rank M.cutRank X of a square matrix is the block rank of the rows in X and the columns outside X. For the adjacency matrix of a graph over 𝔽₂ this is the cut rank of X in the graph Oum; here it measures how far a quadratic form is from splitting across the cut. A quadratic form v ⬝ᵥ Q *ᵥ v on a vector glued from a part u on X and a part w off X is a form in u, plus a form in w, plus the pairing u ⬝ᵥ C *ᵥ w of the block C of the polar matrix Q + Qᵀ with rows X and columns off X (Matrix.dotProduct_mulVec_self_eq_add). A matrix that carries a block R on rows f and columns g and vanishes elsewhere (Matrix.extendBlock) has the bilinear form of R as its quadratic form (Matrix.dotProduct_mulVec_self_eq_of_submatrix).

Block ranks grow with the block, drop by at most one per deleted row, are invariant under transposition and injective relabelling, and add over blocks whose rows live on disjoint sets of columns. Cut ranks of a symmetric matrix are symmetric under complementation.

Main definitions

• Matrix.blockRank: the block rank M.blockRank S T, the rank of the block of M with rows S and columns T.
• Matrix.cutRank: the cut rank M.cutRank X, the rank of the block of M with rows X and columns Xᶜ.
• Matrix.extendBlock: the square matrix extendBlock f g R carrying R on the rows f and the columns g.

Main results

• Matrix.blockRank_eq_rank: block ranks are ranks of submatrices.
• Matrix.blockRank_mono, Matrix.blockRank_le_add_ncard_sdiff, Matrix.blockRank_transpose, Matrix.blockRank_submatrix, Matrix.add_blockRank_le_of_disjoint: the algebra of block ranks.
• Matrix.cutRank_le_add_ncard_sdiff, Matrix.IsSymm.cutRank_compl: the algebra of cut ranks.
• Matrix.dotProduct_mulVec_self_eq_add: a quadratic form across a cut.
• Matrix.dotProduct_mulVec_self_eq_of_submatrix: a bilinear form as a quadratic form.

References

• S. Oum, Rank-width and vertex-minors

noncomputable def Matrix.blockRank {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) (S : Set m) (T : Set n) : ℕ

The rank of the block of M with rows in S and columns in T: the dimension of the span of the rows of the block. It equals Matrix.rank of the submatrix (Matrix.blockRank_eq_rank) but needs no Fintype instance on T.

noncomputable def Matrix.cutRank {ι : Type u_5} {K : Type u_8} [Field K] (M : Matrix ι ι K) (X : Set ι) : ℕ

The cut rank of a square matrix M at a set X of indices: the rank of the block of M with rows in X and columns outside X.

theorem Matrix.blockRank_eq_rank {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite m] (S : Set m) (T : Set n) [Fintype ↑T] : M.blockRank S T = (M.submatrix Subtype.val Subtype.val).rank

Block ranks are ranks of submatrices.

theorem Matrix.blockRank_mono_right {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite n] (S : Set m) {T T' : Set n} (h : T' ⊆ T) : M.blockRank S T' ≤ M.blockRank S T

Deleting columns does not increase the rank of a block.

theorem Matrix.blockRank_mono_left {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite n] {S S' : Set m} (T : Set n) (h : S' ⊆ S) : M.blockRank S' T ≤ M.blockRank S T

Deleting rows does not increase the rank of a block.

theorem Matrix.blockRank_mono {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite n] {S S' : Set m} {T T' : Set n} (hS : S' ⊆ S) (hT : T' ⊆ T) : M.blockRank S' T' ≤ M.blockRank S T

A sub-block has at most the rank of the block.

theorem Matrix.blockRank_le_ncard {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite m] (S : Set m) (T : Set n) : M.blockRank S T ≤ S.ncard

The rank of a block is at most the number of its rows.

theorem Matrix.blockRank_le_add_ncard_sdiff {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite m] [Finite n] {S S' : Set m} (T : Set n) (h : S' ⊆ S) : M.blockRank S T ≤ M.blockRank S' T + (S \ S').ncard

Deleting the rows outside S' lowers the rank of a block by at most their number.

theorem Matrix.blockRank_congr {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] {M M' : Matrix m n K} {S : Set m} {T : Set n} (h : ∀ i ∈ S, ∀ j ∈ T, M i j = M' i j) : M.blockRank S T = M'.blockRank S T

Blocks that agree entrywise have the same rank.

theorem Matrix.blockRank_transpose {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite m] [Finite n] (S : Set m) (T : Set n) : M.transpose.blockRank T S = M.blockRank S T

Row rank equals column rank: transposing a matrix transposes its blocks.

theorem Matrix.blockRank_submatrix {m : Type u_1} {n : Type u_2} {m' : Type u_3} {n' : Type u_4} {K : Type u_8} [Field K] (M : Matrix m n K) {f : m' → m} {g : n' → n} (hf : Function.Injective f) (hg : Function.Injective g) (S : Set m') (T : Set n') : (M.submatrix f g).blockRank S T = M.blockRank (f '' S) (g '' T)

Relabelling the rows and columns injectively does not change the rank of a block.

theorem Matrix.add_blockRank_le_of_disjoint {m : Type u_1} {n : Type u_2} {K : Type u_8} [Field K] (M : Matrix m n K) [Finite n] {S S₁ S₂ : Set m} {T T₁ T₂ : Set n} (h₁ : S₁ ⊆ S) (h₂ : S₂ ⊆ S) (hT : Disjoint T₁ T₂) (hM₁ : ∀ i ∈ S₁, ∀ j ∈ T, j ∉ T₁ → M i j = 0) (hM₂ : ∀ i ∈ S₂, ∀ j ∈ T, j ∉ T₂ → M i j = 0) : M.blockRank S₁ T + M.blockRank S₂ T ≤ M.blockRank S T

Blocks on disjoint columns. If, among the columns T, the rows of S₁ vanish outside T₁ and the rows of S₂ vanish outside T₂, where T₁ and T₂ are disjoint, then the ranks of the blocks S₁ × T and S₂ × T add up to at most the rank of the block S × T.

theorem Matrix.cutRank_eq_rank {ι : Type u_5} {K : Type u_8} [Field K] (M : Matrix ι ι K) [Finite ι] (X : Set ι) [Fintype ↑Xᶜ] : M.cutRank X = (M.submatrix Subtype.val Subtype.val).rank

Cut ranks are ranks of submatrices.

theorem Matrix.cutRank_le_add_ncard_sdiff {ι : Type u_5} {K : Type u_8} [Field K] (M : Matrix ι ι K) [Finite ι] {D X : Set ι} (h : D ⊆ X) : M.cutRank X ≤ M.cutRank D + (X \ D).ncard

Passing from X to a subset D lowers the cut rank by at most |X \ D|.

theorem Matrix.ncard_add_cutRank_le_of_subset {ι : Type u_5} {K : Type u_8} [Field K] (M : Matrix ι ι K) [Finite ι] {D X : Set ι} (h : D ⊆ X) : D.ncard + M.cutRank X ≤ M.cutRank D + X.ncard

Passing from X to a subset D lowers the cut rank by at most |X| - |D|: |D| + ρ(X) ≤ ρ(D) + |X|.

theorem Matrix.cutRank_transpose_compl {ι : Type u_5} {K : Type u_8} [Field K] (M : Matrix ι ι K) [Finite ι] (X : Set ι) : M.transpose.cutRank Xᶜ = M.cutRank X

The cut rank of the transpose at the complement is the cut rank.

theorem Matrix.IsSymm.cutRank_compl {ι : Type u_5} {K : Type u_8} [Field K] [Finite ι] {M : Matrix ι ι K} (hM : M.IsSymm) (X : Set ι) : M.cutRank Xᶜ = M.cutRank X

The cut rank of a symmetric matrix is symmetric under complementation.

theorem Matrix.cutRank_le_ncard {ι : Type u_5} {K : Type u_8} [Field K] (M : Matrix ι ι K) [Finite ι] (X : Set ι) : M.cutRank X ≤ X.ncard

The cut rank is at most the size of the set.

Quadratic forms across a cut

theorem Matrix.dotProduct_mulVec_self_eq_add {ι : Type u_5} {R : Type u_9} [CommRing R] [Fintype ι] (Q : Matrix ι ι R) (X : Set ι) [DecidablePred fun (x : ι) => x ∈ X] (v : ι → R) : v ⬝ᵥ Q.mulVec v = X.domRestrict v ⬝ᵥ (Q.submatrix Subtype.val Subtype.val).mulVec (X.domRestrict v) + Xᶜ.domRestrict v ⬝ᵥ (Q.submatrix Subtype.val Subtype.val).mulVec (Xᶜ.domRestrict v) + X.domRestrict v ⬝ᵥ ((Q + Q.transpose).submatrix Subtype.val Subtype.val).mulVec (Xᶜ.domRestrict v)

A quadratic form across a cut. For a set X of indices, the quadratic form v ⬝ᵥ Q *ᵥ v is the form of the block Q on X × X at the part of v on X, plus the form of the block on Xᶜ × Xᶜ at the part of v off X, plus the pairing of the two parts through the block of the polar matrix Q + Qᵀ with rows X and columns Xᶜ.

noncomputable def Matrix.extendBlock {ι : Type u_5} {κ : Type u_6} {κ' : Type u_7} {α : Type u_9} [Zero α] (f : κ → ι) (g : κ' → ι) (R : Matrix κ κ' α) : Matrix ι ι α

The square matrix that carries R on the rows f and the columns g, and vanishes elsewhere. For injective f and g its quadratic form is the bilinear form of R (Matrix.dotProduct_mulVec_self_eq_of_submatrix).

theorem Matrix.extendBlock_apply_apply {ι : Type u_5} {κ : Type u_6} {κ' : Type u_7} {α : Type u_9} [Zero α] {f : κ → ι} {g : κ' → ι} (hf : Function.Injective f) (hg : Function.Injective g) (R : Matrix κ κ' α) (a : κ) (b : κ') : extendBlock f g R (f a) (g b) = R a b

For injective f and g, the entry of extendBlock f g R at (f a, g b) is R a b.

theorem Matrix.submatrix_extendBlock {ι : Type u_5} {κ : Type u_6} {κ' : Type u_7} {α : Type u_9} [Zero α] {f : κ → ι} {g : κ' → ι} (hf : Function.Injective f) (hg : Function.Injective g) (R : Matrix κ κ' α) : (extendBlock f g R).submatrix f g = R

For injective f and g, the block of extendBlock f g R on the rows f and the columns g is R.

theorem Matrix.extendBlock_eq_zero {ι : Type u_5} {κ : Type u_6} {κ' : Type u_7} {α : Type u_9} [Zero α] {f : κ → ι} {g : κ' → ι} (R : Matrix κ κ' α) {i j : ι} (h : i ∉ Set.range f ∨ j ∉ Set.range g) : extendBlock f g R i j = 0

extendBlock f g R vanishes at (i, j) when i is not in the range of f or j is not in the range of g.

theorem Matrix.dotProduct_mulVec_self_eq_of_submatrix {ι : Type u_5} {κ : Type u_6} {κ' : Type u_7} {S : Type u_9} [CommSemiring S] [Fintype ι] [Fintype κ] [Fintype κ'] {R : Matrix κ κ' S} {M : Matrix ι ι S} {f : κ → ι} {g : κ' → ι} (hf : Function.Injective f) (hg : Function.Injective g) (hMR : M.submatrix f g = R) (hM : ∀ (i j : ι), i ∉ Set.range f ∨ j ∉ Set.range g → M i j = 0) (v : ι → S) : v ⬝ᵥ M.mulVec v = v ∘ f ⬝ᵥ R.mulVec (v ∘ g)

A bilinear form as a quadratic form. If M carries R on the rows f and the columns g and vanishes elsewhere, the quadratic form of M at v is the bilinear form of R at the parts v ∘ f and v ∘ g.