Zero det of rank lt

Stream: Is there code for X?

[Martin Dvořák]

When a square matrix has nonmaximal rank, its determinant is 0.

Direct lemma does not exist.
Should I search for it through a notion of a singular matrix?
What is the definition I need?
I know IsUnit exists.

[Jireh Loreaux]

Together docs#Matrix.rank_of_isUnit, docs#Matrix.isUnit_iff_isUnit_det will show that if a matrix has nonmaximal rank, then the determinant is not a unit. If you want to get that the determinant is zero, you'll need to consider matrices over a field to use something like docs#isUnit_iff_ne_zero.

[Jireh Loreaux]

import Mathlib

variable {n 𝕜 : Type*} [Fintype n] [DecidableEq n] [Field 𝕜]

example (A : Matrix n n 𝕜) (hA: A.rank < Fintype.card n) : A.det = 0 := by
  contrapose hA
  rw [← ne_eq, ← isUnit_iff_ne_zero, ← Matrix.isUnit_iff_isUnit_det] at hA
  exact A.rank_of_isUnit hA |>.not_lt

[Jireh Loreaux]

As for how to find this. Note that you already had the first bit: docs#IsUnit, and you can use Loogle to find the rest for you.

First we link the rank to IsUnit: @loogle Matrix.rank, IsUnit

[loogle]

:search: Matrix.rank_of_isUnit, Matrix.rank_mul_eq_left_of_isUnit_det, and 1 more

[Jireh Loreaux]

Then we link the determinant to IsUnit: @loogle Matrix.det, IsUnit

[loogle]

:search: Matrix.isUnit_det_transpose, Matrix.nonsingInvUnit, and 59 more

[Jireh Loreaux]

Then we link the determinant being a unit to the nonzero condition: @loogle IsUnit, ?a ≠ 0

[loogle]

:search: IsUnit.ne_zero, IsUnit.mk0, and 75 more

[Martin Dvořák]

Should I PR your lemma so that future users don't have to go through the search?

[Junyan Xu]

variable {n 𝕜 : Type*} [Fintype n] [DecidableEq n] [Field 𝕜]
example (A : Matrix n n 𝕜) (hA: A.rank < Fintype.card n) : A.det = 0

This should still be true if 𝕜 is a domain because e.g. we can map the matrix into the FractionRing. The map is injective so if you get zero det over the field it's also zero over the domain. To see that this preserves the rank I see no easier way than to 1) consider the associated linear map, whose range has the same rank as the matrix; 2) use the existing results that the base change of the range is the range of the base-changed linear map (LinearMap.range_localizedMap_eq_localized₀_range), and that rank is preserved under (IsLocalizedModule.lift_rank_eq).

[Martin Dvořák]

Indeed, I will have to look into the generalization; ideally, I want to have the lemma for matrices over integers.

[Martin Dvořák]

Let's postpone the potential PR until we have the most general version.

[Floris van Doorn]

Can docs#Matrix.rank_of_isUnit (and the new lemma) be upgraded to an iff?

[Junyan Xu]

docs#Matrix.rank_of_isUnit cannot; consider the 1x1 matrix with the single entry 2 : ℤ. Its rank is 1 because the range of the associated linear map is 2ℤ which is isomorphic to ℤ and of rank 1, but its determinant is 2, which isn't a unit.

[Riccardo Brasca]

I have the impression that if the rank is not maximal then the determinant must be nilpotent, but I may be wrong.

[Riccardo Brasca]

There are criteria for surjectivity involving the ideal generated by all the minors iirc

[Eric Wieser]

Is it sufficient for the determinant to satisfy docs#IsRegular ?

[Kevin Buzzard]

I don't even know what "rank" means if you're not over a field.

[Junyan Xu]

It's defined to be the Module.rank of the range of the associated linear map. It especially makes sense over a PID, where every submodule of a finite free module is also free.

[Kevin Buzzard]

This is just the sort of daft thing we end up with in mathlib because people write definitions in the max generality for which it compiles. So the open questions in this thread (assuming the base is a commutative ring, my sanity won't let me go any lower) are: does det regular (ie not a zero divisor) imply full rank and does not-full rank imply nilpotent det? These can't both be right because in K[X,Y]/(XY) the element X is neither regular nor nilpotent but I'm about to get on a plane so can't think about this online any more. Is the 1*1 matrix (X) "full rank" or not? :-/

[Kevin Buzzard]

The geometric answer (ie the sensible answer) is "yes on one component of the scheme, no on the other"

[Antoine Chambert-Loir]

There is a determinantal criterion for injectivity— a square matrix is injective iff its determinant is regular. Is it in mathlib?
That will imply full rank.
But it is not a necessary assumption, in a product ring A x B, multiplication by (1, 0) has rank one (for A nonzero) but is neither injective nor surjective.

[Antoine Chambert-Loir]

The absolute rank of a module is not a good invariant, what makes more sense is the function on the spectrum, ranks of the tensor products with the various residual fields

[Junyan Xu]

Antoine Chambert-Loir said:

There is a determinantal criterion for injectivity— a square matrix is injective iff its determinant is regular. Is it in mathlib?
That will imply full rank.

To formalize this proof it looks like we will need #18771.

in a product ring A x B, multiplication by (1, 0) has rank one (for A nonzero) but is neither injective nor surjective.

I don't think it has rank one (according to Mathlib definition)? The only (A x B)-linearly independent subset contained in the range A x 0 is the empty set.

[Martin Dvořák]

I am a computer scientist, hence I naturally think about rank in terms of the Gaussian elimination.
It prevents me from seeing the more general things that could be there.

[Kevin Buzzard]

What's going on is that the Gaussian elimination algorithm involves division and all the discussion above is trying to make it work for rings, where division isn't in general defined.

[Eric Wieser]

Kevin Buzzard said:

assuming the base is a commutative ring, my sanity won't let me go any lower

Avery your eyes from #19581 then!