refactor(LinearAlgebra/Matrix/Rank): generalize Matrix.rank/LinearMap.rank to semirings (leanprover-community#39158)

- Generalize `Matrix.rank` from `CommRing` to `CommSemiring`
- Generalize `LinearMap.rank` from `AddCommGroup`s over `Ring`s to `AddCommMonoid`s over `Semiring`s (which are the minimum requirements for `Module`)
- Many `Matrix.rank` theorems now require `StrongRankCondition` explicitly (which `CommRing` used to provide)
- `Matrix.cRank` theorems don't need commutativity

Author: SnirBroshi

Mathlib/LinearAlgebra/Dimension/LinearMap.lean

@@ -31,8 +31,8 @@ namespace LinearMap
 
 section Ring
 
-variable [Ring K] [AddCommGroup V] [Module K V] [AddCommGroup V₁] [Module K V₁]
-variable [AddCommGroup V'] [Module K V']
+variable [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid V₁] [Module K V₁]
+variable [AddCommMonoid V'] [Module K V']
 
 /-- `rank f` is the rank of a `LinearMap` `f`, defined as the dimension of `f.range`. -/
 abbrev rank (f : V →ₗ[K] V') : Cardinal :=
@@ -48,7 +48,7 @@ theorem rank_le_domain (f : V →ₗ[K] V₁) : rank f ≤ Module.rank K V :=
 theorem rank_zero [Nontrivial K] : rank (0 : V →ₗ[K] V') = 0 := by
   rw [rank, LinearMap.range_zero, rank_bot]
 
-variable [AddCommGroup V''] [Module K V'']
+variable [AddCommMonoid V''] [Module K V'']
 
 theorem rank_comp_le_left (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') : rank (f.comp g) ≤ rank f := by
   refine Submodule.rank_mono ?_

Mathlib/LinearAlgebra/Matrix/Rank.lean

@@ -114,97 +114,93 @@ end Infinite
 
 variable [Fintype n] [Fintype o]
 
-section CommRing
-
-variable [CommRing R]
-
 /-- The rank of a matrix is the rank of its image. -/
-noncomputable def rank (A : Matrix m n R) : ℕ :=
+noncomputable def rank [CommSemiring R] (A : Matrix m n R) : ℕ :=
   finrank R <| LinearMap.range A.mulVecLin
 
 @[simp]
-theorem rank_subsingleton [Subsingleton R] (A : Matrix m n R) : A.rank = 1 :=
+theorem rank_subsingleton [CommSemiring R] [Subsingleton R] (A : Matrix m n R) : A.rank = 1 :=
   finrank_subsingleton
 
 @[simp]
-theorem cRank_one [Nontrivial R] [DecidableEq m] :
+theorem cRank_one [Semiring R] [Nontrivial R] [DecidableEq m] [StrongRankCondition R] :
     (cRank (1 : Matrix m m R)) = lift.{uR} #m := by
   have h : LinearIndependent R (1 : Matrix m m R)ᵀ := by
     convert! Pi.linearIndependent_single_one m R
     simp [funext_iff, Matrix.one_eq_pi_single]
   rw [cRank, rank_span h, ← lift_umax, ← Cardinal.mk_range_eq_of_injective h.injective, lift_id']
 
-@[simp] theorem eRank_one [Nontrivial R] [DecidableEq m] :
+@[simp] theorem eRank_one [Semiring R] [Nontrivial R] [DecidableEq m] [StrongRankCondition R] :
     (eRank (1 : Matrix m m R)) = ENat.card m := by
   rw [eRank, cRank_one, toENat_lift, ENat.card]
 
 @[simp]
-theorem rank_one [Nontrivial R] [DecidableEq n] :
+theorem rank_one [CommSemiring R] [DecidableEq n] [StrongRankCondition R] :
     rank (1 : Matrix n n R) = Fintype.card n := by
   rw [rank, mulVecLin_one, LinearMap.range_id, finrank_top, finrank_pi]
 
 @[simp]
-theorem rank_zero [Nontrivial R] : rank (0 : Matrix m n R) = 0 := by
+theorem rank_zero [CommSemiring R] [Nontrivial R] : rank (0 : Matrix m n R) = 0 := by
   rw [rank, mulVecLin_zero, LinearMap.range_zero, finrank_bot]
 
 set_option backward.isDefEq.respectTransparency false in
 @[simp]
-theorem cRank_zero {m n : Type*} [Nontrivial R] : cRank (0 : Matrix m n R) = 0 := by
+theorem cRank_zero {m n : Type*} [Semiring R] [Nontrivial R] : cRank (0 : Matrix m n R) = 0 := by
   obtain hn | hn := isEmpty_or_nonempty n
   · rw [cRank, range_eq_empty, span_empty, rank_bot]
   rw [cRank, transpose_zero, range_zero, span_zero_singleton, rank_bot]
 
 @[simp]
-theorem eRank_zero {m n : Type*} [Nontrivial R] : eRank (0 : Matrix m n R) = 0 := by
+theorem eRank_zero {m n : Type*} [Semiring R] [Nontrivial R] : eRank (0 : Matrix m n R) = 0 := by
   simp [eRank]
 
-theorem rank_le_card_width [Nontrivial R] (A : Matrix m n R) :
-    A.rank ≤ Fintype.card n := by
-  exact A.mulVecLin.finrank_range_le.trans_eq (finrank_pi _)
+theorem rank_le_card_width [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R) :
+    A.rank ≤ Fintype.card n :=
+  A.mulVecLin.finrank_range_le.trans_eq <| finrank_pi R
 
-theorem rank_le_width [Nontrivial R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) :
-    A.rank ≤ n :=
+theorem rank_le_width [CommSemiring R] [StrongRankCondition R] {m n : ℕ}
+    (A : Matrix (Fin m) (Fin n) R) : A.rank ≤ n :=
   A.rank_le_card_width.trans <| (Fintype.card_fin n).le
 
-theorem rank_mul_le_left (A : Matrix m n R) (B : Matrix n o R) :
-    (A * B).rank ≤ A.rank := by
+theorem rank_mul_le_left [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R)
+    (B : Matrix n o R) : (A * B).rank ≤ A.rank := by
   nontriviality R
   rw [rank, rank, mulVecLin_mul]
-  exact Cardinal.toNat_le_toNat (LinearMap.rank_comp_le_left _ _) (rank_lt_aleph0 _ _)
+  exact Cardinal.toNat_le_toNat (LinearMap.rank_comp_le_left ..) (rank_lt_aleph0 R _)
 
-theorem rank_mul_le_right (A : Matrix m n R) (B : Matrix n o R) :
-    (A * B).rank ≤ B.rank := by
+theorem rank_mul_le_right [CommSemiring R] [StrongRankCondition R] (A : Matrix m n R)
+    (B : Matrix n o R) : (A * B).rank ≤ B.rank := by
   nontriviality R
   rw [rank, rank, mulVecLin_mul]
   exact finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _)
     (rank_lt_aleph0 _ _)
 
-theorem rank_mul_le (A : Matrix m n R) (B : Matrix n o R) :
+theorem rank_mul_le [CommSemiring R] [StrongRankCondition 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 _ _)
 
-theorem rank_vecMulVec_le (w : m → R) (v : n → R) : (Matrix.vecMulVec w v).rank ≤ 1 := by
+theorem rank_vecMulVec_le [CommSemiring R] [StrongRankCondition R] (w : m → R) (v : n → R) :
+    (Matrix.vecMulVec w v).rank ≤ 1 := by
   rw [Matrix.vecMulVec_eq Unit]
   refine le_trans (rank_mul_le_left _ _) ?_
   nontriviality R
   exact rank_le_card_width _
 
-theorem rank_unit [Nontrivial R] [DecidableEq n] (A : (Matrix n n R)ˣ) :
+theorem rank_unit [DecidableEq n] [CommSemiring R] [StrongRankCondition R] (A : (Matrix n n R)ˣ) :
     (A : Matrix n n R).rank = Fintype.card n := by
   apply le_antisymm (rank_le_card_width (A : Matrix n n R)) _
   have := rank_mul_le_left (A : Matrix n n R) (↑A⁻¹ : Matrix n n R)
   rwa [← Units.val_mul, mul_inv_cancel, Units.val_one, rank_one] at this
 
-theorem rank_of_isUnit [Nontrivial R] [DecidableEq n] (A : Matrix n n R) (h : IsUnit A) :
-    A.rank = Fintype.card n := by
+theorem rank_of_isUnit [DecidableEq n] [CommSemiring R] [StrongRankCondition R] (A : Matrix n n R)
+    (h : IsUnit A) : A.rank = Fintype.card n := by
   obtain ⟨A, rfl⟩ := h
   exact rank_unit A
 
 /-- Right multiplying by an invertible matrix does not change the rank -/
 @[simp]
-lemma rank_mul_eq_left_of_isUnit_det [DecidableEq n]
-    (A : Matrix n n R) (B : Matrix m n R) (hA : IsUnit A.det) :
-    (B * A).rank = B.rank := by
+lemma rank_mul_eq_left_of_isUnit_det {R : Type*} [CommRing R] [DecidableEq n] (A : Matrix n n R)
+    (B : Matrix m n R) (hA : IsUnit A.det) : (B * A).rank = B.rank := by
   suffices Function.Surjective A.mulVecLin by
     rw [rank, mulVecLin_mul, LinearMap.range_comp_of_range_eq_top _
       (LinearMap.range_eq_top.mpr this), ← rank]
@@ -213,18 +209,17 @@ lemma rank_mul_eq_left_of_isUnit_det [DecidableEq n]
 
 /-- Left multiplying by an invertible matrix does not change the rank -/
 @[simp]
-lemma rank_mul_eq_right_of_isUnit_det [Fintype m] [DecidableEq m]
-    (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) :
-    (A * B).rank = B.rank := by
+lemma rank_mul_eq_right_of_isUnit_det {R : Type*} [CommRing R] [Fintype m] [DecidableEq m]
+    (A : Matrix m m R) (B : Matrix m n R) (hA : IsUnit A.det) : (A * B).rank = B.rank := by
   let b : Basis m R (m → R) := Pi.basisFun R m
   replace hA : IsUnit (LinearMap.toMatrix b b A.mulVecLin).det := by
     convert! hA; rw [← LinearEquiv.eq_symm_apply]; rfl
   have hAB : mulVecLin (A * B) = (LinearEquiv.ofIsUnitDet hA).comp (mulVecLin B) := by ext; simp
   rw [rank, rank, hAB, LinearMap.range_comp, LinearEquiv.finrank_map_eq]
 
 /-- Taking a subset of the rows and columns reduces the rank. -/
-theorem rank_submatrix_le [Fintype n₀] (A : Matrix m n R) (r : m₀ → m) (c : n₀ → n) :
-    (A.submatrix r c).rank ≤ A.rank := by
+theorem rank_submatrix_le [CommSemiring R] [StrongRankCondition R] [Fintype n₀] (A : Matrix m n R)
+    (r : m₀ → m) (c : n₀ → n) : (A.submatrix r c).rank ≤ A.rank := by
   nontriviality R
   have := Module.Finite.span_of_finite R (Set.finite_range (A.submatrix r id).col)
   calc
@@ -242,49 +237,50 @@ theorem rank_submatrix_le [Fintype n₀] (A : Matrix m n R) (r : m₀ → m) (c
       (Equiv.refl n).symm from rfl, LinearEquiv.range, Submodule.map_top]
   exact Submodule.finrank_map_le _ _
 
-theorem rank_reindex [Fintype n₀] (em : m ≃ m₀) (en : n ≃ n₀) (A : Matrix m n R) :
+theorem rank_reindex [Fintype n₀] [CommSemiring R] (em : m ≃ m₀) (en : n ≃ n₀) (A : Matrix m n R) :
     rank (A.reindex em en) = rank A := by
   rw [rank, rank, mulVecLin_reindex, LinearMap.range_comp, LinearMap.range_comp,
     LinearEquiv.range, Submodule.map_top, LinearEquiv.finrank_map_eq]
 
 @[simp]
-theorem rank_submatrix [Fintype n₀] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
-    rank (A.submatrix em en) = rank A := by
+theorem rank_submatrix [Fintype n₀] [CommSemiring R] (A : Matrix m n R) (em : m₀ ≃ m)
+    (en : n₀ ≃ n) : rank (A.submatrix em en) = rank A := by
   simpa only [reindex_apply] using! rank_reindex em.symm en.symm A
 
 @[simp]
-theorem lift_cRank_submatrix {n : Type un} (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
-    lift.{um} (cRank (A.submatrix em en)) = lift.{um₀} (cRank A) :=
+theorem lift_cRank_submatrix {n : Type un} [Semiring R] (A : Matrix m n R) (em : m₀ ≃ m)
+    (en : n₀ ≃ n) : lift.{um} (cRank (A.submatrix em en)) = lift.{um₀} (cRank A) :=
   (A.lift_cRank_submatrix_le em en).antisymm
     <| by simpa using ((A.reindex em.symm en.symm).lift_cRank_submatrix_le em.symm en.symm)
 
 /-- A special case of `lift_cRank_submatrix` for when the row types are in the same universe. -/
 @[simp]
-theorem cRank_submatrix {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m₀ ≃ m)
+theorem cRank_submatrix {m₀ : Type um} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m₀ ≃ m)
     (en : n₀ ≃ n) : cRank (A.submatrix em en) = cRank A := by
   simpa [-lift_cRank_submatrix] using A.lift_cRank_submatrix em en
 
-theorem lift_cRank_reindex {n : Type un} (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) :
-    lift.{um} (cRank (A.reindex em en)) = lift.{um₀} (cRank A) :=
+theorem lift_cRank_reindex {n : Type un} [Semiring R] (A : Matrix m n R) (em : m ≃ m₀)
+    (en : n ≃ n₀) : lift.{um} (cRank (A.reindex em en)) = lift.{um₀} (cRank A) :=
   lift_cRank_submatrix ..
 
 /-- A special case of `lift_cRank_reindex` for when the row types are in the same universe. -/
-theorem cRank_reindex {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) :
-    cRank (A.reindex em en) = cRank A :=
+theorem cRank_reindex {m₀ : Type um} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m ≃ m₀)
+    (en : n ≃ n₀) : cRank (A.reindex em en) = cRank A :=
   cRank_submatrix ..
 
 @[simp]
-theorem eRank_submatrix {n : Type un} (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
+theorem eRank_submatrix {n : Type un} [Semiring R] (A : Matrix m n R) (em : m₀ ≃ m) (en : n₀ ≃ n) :
     eRank (A.submatrix em en) = eRank A := by
   simpa [-lift_cRank_submatrix] using! congr_arg Cardinal.toENat <| A.lift_cRank_submatrix em en
 
-theorem eRank_reindex {m₀ : Type um} {n : Type un} (A : Matrix m n R) (em : m ≃ m₀) (en : n ≃ n₀) :
-    eRank (A.reindex em en) = eRank A :=
+theorem eRank_reindex {m₀ : Type um} {n : Type un} [Semiring R] (A : Matrix m n R) (em : m ≃ m₀)
+    (en : n ≃ n₀) : eRank (A.reindex em en) = eRank A :=
   eRank_submatrix ..
 
-theorem rank_eq_finrank_range_toLin [Finite m] [DecidableEq n] {M₁ M₂ : Type*} [AddCommGroup M₁]
-    [AddCommGroup M₂] [Module R M₁] [Module R M₂] (A : Matrix m n R) (v₁ : Basis m R M₁)
-    (v₂ : Basis n R M₂) : A.rank = finrank R (LinearMap.range (toLin v₂ v₁ A)) := by
+theorem rank_eq_finrank_range_toLin [Finite m] [DecidableEq n] {M₁ M₂ : Type*} [CommSemiring R]
+    [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] (A : Matrix m n R)
+    (v₁ : Basis m R M₁) (v₂ : Basis n R M₂) :
+    A.rank = finrank R (LinearMap.range (toLin v₂ v₁ A)) := by
   cases nonempty_fintype m
   let e₁ := (Pi.basisFun R m).equiv v₁ (Equiv.refl _)
   let e₂ := (Pi.basisFun R n).equiv v₂ (Equiv.refl _)
@@ -301,28 +297,26 @@ theorem rank_eq_finrank_range_toLin [Finite m] [DecidableEq n] {M₁ M₂ : Type
   simp only [e₁, e₂, LinearMap.comp_apply, LinearEquiv.coe_coe, Equiv.refl_apply,
     aux₁, aux₂, LinearMap.coe_single, toLin_self, map_sum, map_smul, Basis.equiv_apply]
 
-theorem rank_le_card_height [Fintype m] [Nontrivial R] (A : Matrix m n R) :
-    A.rank ≤ Fintype.card m := by
-  exact (Submodule.finrank_le _).trans (finrank_pi R).le
+theorem rank_le_card_height [Fintype m] [CommSemiring R] [StrongRankCondition R]
+    (A : Matrix m n R) : A.rank ≤ Fintype.card m :=
+  (Submodule.finrank_le _).trans (finrank_pi R).le
 
-theorem rank_le_height [Nontrivial R] {m n : ℕ} (A : Matrix (Fin m) (Fin n) R) :
-    A.rank ≤ m :=
-  A.rank_le_card_height.trans <| (Fintype.card_fin m).le
+theorem rank_le_height [CommSemiring R] [StrongRankCondition R] {m n : ℕ}
+    (A : Matrix (Fin m) (Fin n) R) : A.rank ≤ m :=
+  A.rank_le_card_height.trans (Fintype.card_fin m).le
 
 /-- The rank of a matrix is the rank of the space spanned by its columns. -/
-theorem rank_eq_finrank_span_cols (A : Matrix m n R) :
+theorem rank_eq_finrank_span_cols [CommSemiring R] (A : Matrix m n R) :
     A.rank = finrank R (Submodule.span R (Set.range A.col)) := by rw [rank, Matrix.range_mulVecLin]
 
 @[simp]
-theorem cRank_toNat_eq_rank (A : Matrix m n R) : A.cRank.toNat = A.rank := by
+theorem cRank_toNat_eq_rank [CommSemiring R] (A : Matrix m n R) : A.cRank.toNat = A.rank := by
   rw [cRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]
 
 @[simp]
-theorem eRank_toNat_eq_rank (A : Matrix m n R) : A.eRank.toNat = A.rank := by
+theorem eRank_toNat_eq_rank [CommSemiring R] (A : Matrix m n R) : A.eRank.toNat = A.rank := by
   rw [eRank_toNat_eq_finrank, ← rank_eq_finrank_span_cols]
 
-end CommRing
-
 section Field
 
 variable [Field R]