Rank of Matrix Multiplied by an Invertible Matrix

Stream: Is there code for X?

[MohanadAhmed]

Let $A$ and $B$ be two matrices, with A being invertible. The rank of $B$ is not affected by pre or post multiplication by $A$. Is there code for this in mathlib? (or Mathlib4)

$\text{invertible} A \implies \text{rank}({AB}) = \text{rank}({BA}) = \text{rank}({B})$

[Eric Wieser]

I don't think we have it, but it should follow without too much work either from docs#matrix.rank_mul_le_left, or by proving it about linear_equiv first then using matrix.to_lin

[MohanadAhmed]

I have a proof that seems like a lot more work than what you suggest. Any tips?

import data.complex.basic
import linear_algebra.matrix.nonsingular_inverse
import data.matrix.rank

variables {m n R: Type*}
variables [fintype m][fintype n][decidable_eq m][decidable_eq n]
variables [field R][decidable_eq R]

open matrix
open_locale matrix

lemma rank_mul_unit (A: matrix n n R)(B: matrix m n R) (hA: is_unit A.det):
  (B⬝A).rank = B.rank := begin
  rw [matrix.rank, mul_vec_lin_mul, linear_map.range_comp_of_range_eq_top, ← matrix.rank],
  rw linear_map.range_eq_top,
  intro x,
  use ((A⁻¹).mul_vec_lin ) x,
  rwa [mul_vec_lin_apply, mul_vec_lin_apply, mul_vec_mul_vec, mul_nonsing_inv, one_mul_vec],
end

lemma rank_mul_unit' (A: matrix m m R)(B: matrix m n R) (hA: is_unit A.det):
  (A⬝B).rank = B.rank := begin
  have h: linear_map.ker ((A⬝B).mul_vec_lin) = linear_map.ker (B.mul_vec_lin) ,
  { rw [mul_vec_lin_mul, linear_map.ker_comp_of_ker_eq_bot],
    rw linear_map.ker_eq_bot,
    simp_rw [function.injective, mul_vec_lin_apply],
    intros x y h,
    replace h := congr_arg (λ x, matrix.mul_vec (A⁻¹) x)  h,
    simp_rw [mul_vec_mul_vec, nonsing_inv_mul A hA, one_mul_vec] at h,
    exact h, },
  have hB := linear_map.finrank_range_add_finrank_ker ((B).mul_vec_lin),
  rw [← linear_map.finrank_range_add_finrank_ker ((A⬝B).mul_vec_lin), h, add_left_inj] at hB,
  rw [matrix.rank, matrix.rank, hB],
end

[Eric Wieser]

Apply matrix.rank_mul_le_left twice and use antisymmetry?

[MohanadAhmed]

Related Question:
Islinear_ordered_field needed in rank_transpose, rank_transpose_mul_self?

[Eric Wieser]

No and maybe

[Eric Wieser]

There's another thread with a better proof of rank_transpose

[Eric Wieser]

rank_transpose_self is going to need @Jireh Loreaux's refactor of star_ordered_ring

[Damiano Testa]

MohanadAhmed said:

Related Question:
Islinear_ordered_field needed in rank_transpose, rank_transpose_mul_self?

Over $\mathbb{C}$, the matrix $\begin{pmatrix}1 & i \cr i & -1 \end{pmatrix}$ is symmetric and its square is zero. The rank goes from 1 to 0, so some assumption on the field is needed.

[Damiano Testa]

I think that Eric is referring to this proof.

With rank_transpose' from the previous link, you can prove rank_mul_unit' as follows:

lemma rank_mul_unit' (A: matrix m m R) (B: matrix m n R) (hA: is_unit A.det) :
  (A⬝B).rank = B.rank :=
begin
  rw [← matrix.rank_transpose' B, ← matrix.rank_transpose' (A ⬝ B), transpose_mul],
  apply rank_mul_unit,
  rwa det_transpose,
end

[MohanadAhmed]

Eric Wieser said:

rank_transpose_self is going to need Jireh Loreaux's refactor of star_ordered_ring

For Future Ref:

• The Refactor Eric is Referring to: Pull Request 18854
• The Zulip thread containing the Star Ordered Ring refactor discussion .
• Another related thread about rank_transpose a.k.a column rank equal row rank.