feat(linear_algebra/matrix/rank): generalize to rings (#18748)

This addresses a TODO comment.

To achieve this we generalize `submodule.finrank_le`, `submodule.finrank_quotient_le`, and `finrank_le_finrank_of_injective` from vector spaces to free modules, and add a new lemma `linear_map.finrank_range_le`.

src/data/matrix/rank.lean

@@ -20,7 +20,6 @@ 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 column-rank
-* Generalize away from fields
 
 -/
 
@@ -30,77 +29,88 @@ namespace matrix
 
 open finite_dimensional
 
-variables {m n o K : Type*} [m_fin : fintype m] [fintype n] [fintype o]
-variables [decidable_eq n] [decidable_eq o] [field K]
-variables (A : matrix m n K)
+variables {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. -/
-noncomputable def rank : ℕ := finrank K A.to_lin'.range
+noncomputable def rank (A : matrix m n R) : ℕ := finrank R A.to_lin'.range
 
-@[simp] lemma rank_one : rank (1 : matrix n n K) = fintype.card n :=
+@[simp] lemma rank_one [strong_rank_condition R] : rank (1 : matrix n n R) = fintype.card n :=
 by rw [rank, to_lin'_one, linear_map.range_id, finrank_top, finrank_pi]
 
-@[simp] lemma rank_zero : rank (0 : matrix n n K) = 0 :=
+@[simp] lemma rank_zero [nontrivial R] : rank (0 : matrix m n R) = 0 :=
 by rw [rank, linear_equiv.map_zero, linear_map.range_zero, finrank_bot]
 
-lemma rank_le_card_width : A.rank ≤ fintype.card n :=
+lemma rank_le_card_width [strong_rank_condition R] (A : matrix m n R) : A.rank ≤ fintype.card n :=
 begin
-  convert le_of_add_le_left (A.to_lin'.finrank_range_add_finrank_ker).le,
-  exact (finrank_pi K).symm,
+  haveI : module.finite R (n → R) := module.finite.pi,
+  haveI : module.free R (n → R) := module.free.pi _ _,
+  exact A.to_lin'.finrank_range_le.trans_eq (finrank_pi _)
 end
 
-lemma rank_le_width {m n : ℕ} (A : matrix (fin m) (fin n) K) : A.rank ≤ n :=
+lemma rank_le_width [strong_rank_condition R] {m n : ℕ} (A : matrix (fin m) (fin n) R) :
+  A.rank ≤ n :=
 A.rank_le_card_width.trans $ (fintype.card_fin n).le
 
-lemma rank_mul_le (B : matrix n o K) : (A ⬝ B).rank ≤ A.rank :=
+lemma rank_mul_le [strong_rank_condition R] (A : matrix m n R) (B : matrix n o R) :
+  (A ⬝ B).rank ≤ A.rank :=
 begin
-  refine linear_map.finrank_le_finrank_of_injective (submodule.of_le_injective _),
-  rw [to_lin'_mul],
-  exact linear_map.range_comp_le_range _ _,
+  rw [rank, rank, to_lin'_mul],
+  refine cardinal.to_nat_le_of_le_of_lt_aleph_0 _ (linear_map.rank_comp_le1 _ _),
+  rw [←cardinal.lift_lt_aleph_0],
+  have := lift_rank_range_le A.to_lin',
+  rw [rank_fun', cardinal.lift_nat_cast] at this,
+  exact this.trans_lt (cardinal.nat_lt_aleph_0 (fintype.card n)),
 end
 
-lemma rank_unit (A : (matrix n n K)ˣ) :
-  (A : matrix n n K).rank = fintype.card n :=
+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 K) (↑A⁻¹ : matrix n n K),
+  have := rank_mul_le (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
 
-lemma rank_of_is_unit (A : matrix n n K) (h : is_unit A) :
+lemma rank_of_is_unit [strong_rank_condition R] (A : matrix n n R) (h : is_unit A) :
   A.rank = fintype.card n :=
 by { obtain ⟨A, rfl⟩ := h, exact rank_unit A }
 
 include m_fin
 
 lemma rank_eq_finrank_range_to_lin
   {M₁ M₂ : Type*} [add_comm_group M₁] [add_comm_group M₂]
-  [module K M₁] [module K M₂] (v₁ : basis m K M₁) (v₂ : basis n K M₂) :
-  A.rank = finrank K (to_lin v₂ v₁ A).range :=
+  [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 (to_lin v₂ v₁ A).range :=
 begin
-  let e₁ := (pi.basis_fun K m).equiv v₁ (equiv.refl _),
-  let e₂ := (pi.basis_fun K n).equiv v₂ (equiv.refl _),
-  have range_e₂ : (e₂ : (n → K) →ₗ[K] M₂).range = ⊤,
+  let e₁ := (pi.basis_fun R m).equiv v₁ (equiv.refl _),
+  let e₂ := (pi.basis_fun R n).equiv v₂ (equiv.refl _),
+  have range_e₂ : (e₂ : (n → R) →ₗ[R] M₂).range = ⊤,
   { rw linear_map.range_eq_top, exact e₂.surjective },
   refine linear_equiv.finrank_eq (e₁.of_submodules _ _ _),
   rw [← linear_map.range_comp, ← linear_map.range_comp_of_range_eq_top (to_lin v₂ v₁ A) range_e₂],
   congr' 1,
   apply linear_map.pi_ext', rintro i, apply linear_map.ext_ring,
-  have aux₁ := to_lin_self (pi.basis_fun K n) (pi.basis_fun K m) A i,
-  have aux₂ := basis.equiv_apply (pi.basis_fun K n) i v₂,
+  have aux₁ := to_lin_self (pi.basis_fun R n) (pi.basis_fun R m) A i,
+  have aux₂ := basis.equiv_apply (pi.basis_fun R n) i v₂,
   rw [to_lin_eq_to_lin'] at aux₁,
   rw [pi.basis_fun_apply, linear_map.coe_std_basis] at aux₁ aux₂,
   simp only [linear_map.comp_apply, e₁, e₂, linear_equiv.coe_coe, equiv.refl_apply, aux₁, aux₂,
     linear_map.coe_single, to_lin_self, linear_equiv.map_sum, linear_equiv.map_smul,
     basis.equiv_apply],
 end
 
-lemma rank_le_card_height : A.rank ≤ fintype.card m :=
-(submodule.finrank_le _).trans (finrank_pi K).le
+lemma rank_le_card_height [strong_rank_condition R] (A : matrix m n R) :
+  A.rank ≤ fintype.card m :=
+begin
+  haveI : module.finite R (m → R) := module.finite.pi,
+  haveI : module.free R (m → R) := module.free.pi _ _,
+  exact (submodule.finrank_le _).trans (finrank_pi R).le
+end
 
 omit m_fin
 
-lemma rank_le_height {m n : ℕ} (A : matrix (fin m) (fin n) K) : A.rank ≤ m :=
+lemma rank_le_height [strong_rank_condition R] {m n : ℕ} (A : matrix (fin m) (fin n) R) :
+  A.rank ≤ m :=
 A.rank_le_card_height.trans $ (fintype.card_fin m).le
 
 end matrix

src/linear_algebra/finite_dimensional.lean

@@ -696,17 +696,6 @@ begin
   exact submodule.finite_dimensional_finset_sup _ _,
 end
 
-/-- The dimension of a submodule is bounded by the dimension of the ambient space. -/
-lemma finrank_le [finite_dimensional K V] (s : submodule K V) : finrank K s ≤ finrank K V :=
-by simpa only [cardinal.nat_cast_le, ←finrank_eq_rank] using
-  s.subtype.rank_le_of_injective (injective_subtype s)
-
-/-- The dimension of a quotient is bounded by the dimension of the ambient space. -/
-lemma finrank_quotient_le [finite_dimensional K V] (s : submodule K V) :
-  finrank K (V ⧸ s) ≤ finrank K V :=
-by simpa only [cardinal.nat_cast_le, ←finrank_eq_rank] using
-  (mkq s).rank_le_of_surjective (surjective_quot_mk _)
-
 /-- In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding
 quotient add up to the dimension of the space. -/
 theorem finrank_quotient_add_finrank [finite_dimensional K V] (s : submodule K V) :
@@ -1014,13 +1003,6 @@ lemma ker_eq_bot_iff_range_eq_top_of_finrank_eq_finrank [finite_dimensional K V]
   f.ker = ⊥ ↔ f.range = ⊤ :=
 by rw [range_eq_top, ker_eq_bot, injective_iff_surjective_of_finrank_eq_finrank H]
 
-theorem finrank_le_finrank_of_injective [finite_dimensional K V] [finite_dimensional K V₂]
-  {f : V →ₗ[K] V₂} (hf : function.injective f) : finrank K V ≤ finrank K V₂ :=
-calc  finrank K V
-    = finrank K f.range + finrank K f.ker : (finrank_range_add_finrank_ker f).symm
-... = finrank K f.range : by rw [ker_eq_bot.2 hf, finrank_bot, add_zero]
-... ≤ finrank K V₂ : submodule.finrank_le _
-
 /-- Given a linear map `f` between two vector spaces with the same dimension, if
 `ker f = ⊥` then `linear_equiv_of_injective` is the induced isomorphism
 between the two vector spaces. -/

src/linear_algebra/finrank.lean

@@ -85,6 +85,12 @@ begin
     exact n.zero_le },
 end
 
+lemma finrank_le_finrank_of_rank_le_rank
+  (h : lift.{v'} (module.rank K V) ≤ cardinal.lift.{v} (module.rank K V₂))
+  (h' : module.rank K V₂ < ℵ₀) :
+    finrank K V ≤ finrank K V₂ :=
+by simpa only [to_nat_lift] using to_nat_le_of_le_of_lt_aleph_0 (lift_lt_aleph_0.mpr h') h
+
 section
 variables [nontrivial K] [no_zero_smul_divisors K V]
 

src/linear_algebra/free_module/finite/rank.lean

@@ -111,3 +111,35 @@ by { simp [finrank] }
 end comm_ring
 
 end finite_dimensional
+
+section
+open finite_dimensional
+
+variables {R M N}
+variables [ring R] [strong_rank_condition R]
+variables [add_comm_group M] [module R M]
+variables [add_comm_group N] [module R N]
+
+lemma linear_map.finrank_le_finrank_of_injective
+  [module.free R N] [module.finite R N] {f : M →ₗ[R] N} (hf : function.injective f) :
+  finrank R M ≤ finrank R N :=
+finrank_le_finrank_of_rank_le_rank
+  (linear_map.lift_rank_le_of_injective _ hf) (rank_lt_aleph_0 _ _)
+
+lemma linear_map.finrank_range_le [module.free R M] [module.finite R M] (f : M →ₗ[R] N) :
+  finrank R f.range ≤ finrank R M :=
+finrank_le_finrank_of_rank_le_rank (lift_rank_range_le f) (rank_lt_aleph_0 _ _)
+
+/-- The dimension of a submodule is bounded by the dimension of the ambient space. -/
+lemma submodule.finrank_le [module.free R M] [module.finite R M] (s : submodule R M) :
+  finrank R s ≤ finrank R M :=
+by simpa only [cardinal.to_nat_lift] using to_nat_le_of_le_of_lt_aleph_0
+  (rank_lt_aleph_0 _ _) (rank_submodule_le s)
+
+/-- The dimension of a quotient is bounded by the dimension of the ambient space. -/
+lemma submodule.finrank_quotient_le [module.free R M] [module.finite R M] (s : submodule R M) :
+  finrank R (M ⧸ s) ≤ finrank R M :=
+by simpa only [cardinal.to_nat_lift] using to_nat_le_of_le_of_lt_aleph_0
+  (rank_lt_aleph_0 _ _) ((submodule.mkq s).rank_le_of_surjective (surjective_quot_mk _))
+
+end