row rank equals column rank

Stream: maths

[Kevin Buzzard]

@Eric Wieser nerdsniped me into thinking about in what generality "row rank of a matrix equals column rank" is true. We have docs#matrix.rank for general commutative rings and (A : matrix m n R) : Aᵀ.rank = A.rank makes sense for m and n both fintypes.

So whatever is the rank of a matrix over a commutative ring $R$? It's defined to be the rank of the image of the corresponding linear map, which is a finitely-generated $R$-module. If $R=0$ then there's only one finitely-generated $R$-module so it's true in this case. For $R$ nonzero, the rank $r(M)$ of an $R$-module $M$ is defined to be the sup of the ranks of the free submodules of $M$. If $M\to N$ is injective then $r(M)\leq r(N)$ (obvious) and if $M\to N$ is surjective then $r(M)\geq r(N)$ (you can lift a free submodule of $N$ back to $M$ by lifting generators), so at least $r$ isn't completely pathological, and in particular the rank of an $R$-module which is generated by $d$ elements is at most $d$. But for general $R$ this is pretty much all one can say; rank is not additive even for direct sums, for example (if $R=A\oplus B$ is the sum of two fields then $r(A)=r(B)=0$ but $r(R)=1$).

This definition of rank was basically invented by the mathlib community, I think, and doesn't seem to be in the literature (perhaps because it's so poorly-behaved). If $R$ is an integral domain then the definition is in the literature and the function is better-behaved. Here is what I think should be a proof of row rank = column rank for integral domains: first show that if $K$ is the field of fractions of $R$ then $r_R(M)=r_K(K\otimes_RM)$ which reduces the question to fields and then for fields it's a standard result (proof by elementary row operations or whatever). I assume the equality is true. Perhaps one route (probably not the shortest) to it would be to first show that if $R\to S$ is an injection of commutative rings and $M$ is an $S$-module then $r_R(M)=r_S(M)$; this would follow from the facts that if $S^d\subseteq M$ then obviously $R^d\subseteq M$, and conversely if $R^d\subseteq M$ then I am assuming one can use a basis to get $S^d\subseteq M$ although I don't immediately see why the map is injective. Then one could presumably show that $r_R(M)=r_R(M\otimes_RK)$ for $R$ an integral domain and $K$ its field of fractions. I should say that I have checked none of this and am just going by intuition, which might be wrong.

[Kevin Buzzard]

As I say, I think that for $R$ not an integral domain, our definition is not in the literature. What is in the literature is the function on $X:=\mathrm{Spec}(R)$ sending a prime ideal $P$ to the $R_P/PR_P$-dimension of $M_P/PM_P$. For $R$ reduced, our rank function might be the min of this function on $X$, although unfortunately this does not seem to be true in general; for example if $R=\Z/p^2\Z$ for $p$ prime, or $R=\mathbb{C}[\epsilon]/(\epsilon^2)$ then $R$ is local with maximal ideal $m$ and $r_R(R/m)=0$, whereas the function in the literature takes the value 1. So if one were to approach the question via the standard alegebraic geometry "reduction" techniques (which I've already hinted at, by suggesting that the result can be proved for integral domains given that it's true for fields) then one has to get around this hurdle somehow. If it's true that for $R\subseteq S$ then $r_R(M)=r_S(M\otimes_RS)$ then I guess one can reduce to the Noetherian case; I then don't know how to reduce to the case where $R$ is reduced, but once you're there then maybe our function is the min of the function on $X$ and then perhaps one can prove the general case (if it's true) by arguing on points.

[Eric Wieser]

(for reference, #18818 has a proof of the titular fact, but under fairly unreasonable requirements; though I suggest we don't discuss that PR here)

[Eric Wieser]

There some more discussion of ranks here

[Praneeth Kolichala]

The PR seems to suggest that proving row rank = column rank would require Gaussian elimination, but at least for fields, we seem to already have the result in docs#linear_map.finrank_range_dual_map_eq_finrank_range. It's fairly straightforward to combine that with docs#matrix.to_lin_transpose to get the desired result for matrices:

theorem matrix.rank_transpose' {𝕜 i j : Type*}
  [field 𝕜] [fintype i] [fintype j] (m : matrix i j 𝕜) :
  m.transpose.rank = m.rank :=
begin
  classical,
  rw [m.transpose.rank_eq_finrank_range_to_lin (pi.basis_fun 𝕜 j).dual_basis (pi.basis_fun 𝕜 i).dual_basis,
      matrix.to_lin_transpose, ← linear_map.dual_map_def, linear_map.finrank_range_dual_map_eq_finrank_range, matrix.to_lin_eq_to_lin',
      matrix.to_lin'_apply', matrix.rank],
end

(Note: I'm not sure why docs#matrix.to_lin_transpose states the result using docs#module.dual.transpose instead of docs#linear_map.dual_map. Why even bother having the latter if lemma statements will use transpose f instead of f.dual_map?)

This would at least prove the "standard undergrad" version of the result, and is useful for the many times when you have to do linear algebra over a finite field in TCS.

[Eric Wieser]

(docs#matrix.rank_transpose for comparison)

[Eric Wieser]

I assume you meant docs#module.dual.transpose not matrix.dual.transpose