Zero rank iff zero matrix

Stream: Is there code for X?

[MohanadAhmed]

Is there a lemma in mathlib saying that a finite dimensional matrix has rank zero iff and only if it is the zero matrix?

One direction is provided by docs#matrix.rank_zero . After some futile searching I though I would try to prove it on my own but I am stuck?
It seems a module with rank zero is both a zero dimension space and an inifinite dimensional space!!!
What am a I missing? Any thoughts on how to finish this one?

import data.complex.basic
import linear_algebra.std_basis
import data.matrix.basic
import data.matrix.rank
import data.fin.tuple.sort

open matrix
open complex
open_locale matrix big_operators

theorem matrix.rank_zero_iff_eq_zero {m : Type*} {n : Type*} {R : Type*}
  [fintype n][fintype m] [field R] [nontrivial R] {A: matrix m n R} :
    A = 0 ↔ A.rank = 0 :=
begin
  split,
  intro h, rw [h, matrix.rank_zero],
  intro h,

  -- rw matrix.rank at h,
  -- have rnt := (linear_map.finrank_range_add_finrank_ker (matrix.mul_vec_lin A)),
  -- rw [h, zero_add, finite_dimensional.finrank_fintype_fun_eq_card] at rnt,

  rw matrix.rank at h,
  rw finite_dimensional.finrank at h,
  sorry {rw cardinal.to_nat_cast,},
  -- rank_eq_zero
  -- linear_map.range_eq_bot
end

[Eric Rodriguez]

docs#linear_map.range_eq_bot?

[Eric Rodriguez]

and then maybe go through the to_lin machinery

[Eric Rodriguez]

never mind, I'm no longer sure if this si even true
I forgot how empty functionsworked

[Eric Wieser]

docs#finrank_eq_zero looks like it should do most of the work

[MohanadAhmed]

Yeah I was hoping to use that lemma (the commented out bit!) but I don't know how to tell lean: "if range has rank zero, then the linear map is bot"?

The state after rw matrix.rank at h is

  /-
  m : Type u_1,
  n : Type u_2,
  R : Type u_3,
  _inst_1 : fintype n,
  _inst_2 : fintype m,
  _inst_3 : field R,
  _inst_4 : nontrivial R,
  A : matrix m n R,
  h : finite_dimensional.finrank R ↥(linear_map.range A.mul_vec_lin) = 0
  ⊢ A = 0
  -/

[MohanadAhmed]

Eric Wieser said:

docs#finrank_eq_zero looks like it should do most of the work

Yeah that one is for some reason not working!!

[Eric Wieser]

What goes wrong?

[Eric Rodriguez]

you may need to throw in a classical

[MohanadAhmed]

Eric Wieser said:

What goes wrong?

Something like cannot find instance. I will retry it and post the exact thing?

[MohanadAhmed]

Seems I was missing the [decidable_eq m] and [decidale_eq n]. I am not sure if that is the reason. But this seems to work now:
Thanks @Eric Wieser and @Eric Rodriguez

import data.complex.basic
import linear_algebra.std_basis
import data.matrix.basic
import data.matrix.rank
import data.fin.tuple.sort
import algebra.module.linear_map

open matrix
open complex
open_locale matrix big_operators

lemma range_zero_mat_zero {m n R: Type*}
  [fintype n][fintype m][decidable_eq m][decidable_eq n]
  [comm_ring R] [nontrivial R] {A: matrix m n R} :
  (∀ x, A.mul_vec x = 0) → A = 0 :=
begin
  intro h,
  funext x y, rw [pi.zero_apply,pi.zero_apply],
  let z := λ i, ite (i = y) (1:R) 0,

  specialize h z,
  rw function.funext_iff at h,
  specialize h x,
  simp_rw [mul_vec, dot_product, z, mul_boole, finset.sum_ite_eq',
    finset.mem_univ, if_true, pi.zero_apply] at h,
  exact h,
end

theorem matrix.rank_zero_iff_eq_zero {m n: Type*}  {R : Type*}
  [fintype n][fintype m][decidable_eq m][decidable_eq n]
  [field R] [nontrivial R] {A: matrix m n R} :
    A = 0 ↔ A.rank = 0 :=
begin
  split,
  intro h, rw [h, matrix.rank_zero],
  intro h,
  rw [matrix.rank, finrank_eq_zero, linear_map.range_eq_bot, linear_map.ext_iff] at h,
  simp_rw mul_vec_lin_apply at h,
  apply range_zero_mat_zero h,
end

[Eric Wieser]

I'm pretty sure at already have that first lemma

[MohanadAhmed]

You mean in mathlib?

[MohanadAhmed]

Can you guess any name?

[MohanadAhmed]

I tried looking but I admit my mathlib search-fu is quite weak :joy:

[Eric Wieser]

No, but you should be able to avoid it entirely by using docs#map_eq_zero_iff on to_lin which is a linear equivalence

[Yury G. Kudryashov]

finrank_eq_zero needs division_ring. Why?

[Yury G. Kudryashov]

Is it for historical reasons or there is a counterexample?

[Yury G. Kudryashov]

docs#rank_eq_zero needs division_ring too.

[Eric Wieser]

It could easily just be historical

[Yury G. Kudryashov]

I'm trying to generalize.

[Eric Wieser]

It might be best to leave that till the port is done

[Eric Wieser]

I did as many generalizations here as I could in the week or two before the port caught up with the dimension files

[Eric Wieser]

I think there's likely to be a counterexample for semirings because our linear_independent is nonsense there

[Yury G. Kudryashov]

I'm looking into it.

[Yury G. Kudryashov]

I'll post what I find later tonight.

[MohanadAhmed]

that might be one of the things I was messing up. At some point I was using comm_ring R that might have made finrank_eq_zero not work before I switched to fields

[MohanadAhmed]

A comm_ring is not a division_ring right?

[Yury G. Kudryashov]

A counterexample (for module.rank_eq_zero over rings): the rank of zmod 5 as a module over int is 0. NO

[Yury G. Kudryashov]

We need docs#no_zero_smul_divisors UPD: if we don't have that, then we need injective (λ c, c • x) instead of x ≠ 0.

[Yury G. Kudryashov]

I guess, you can have a counterexample to your statement about matrices for R = zmod 10. UPD: not sure anymore but you can try. Both singletons {2} and {5} in zmod 10 are not linear independent over zmod 10.

[Yury G. Kudryashov]

docs#rank_zero_iff or docs#rank_zero_iff_forall_zero should help you a lot.

[Yury G. Kudryashov]

They have weaker assumptions. I don't want to generalize more results about module.rank before the port is over.