refactor(linear_algebra/matrix/finite_dimensional): deduplicate (#18770)

* `matrix.finrank_matrix` was a duplicate of `finite_dimensional.finrank_matrix`.
* `linear_map.finrank_linear_map` was a duplicate of `finrank_linear_hom`, now merged to `finite_dimensional.finrank_linear_map`
* `finite_dimensional.linear_map` was a duplicate of `linear_map.finite_dimensional` and can be golfed using `module.finite.linear_map`
* `finite_dimensional.matrix` can be golfed using `module.finite.matrix`

For now, I've left behind `finite_dimensional` instances, but proved them in terms of the `module.finite` versions.
To enable this, some imports have been adjusted.

The resulting import structure substantially cuts the dependencies consumed by `linear_algebra.matrix.to_lin`; it no longer needs `module.rank` to be available.



Co-authored-by: Jeremy Tan Jie Rui <e0191785@u.nus.edu>

Author: eric-wieser

src/algebra/category/fgModule/basic.lean

@@ -6,6 +6,7 @@ Authors: Jakob von Raumer
 import category_theory.monoidal.rigid.basic
 import category_theory.monoidal.subcategory
 import linear_algebra.coevaluation
+import linear_algebra.free_module.finite.matrix
 import algebra.category.Module.monoidal
 
 /-!
@@ -131,7 +132,7 @@ instance (V W : fgModule K) : module.finite K (V ⟶ W) :=
 
 instance closed_predicate_module_finite :
   monoidal_category.closed_predicate (λ V : Module.{u} K, module.finite K V) :=
-{ prop_ihom' := λ X Y hX hY, by exactI @linear_map.finite_dimensional K _ X _ _ hX Y _ _ hY }
+{ prop_ihom' := λ X Y hX hY, by exactI @module.finite.linear_map K X Y _ _ _ _ _ _ _ hX hY }
 
 instance : monoidal_closed (fgModule K) := by dsimp_result { dsimp [fgModule], apply_instance, }
 

src/analysis/normed_space/finite_dimension.lean

@@ -8,7 +8,6 @@ import analysis.normed_space.add_torsor
 import analysis.normed_space.affine_isometry
 import analysis.normed_space.operator_norm
 import analysis.normed_space.riesz_lemma
-import linear_algebra.matrix.to_lin
 import topology.algebra.module.finite_dimension
 import topology.algebra.infinite_sum.module
 import topology.instances.matrix

src/field_theory/tower.lean

@@ -114,25 +114,10 @@ theorem subalgebra.is_simple_order_of_finrank_prime (A) [ring A] [is_domain A] [
   end }
 /- TODO: `intermediate_field` version -/
 
-instance linear_map (F : Type u) (V : Type v) (W : Type w)
-  [field F] [add_comm_group V] [module F V] [add_comm_group W] [module F W]
-  [finite_dimensional F V] [finite_dimensional F W] :
-  finite_dimensional F (V →ₗ[F] W) :=
-let b := basis.of_vector_space F V, c := basis.of_vector_space F W in
-(matrix.to_lin b c).finite_dimensional
-
-lemma finrank_linear_map (F : Type u) (V : Type v) (W : Type w)
-  [field F] [add_comm_group V] [module F V] [add_comm_group W] [module F W]
-  [finite_dimensional F V] [finite_dimensional F W] :
-  finrank F (V →ₗ[F] W) = finrank F V * finrank F W :=
-  let b := basis.of_vector_space F V, c := basis.of_vector_space F W in
-by rw [linear_equiv.finrank_eq (linear_map.to_matrix b c), matrix.finrank_matrix,
-      finrank_eq_card_basis b, finrank_eq_card_basis c, mul_comm]
-
 -- TODO: generalize by removing [finite_dimensional F K]
 -- V = ⊕F,
 -- (V →ₗ[F] K) = ((⊕F) →ₗ[F] K) = (⊕ (F →ₗ[F] K)) = ⊕K
-instance linear_map' (F : Type u) (K : Type v) (V : Type w)
+instance _root_.linear_map.finite_dimensional'' (F : Type u) (K : Type v) (V : Type w)
   [field F] [field K] [algebra F K] [finite_dimensional F K]
   [add_comm_group V] [module F V] [finite_dimensional F V] :
   finite_dimensional K (V →ₗ[F] K) :=

src/linear_algebra/bilinear_form.lean

@@ -5,6 +5,7 @@ Authors: Andreas Swerdlow, Kexing Ying
 -/
 
 import linear_algebra.dual
+import linear_algebra.free_module.finite.matrix
 import linear_algebra.matrix.to_lin
 
 /-!

src/linear_algebra/determinant.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
+import linear_algebra.finite_dimensional
 import linear_algebra.general_linear_group
 import linear_algebra.matrix.reindex
 import tactic.field_simp

src/linear_algebra/free_module/finite/matrix.lean

@@ -5,7 +5,7 @@ Authors: Riccardo Brasca
 -/
 
 import linear_algebra.finrank
-import linear_algebra.free_module.finite.basic
+import linear_algebra.free_module.finite.rank
 import linear_algebra.matrix.to_lin
 
 /-!
@@ -25,25 +25,26 @@ universes u v w
 
 variables (R : Type u) (M : Type v) (N : Type w)
 
-namespace module.free
+open module.free (choose_basis)
+open finite_dimensional (finrank)
 
 section comm_ring
 
 variables [comm_ring R] [add_comm_group M] [module R M] [module.free R M]
 variables [add_comm_group N] [module R N] [module.free R N]
 
-instance linear_map [module.finite R M] [module.finite R N] : module.free R (M →ₗ[R] N) :=
+instance module.free.linear_map [module.finite R M] [module.finite R N] :
+  module.free R (M →ₗ[R] N) :=
 begin
   casesI subsingleton_or_nontrivial R,
   { apply module.free.of_subsingleton' },
   classical,
-  exact of_equiv
-    (linear_map.to_matrix (module.free.choose_basis R M) (module.free.choose_basis R N)).symm,
+  exact module.free.of_equiv (linear_map.to_matrix (choose_basis R M) (choose_basis R N)).symm,
 end
 
 variables {R}
 
-instance _root_.module.finite.linear_map [module.finite R M] [module.finite R N] :
+instance module.finite.linear_map [module.finite R M] [module.finite R N] :
   module.finite R (M →ₗ[R] N) :=
 begin
   casesI subsingleton_or_nontrivial R,
@@ -60,10 +61,10 @@ section integer
 variables [add_comm_group M] [module.finite ℤ M] [module.free ℤ M]
 variables [add_comm_group N] [module.finite ℤ N] [module.free ℤ N]
 
-instance _root_.module.finite.add_monoid_hom : module.finite ℤ (M →+ N) :=
+instance module.finite.add_monoid_hom : module.finite ℤ (M →+ N) :=
 module.finite.equiv (add_monoid_hom_lequiv_int ℤ).symm
 
-instance add_monoid_hom : module.free ℤ (M →+ N) :=
+instance module.free.add_monoid_hom : module.free ℤ (M →+ N) :=
 begin
   letI : module.free ℤ (M →ₗ[ℤ] N) := module.free.linear_map _ _ _,
   exact module.free.of_equiv (add_monoid_hom_lequiv_int ℤ).symm
@@ -73,25 +74,30 @@ end integer
 
 section comm_ring
 
-open finite_dimensional
-
 variables [comm_ring R] [strong_rank_condition R]
 variables [add_comm_group M] [module R M] [module.free R M] [module.finite R M]
 variables [add_comm_group N] [module R N] [module.free R N] [module.finite R N]
 
 /-- The finrank of `M →ₗ[R] N` is `(finrank R M) * (finrank R N)`. -/
---TODO: this should follow from `linear_equiv.finrank_eq`, that is over a field.
-lemma finrank_linear_hom : finrank R (M →ₗ[R] N) = (finrank R M) * (finrank R N) :=
+lemma finite_dimensional.finrank_linear_map :
+  finrank R (M →ₗ[R] N) = (finrank R M) * (finrank R N) :=
 begin
   classical,
   letI := nontrivial_of_invariant_basis_number R,
   have h := (linear_map.to_matrix (choose_basis R M) (choose_basis R N)),
-  let b := (matrix.std_basis _ _ _).map h.symm,
-  rw [finrank, rank_eq_card_basis b, ← cardinal.mk_fintype, cardinal.mk_to_nat_eq_card, finrank,
-    finrank, rank_eq_card_choose_basis_index, rank_eq_card_choose_basis_index,
-    cardinal.mk_to_nat_eq_card, cardinal.mk_to_nat_eq_card, fintype.card_prod, mul_comm]
+  simp_rw [h.finrank_eq, finite_dimensional.finrank_matrix,
+    finite_dimensional.finrank_eq_card_choose_basis_index, mul_comm],
 end
 
 end comm_ring
 
-end module.free
+lemma matrix.rank_vec_mul_vec {K m n : Type u}
+  [comm_ring K] [strong_rank_condition K] [fintype n] [decidable_eq n]
+  (w : m → K) (v : n → K) :
+  (matrix.vec_mul_vec w v).to_lin'.rank ≤ 1 :=
+begin
+  rw [matrix.vec_mul_vec_eq, matrix.to_lin'_mul],
+  refine le_trans (linear_map.rank_comp_le_left _ _) _,
+  refine (linear_map.rank_le_domain _).trans_eq _,
+  rw [rank_fun', fintype.card_unit, nat.cast_one]
+end

src/linear_algebra/free_module/finite/rank.lean

@@ -90,7 +90,7 @@ end
 
 /-- If `m` and `n` are `fintype`, the finrank of `m × n` matrices is
   `(fintype.card m) * (fintype.card n)`. -/
-lemma finrank_matrix (m n : Type v) [fintype m] [fintype n] :
+lemma finrank_matrix (m n : Type*) [fintype m] [fintype n] :
   finrank R (matrix m n R) = (card m) * (card n) :=
 by { simp [finrank] }
 

src/linear_algebra/matrix/diagonal.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
 import linear_algebra.matrix.to_lin
+import linear_algebra.free_module.rank
 
 /-!
 # Diagonal matrices

src/linear_algebra/matrix/finite_dimensional.lean

@@ -5,17 +5,20 @@ Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
 import data.matrix.basic
 import linear_algebra.finite_dimensional
+import linear_algebra.free_module.finite.matrix
+import linear_algebra.matrix.to_lin
 
 /-!
 # The finite-dimensional space of matrices
 
-This file shows that `m` by `n` matrices form a finite-dimensional space,
-and proves the `finrank` of that space is equal to `card m * card n`.
+This file shows that `m` by `n` matrices form a finite-dimensional space.
+Note that this is proven more generally elsewhere over modules as `module.finite.matrix`; this file
+exists only to provide an entry in the instance list for `finite_dimensional`.
 
 ## Main definitions
 
  * `matrix.finite_dimensional`: matrices form a finite dimensional vector space over a field `K`
- * `matrix.finrank_matrix`: the `finrank` of `matrix m n R` is `card m * card n`
+ * `linear_map.finite_dimensional`
 
 ## Tags
 
@@ -32,17 +35,28 @@ section finite_dimensional
 variables {m n : Type*} {R : Type v} [field R]
 
 instance [finite m] [finite n] : finite_dimensional R (matrix m n R) :=
-linear_equiv.finite_dimensional (linear_equiv.curry R m n)
-
-/--
-The dimension of the space of finite dimensional matrices
-is the product of the number of rows and columns.
--/
-@[simp] lemma finrank_matrix [fintype m] [fintype n] :
-  finite_dimensional.finrank R (matrix m n R) = fintype.card m * fintype.card n :=
-by rw [@linear_equiv.finrank_eq R (matrix m n R) _ _ _ _ _ _ (linear_equiv.curry R m n).symm,
-       finite_dimensional.finrank_fintype_fun_eq_card, fintype.card_prod]
+module.finite.matrix
 
 end finite_dimensional
 
 end matrix
+
+namespace linear_map
+
+variables {K : Type*} [field K]
+variables {V : Type*} [add_comm_group V] [module K V] [finite_dimensional K V]
+variables {W : Type*} [add_comm_group W] [module K W] [finite_dimensional K W]
+
+instance finite_dimensional : finite_dimensional K (V →ₗ[K] W) :=
+module.finite.linear_map _ _
+
+variables {A : Type*} [ring A] [algebra K A] [module A V] [is_scalar_tower K A V]
+  [module A W] [is_scalar_tower K A W]
+
+/-- Linear maps over a `k`-algebra are finite dimensional (over `k`) if both the source and
+target are, as they form a subspace of all `k`-linear maps. -/
+instance finite_dimensional' : finite_dimensional K (V →ₗ[A] W) :=
+finite_dimensional.of_injective (restrict_scalars_linear_map K A V W)
+  (restrict_scalars_injective _)
+
+end linear_map

src/linear_algebra/matrix/to_lin.lean

@@ -5,7 +5,6 @@ Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
 import data.matrix.block
 import data.matrix.notation
-import linear_algebra.matrix.finite_dimensional
 import linear_algebra.std_basis
 import ring_theory.algebra_tower
 import algebra.module.algebra
@@ -342,17 +341,6 @@ lemma linear_map.to_matrix_alg_equiv'_mul
   (f * g).to_matrix_alg_equiv' = f.to_matrix_alg_equiv' ⬝ g.to_matrix_alg_equiv' :=
 linear_map.to_matrix_alg_equiv'_comp f g
 
-lemma matrix.rank_vec_mul_vec {K m n : Type u}
-  [comm_ring K] [strong_rank_condition K] [fintype n] [decidable_eq n]
-  (w : m → K) (v : n → K) :
-  rank (vec_mul_vec w v).to_lin' ≤ 1 :=
-begin
-  rw [vec_mul_vec_eq, matrix.to_lin'_mul],
-  refine le_trans (rank_comp_le_left _ _) _,
-  refine (rank_le_domain _).trans_eq _,
-  rw [rank_fun', fintype.card_unit, nat.cast_one]
-end
-
 end to_matrix'
 
 section to_matrix
@@ -723,51 +711,6 @@ end lmul_tower
 
 end algebra
 
-namespace linear_map
-
-section finite_dimensional
-
-open_locale classical
-
-variables {K : Type*} [field K]
-variables {V : Type*} [add_comm_group V] [module K V] [finite_dimensional K V]
-variables {W : Type*} [add_comm_group W] [module K W] [finite_dimensional K W]
-
-instance finite_dimensional : finite_dimensional K (V →ₗ[K] W) :=
-linear_equiv.finite_dimensional
-  (linear_map.to_matrix (basis.of_vector_space K V) (basis.of_vector_space K W)).symm
-
-section
-
-variables {A : Type*} [ring A] [algebra K A] [module A V] [is_scalar_tower K A V]
-  [module A W] [is_scalar_tower K A W]
-
-/-- Linear maps over a `k`-algebra are finite dimensional (over `k`) if both the source and
-target are, as they form a subspace of all `k`-linear maps. -/
-instance finite_dimensional' : finite_dimensional K (V →ₗ[A] W) :=
-finite_dimensional.of_injective (restrict_scalars_linear_map K A V W)
-  (restrict_scalars_injective _)
-
-end
-
-/--
-The dimension of the space of linear transformations is the product of the dimensions of the
-domain and codomain.
--/
-@[simp] lemma finrank_linear_map :
-  finite_dimensional.finrank K (V →ₗ[K] W) =
-  (finite_dimensional.finrank K V) * (finite_dimensional.finrank K W) :=
-begin
-  let hbV := basis.of_vector_space K V,
-  let hbW := basis.of_vector_space K W,
-  rw [linear_equiv.finrank_eq (linear_map.to_matrix hbV hbW), matrix.finrank_matrix,
-    finite_dimensional.finrank_eq_card_basis hbV, finite_dimensional.finrank_eq_card_basis hbW,
-    mul_comm],
-end
-
-end finite_dimensional
-end linear_map
-
 section
 
 variables {R : Type v} [comm_ring R] {n : Type*} [decidable_eq n]