Ranks of blocks over GF(2) #
Elementary facts about Correlation.blockRank, the dimension of the row space of a block:
it grows with the block, it drops by at most one per deleted row, it is invariant under
transposition and injective relabelling of rows and columns, and two blocks whose rows live
on disjoint sets of columns contribute their ranks additively.
theorem
Complexity.Correlation.span_blockRows_eq_map
{ι : Type u_1}
{κ : Type u_2}
{M : Matrix ι κ (ZMod 2)}
(S : Set ι)
{T T' : Set κ}
(h : T' ⊆ T)
:
Submodule.span (ZMod 2) (Set.range (blockRows M S T')) = Submodule.map (LinearMap.funLeft (ZMod 2) (ZMod 2) (Set.inclusion h))
(Submodule.span (ZMod 2) (Set.range (blockRows M S T)))
Restricting the columns of a block maps its row space onto the smaller row space.
theorem
Complexity.Correlation.blockRank_comp
{ι : Type u_1}
{κ : Type u_2}
{ι' : Type u_3}
{κ' : Type u_4}
(M : Matrix ι κ (ZMod 2))
{f : ι' → ι}
{g : κ' → κ}
(hf : Function.Injective f)
(hg : Function.Injective g)
(S : Set ι')
(T : Set κ')
:
Relabelling the rows and columns injectively does not change the rank of a block.
theorem
Complexity.Correlation.add_blockRank_le_of_disjoint
{ι : Type u_1}
{κ : Type u_2}
[Finite κ]
(M : Matrix ι κ (ZMod 2))
{S S₁ S₂ : Set ι}
{T T₁ T₂ : Set κ}
(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)
:
Blocks on disjoint columns. If, among the columns T, the rows of S₁ vanish outside
T₁ and the rows of S₂ vanish outside T₂, with T₁ and T₂ disjoint, then the rank of the
block S × T is at least the sum of the ranks of S₁ × T and S₂ × T.