chore(linear_algebra/free_module/finite/rank): move lemmas from `modu…

…le.free` to `finite_dimensional` (#18733)

The lemmas about finite-dimensional spaces are currently scattered between namespaces.
This commit mostly addresses the confusion by renaming all the `module.free.finrank_*` lemmas to `finite_dimensional.finrank_*`.

This rename makes it apparent that `finrank_eq_dim` and `finrank_eq_rank` are duplicates; though it seems that for performances reasons it's still useful in one or two places to keep both.

[Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/naming.3A.20finrank.20and.20rank.20lemmas/near/346701602)

src/data/matrix/rank.lean

@@ -38,15 +38,15 @@ variables (A : matrix m n K)
 noncomputable def rank : ℕ := finrank K A.to_lin'.range
 
 @[simp] lemma rank_one : rank (1 : matrix n n K) = fintype.card n :=
-by rw [rank, to_lin'_one, linear_map.range_id, finrank_top, module.free.finrank_pi]
+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 :=
 by rw [rank, linear_equiv.map_zero, linear_map.range_zero, finrank_bot]
 
 lemma rank_le_card_width : A.rank ≤ fintype.card n :=
 begin
   convert le_of_add_le_left (A.to_lin'.finrank_range_add_finrank_ker).le,
-  exact (module.free.finrank_pi K).symm,
+  exact (finrank_pi K).symm,
 end
 
 lemma rank_le_width {m n : ℕ} (A : matrix (fin m) (fin n) K) : A.rank ≤ n :=
@@ -96,7 +96,7 @@ begin
 end
 
 lemma rank_le_card_height : A.rank ≤ fintype.card m :=
-(submodule.finrank_le _).trans (module.free.finrank_pi K).le
+(submodule.finrank_le _).trans (finrank_pi K).le
 
 omit m_fin
 

src/linear_algebra/finite_dimensional.lean

@@ -168,13 +168,10 @@ module.finite.of_surjective (submodule.mkq S) $ surjective_quot_mk _
 
 variables (K V)
 /-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
-`finrank`. -/
+`finrank`. This is a copy of `finrank_eq_rank _ _` which creates easier typeclass searches. -/
 lemma finrank_eq_dim [finite_dimensional K V] :
   (finrank K V : cardinal.{v}) = module.rank K V :=
-begin
-  letI : is_noetherian K V := iff_fg.2 infer_instance,
-  rw [finrank, cast_to_nat_of_lt_aleph_0 (dim_lt_aleph_0 K V)]
-end
+finrank_eq_rank _ _
 variables {K V}
 
 lemma finrank_of_infinite_dimensional (h : ¬finite_dimensional K V) : finrank K V = 0 :=
@@ -252,7 +249,7 @@ lemma cardinal_mk_le_finrank_of_linear_independent
   #ι ≤ finrank K V :=
 begin
   rw ← lift_le.{_ (max v w)},
-  simpa [← finrank_eq_dim, -module.free.finrank_eq_rank] using
+  simpa [← finrank_eq_dim, -finrank_eq_rank] using
     cardinal_lift_le_dim_of_linear_independent.{_ _ _ (max v w)} h
 end
 
@@ -371,7 +368,7 @@ end
 /-- Pushforwards of finite-dimensional submodules have a smaller finrank. -/
 lemma finrank_map_le (f : V →ₗ[K] V₂) (p : submodule K V) [finite_dimensional K p] :
   finrank K (p.map f) ≤ finrank K p :=
-by simpa [← finrank_eq_dim, -module.free.finrank_eq_rank] using lift_dim_map_le f p
+by simpa [← finrank_eq_dim, -finrank_eq_rank] using lift_dim_map_le f p
 
 variable {K}
 

src/linear_algebra/free_module/finite/rank.lean

@@ -16,8 +16,7 @@ This is a basic API for the rank of finite free modules.
 
 -/
 
---TODO: `linear_algebra/finite_dimensional` should import this file, and a lot of results should
---be moved here.
+--TODO: many results from `linear_algebra/finite_dimensional` should be moved here.
 
 universes u v w
 
@@ -27,7 +26,8 @@ open_locale tensor_product direct_sum big_operators cardinal
 
 open cardinal finite_dimensional fintype
 
-namespace module.free
+namespace finite_dimensional
+open module.free
 
 section ring
 
@@ -110,4 +110,4 @@ by { simp [finrank] }
 
 end comm_ring
 
-end module.free
+end finite_dimensional

src/linear_algebra/trace.lean

@@ -165,7 +165,7 @@ trace_eq_contract_of_basis' (module.free.choose_basis R M)
 @[simp] theorem trace_one : trace R M 1 = (finrank R M : R) :=
 begin
   have b := module.free.choose_basis R M,
-  rw [trace_eq_matrix_trace R b, to_matrix_one, module.free.finrank_eq_card_choose_basis_index],
+  rw [trace_eq_matrix_trace R b, to_matrix_one, finrank_eq_card_choose_basis_index],
   simp,
 end
 

src/number_theory/ramification_inertia.lean

@@ -815,7 +815,7 @@ begin
           finrank (R ⧸ p) (S ⧸ (P : ideal S)^(e P)) : _
   ... = finrank (R ⧸ p) (Π P : (factors (map (algebra_map R S) p)).to_finset,
           (S ⧸ (P : ideal S)^(e P))) :
-    (module.free.finrank_pi_fintype (R ⧸ p)).symm
+    (finrank_pi_fintype (R ⧸ p)).symm
   ... = finrank (R ⧸ p) (S ⧸ map (algebra_map R S) p) : _
   ... = finrank K L : _,
   { rw ← finset.sum_attach,

src/ring_theory/dedekind_domain/integral_closure.lean

@@ -233,7 +233,8 @@ begin
   haveI : is_localization (algebra.algebra_map_submonoid C A⁰) L :=
     is_integral_closure.is_localization A K L C,
   let b := basis.localization_localization K A⁰ L (module.free.choose_basis A C),
-  rw [module.free.finrank_eq_card_choose_basis_index, finite_dimensional.finrank_eq_card_basis b],
+  rw [finite_dimensional.finrank_eq_card_choose_basis_index,
+    finite_dimensional.finrank_eq_card_basis b],
 end
 
 variables {A K}