feat(data/matrix/rank): rank of multiplication (#18784)

This adds a universe-polymorphic version of `rank_comp_le_right`, and then uses it to show `(A ⬝ B).rank ≤ B.rank`; previously we only had `(A ⬝ B).rank ≤ A.rank`.

For convenience, this adds the spellings `(A ⬝ B).rank ≤ min A.rank B.rank` and `rank (f.comp g) ≤ min (rank f) (rank g)`, as these map well to the way that rank would be described in words.

src/data/matrix/rank.lean

@@ -29,7 +29,7 @@ namespace matrix
 
 open finite_dimensional
 
-variables {m n o R : Type*} [m_fin : fintype m] [fintype n] [fintype o]
+variables {l m n o R : Type*} [m_fin : fintype m] [fintype n] [fintype o]
 variables [decidable_eq n] [decidable_eq o] [comm_ring R]
 
 /-- The rank of a matrix is the rank of its image. -/
@@ -52,19 +52,36 @@ lemma rank_le_width [strong_rank_condition R] {m n : ℕ} (A : matrix (fin m) (f
   A.rank ≤ n :=
 A.rank_le_card_width.trans $ (fintype.card_fin n).le
 
-lemma rank_mul_le [strong_rank_condition R] (A : matrix m n R) (B : matrix n o R) :
+lemma rank_mul_le_left [strong_rank_condition R] (A : matrix m n R) (B : matrix n o R) :
   (A ⬝ B).rank ≤ A.rank :=
 begin
   rw [rank, rank, to_lin'_mul],
   exact cardinal.to_nat_le_of_le_of_lt_aleph_0
     (rank_lt_aleph_0 _ _) (linear_map.rank_comp_le_left _ _),
 end
 
+include m_fin
+
+lemma rank_mul_le_right [strong_rank_condition R] (A : matrix l m R) (B : matrix m n R) :
+  (A ⬝ B).rank ≤ B.rank :=
+begin
+  letI := classical.dec_eq m,
+  rw [rank, rank, to_lin'_mul],
+  exact finrank_le_finrank_of_rank_le_rank
+    (linear_map.lift_rank_comp_le_right B.to_lin' A.to_lin') (rank_lt_aleph_0 _ _),
+end
+
+omit m_fin
+
+lemma rank_mul_le [strong_rank_condition R] (A : matrix m n R) (B : matrix n o R) :
+  (A ⬝ B).rank ≤ min A.rank B.rank :=
+le_min (rank_mul_le_left _ _) (rank_mul_le_right _ _)
+
 lemma rank_unit [strong_rank_condition R] (A : (matrix n n R)ˣ) :
   (A : matrix n n R).rank = fintype.card n :=
 begin
   refine le_antisymm (rank_le_card_width A) _,
-  have := rank_mul_le (A : matrix n n R) (↑A⁻¹ : matrix n n R),
+  have := rank_mul_le_left (A : matrix n n R) (↑A⁻¹ : matrix n n R),
   rwa [← mul_eq_mul, ← units.coe_mul, mul_inv_self, units.coe_one, rank_one] at this,
 end
 

src/linear_algebra/dimension.lean

@@ -1344,10 +1344,27 @@ begin
   exact linear_map.map_le_range,
 end
 
+lemma lift_rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
+  cardinal.lift.{v'} (rank (f.comp g)) ≤ cardinal.lift.{v''} (rank g) :=
+by rw [rank, rank, linear_map.range_comp]; exact lift_rank_map_le _ _
+
+/-- The rank of the composition of two maps is less than the minimum of their ranks. -/
+lemma lift_rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
+  cardinal.lift.{v'} (rank (f.comp g)) ≤
+    min (cardinal.lift.{v'} (rank f)) (cardinal.lift.{v''} (rank g)) :=
+le_min (cardinal.lift_le.mpr $ rank_comp_le_left _ _) (lift_rank_comp_le_right _ _)
+
 variables [add_comm_group V'₁] [module K V'₁]
 
 lemma rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) : rank (f.comp g) ≤ rank g :=
-by rw [rank, rank, linear_map.range_comp]; exact rank_map_le _ _
+by simpa only [cardinal.lift_id] using lift_rank_comp_le_right g f
+
+/-- The rank of the composition of two maps is less than the minimum of their ranks.
+
+See `lift_rank_comp_le` for the universe-polymorphic version. -/
+lemma rank_comp_le (g : V →ₗ[K] V') (f : V' →ₗ[K] V'₁) :
+  rank (f.comp g) ≤ min (rank f) (rank g) :=
+by simpa only [cardinal.lift_id] using lift_rank_comp_le g f
 
 end ring