feat(data/matrix/rank): rank of Aᵀ ⬝ A and Aᴴ ⬝ A (#18818)

Since these results imply it trivially, this also includes lemmas about the rank of `Aᵀ` and `Aᴴ`.
However, these lemmas are not stated very generally, and are surely true in wider cases than the ones proven here.

src/data/matrix/rank.lean

@@ -1,11 +1,14 @@
 /-
 Copyright (c) 2021 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin
+Authors: Johan Commelin, Eric Wieer
 -/
 
 import linear_algebra.free_module.finite.rank
 import linear_algebra.matrix.to_lin
+import linear_algebra.finite_dimensional
+import linear_algebra.matrix.dot_product
+import data.complex.module
 
 /-!
 # Rank of matrices
@@ -19,7 +22,9 @@ This definition does not depend on the choice of basis, see `matrix.rank_eq_finr
 
 ## TODO
 
-* Show that `matrix.rank` is equal to the row-rank, and that `rank Aᵀ = rank A`.
+* Do a better job of generalizing over `ℚ`, `ℝ`, and `ℂ` in `matrix.rank_transpose` and
+  `matrix.rank_conj_transpose`. See
+  [this Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/row.20rank.20equals.20column.20rank/near/350462992).
 
 -/
 
@@ -30,6 +35,8 @@ namespace matrix
 open finite_dimensional
 
 variables {l m n o R : Type*} [m_fin : fintype m] [fintype n] [fintype o]
+
+section comm_ring
 variables [comm_ring R]
 
 /-- The rank of a matrix is the rank of its image. -/
@@ -98,8 +105,7 @@ begin
   rw [rank, rank, mul_vec_lin_submatrix, linear_map.range_comp, linear_map.range_comp,
     (show linear_map.fun_left R R e.symm = linear_equiv.fun_congr_left R R e.symm, from rfl),
     linear_equiv.range, submodule.map_top],
-  -- TODO: generalize `finite_dimensional.finrank_map_le` and use it here
-  exact finrank_le_finrank_of_rank_le_rank (lift_rank_map_le _ _) (rank_lt_aleph_0 _ _),
+  exact submodule.finrank_map_le _ _,
 end
 
 lemma rank_reindex [fintype m] (e₁ e₂ : m ≃ n) (A : matrix m m R) :
@@ -154,4 +160,110 @@ lemma rank_eq_finrank_span_cols (A : matrix m n R) :
   A.rank = finrank R (submodule.span R (set.range Aᵀ)) :=
 by rw [rank, matrix.range_mul_vec_lin]
 
+end comm_ring
+
+/-! ### Lemmas about transpose and conjugate transpose
+
+This section contains lemmas about the rank of `matrix.transpose` and `matrix.conj_transpose`.
+
+Unfortunately the proofs are essentially duplicated between the two; `ℚ` is a linearly-ordered ring
+but can't be a star-ordered ring, while `ℂ` is star-ordered (with `open_locale complex_order`) but
+not linearly ordered. For now we don't prove the transpose case for `ℂ`.
+
+TODO: the lemmas `matrix.rank_transpose` and `matrix.rank_conj_transpose` current follow a short
+proof that is a simple consequence of `matrix.rank_transpose_mul_self` and
+`matrix.rank_conj_transpose_mul_self`. This proof pulls in unecessary assumptions on `R`, and should
+be replaced with a proof that uses Gaussian reduction or argues via linear combinations.
+-/
+
+section star_ordered_field
+variables [fintype m] [field R] [partial_order R] [star_ordered_ring R]
+
+lemma ker_mul_vec_lin_conj_transpose_mul_self (A : matrix m n R) :
+  linear_map.ker (Aᴴ ⬝ A).mul_vec_lin = linear_map.ker (mul_vec_lin A):=
+begin
+  ext x,
+  simp only [linear_map.mem_ker, mul_vec_lin_apply, ←mul_vec_mul_vec],
+  split,
+  { intro h,
+    replace h := congr_arg (dot_product (star x)) h,
+    rwa [dot_product_mul_vec, dot_product_zero, vec_mul_conj_transpose, star_star,
+      dot_product_star_self_eq_zero] at h },
+  { intro h, rw [h, mul_vec_zero] },
+end
+
+lemma rank_conj_transpose_mul_self (A : matrix m n R) :
+  (Aᴴ ⬝ A).rank = A.rank :=
+begin
+  dunfold rank,
+  refine add_left_injective (finrank R (A.mul_vec_lin).ker) _,
+  dsimp only,
+  rw [linear_map.finrank_range_add_finrank_ker,
+    ←((Aᴴ ⬝ A).mul_vec_lin).finrank_range_add_finrank_ker],
+  congr' 1,
+  rw ker_mul_vec_lin_conj_transpose_mul_self,
+end
+
+-- this follows the proof here https://math.stackexchange.com/a/81903/1896
+/-- TODO: prove this in greater generality. -/
+@[simp] lemma rank_conj_transpose (A : matrix m n R) : Aᴴ.rank = A.rank :=
+le_antisymm
+  (((rank_conj_transpose_mul_self _).symm.trans_le $ rank_mul_le_left _ _).trans_eq $
+    congr_arg _ $ conj_transpose_conj_transpose _)
+  ((rank_conj_transpose_mul_self _).symm.trans_le $ rank_mul_le_left _ _)
+
+@[simp] lemma rank_self_mul_conj_transpose (A : matrix m n R) : (A ⬝ Aᴴ).rank = A.rank :=
+by simpa only [rank_conj_transpose, conj_transpose_conj_transpose]
+  using rank_conj_transpose_mul_self Aᴴ
+
+end star_ordered_field
+
+section linear_ordered_field
+variables [fintype m] [linear_ordered_field R]
+
+lemma ker_mul_vec_lin_transpose_mul_self  (A : matrix m n R) :
+  linear_map.ker (Aᵀ ⬝ A).mul_vec_lin = linear_map.ker (mul_vec_lin A):=
+begin
+  ext x,
+  simp only [linear_map.mem_ker, mul_vec_lin_apply, ←mul_vec_mul_vec],
+  split,
+  { intro h,
+    replace h := congr_arg (dot_product x) h,
+    rwa [dot_product_mul_vec, dot_product_zero, vec_mul_transpose,
+      dot_product_self_eq_zero] at h },
+  { intro h, rw [h, mul_vec_zero] },
+end
+
+lemma rank_transpose_mul_self (A : matrix m n R) : (Aᵀ ⬝ A).rank = A.rank :=
+begin
+  dunfold rank,
+  refine add_left_injective (finrank R (A.mul_vec_lin).ker) _,
+  dsimp only,
+  rw [linear_map.finrank_range_add_finrank_ker,
+    ←((Aᵀ ⬝ A).mul_vec_lin).finrank_range_add_finrank_ker],
+  congr' 1,
+  rw ker_mul_vec_lin_transpose_mul_self,
+end
+
+/-- TODO: prove this in greater generality. -/
+@[simp] lemma rank_transpose (A : matrix m n R) : Aᵀ.rank = A.rank :=
+le_antisymm
+  ((rank_transpose_mul_self _).symm.trans_le $ rank_mul_le_left _ _)
+  ((rank_transpose_mul_self _).symm.trans_le $ rank_mul_le_left _ _)
+
+@[simp] lemma rank_self_mul_transpose (A : matrix m n R) : (A ⬝ Aᵀ).rank = A.rank :=
+by simpa only [rank_transpose, transpose_transpose] using rank_transpose_mul_self Aᵀ
+
+end linear_ordered_field
+
+/-- The rank of a matrix is the rank of the space spanned by its rows.
+
+TODO: prove this in a generality that works for `ℂ` too, not just `ℚ` and `ℝ`. -/
+lemma rank_eq_finrank_span_row [linear_ordered_field R] [finite m] (A : matrix m n R) :
+  A.rank = finrank R (submodule.span R (set.range A)) :=
+begin
+  casesI nonempty_fintype m,
+  rw [←rank_transpose, rank_eq_finrank_span_cols, transpose_transpose]
+end
+
 end matrix