chore(linear_algebra): import free_module.finite.rank from `finite_…

…dimensional` (#17482)

This PR reworks the import structure between `linear_algebra.free_module.finite` and `linear_algebra.finite_dimensional` with the goal of reducing the length of the dependency chain, and importing `linear_algebra.free_module.finite.rank` from `linear_algebra.finite_dimensional` instead of vice versa.

In addition to the changes in #17473 and #17474, this PR removes the import of `linear_algebra.matrix.to_lin` from `linear_algebra.free_module.finite.basic`, moving the dependent lemmas to `linear_algebra.free_module.finite.matrix`.



Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/matrix/rank.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin
 -/
 
 import linear_algebra.free_module.finite.rank
+import linear_algebra.matrix.to_lin
 
 /-!
 # Rank of matrices

src/linear_algebra/finite_dimensional.lean

@@ -5,7 +5,7 @@ Authors: Chris Hughes
 -/
 import algebra.algebra.subalgebra.basic
 import field_theory.finiteness
-import linear_algebra.finrank
+import linear_algebra.free_module.finite.rank
 import tactic.interval_cases
 
 /-!
@@ -248,7 +248,7 @@ lemma cardinal_mk_le_finrank_of_linear_independent
   #ι ≤ finrank K V :=
 begin
   rw ← lift_le.{_ (max v w)},
-  simpa [← finrank_eq_dim K V] using
+  simpa [← finrank_eq_dim K V, -module.free.finrank_eq_rank] using
     cardinal_lift_le_dim_of_linear_independent.{_ _ _ (max v w)} h
 end
 
@@ -368,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] using lift_dim_map_le f p
+by simpa [← finrank_eq_dim, -module.free.finrank_eq_rank] using lift_dim_map_le f p
 
 variable {K}
 

src/linear_algebra/free_module/finite/basic.lean

@@ -5,7 +5,6 @@ Authors: Riccardo Brasca
 -/
 
 import linear_algebra.free_module.basic
-import linear_algebra.matrix.to_lin
 import ring_theory.finiteness
 
 /-!
@@ -18,7 +17,6 @@ We provide some instances for finite and free modules.
 * `module.free.choose_basis_index.fintype` : If a free module is finite, then any basis is
   finite.
 * `module.free.linear_map.free ` : if `M` and `N` are finite and free, then `M →ₗ[R] N` is free.
-* `module.finite.of_basis` : A free module with a basis indexed by a `fintype` is finite.
 * `module.free.linear_map.module.finite` : if `M` and `N` are finite and free, then `M →ₗ[R] N`
   is finite.
 -/
@@ -50,15 +48,6 @@ 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) :=
-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,
-end
-
 variables {R}
 
 /-- A free module with a basis indexed by a `fintype` is finite. -/
@@ -76,32 +65,6 @@ instance _root_.module.finite.matrix {ι₁ ι₂ : Type*} [finite ι₁] [finit
 by { casesI nonempty_fintype ι₁, casesI nonempty_fintype ι₂,
   exact module.finite.of_basis (pi.basis $ λ i, pi.basis_fun R _) }
 
-instance _root_.module.finite.linear_map [module.finite R M] [module.finite R N] :
-  module.finite R (M →ₗ[R] N) :=
-begin
-  casesI subsingleton_or_nontrivial R,
-  { apply_instance },
-  classical,
-  have f := (linear_map.to_matrix (choose_basis R M) (choose_basis R N)).symm,
-  exact module.finite.of_surjective f.to_linear_map (linear_equiv.surjective f),
-end
-
 end comm_ring
 
-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) :=
-module.finite.equiv (add_monoid_hom_lequiv_int ℤ).symm
-
-instance 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
-end
-
-end integer
-
 end module.free

src/linear_algebra/free_module/finite/matrix.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2021 Riccardo Brasca. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Riccardo Brasca
+-/
+
+import linear_algebra.finrank
+import linear_algebra.free_module.finite.basic
+import linear_algebra.matrix.to_lin
+
+/-!
+# Finite and free modules using matrices
+
+We provide some instances for finite and free modules involving matrices.
+
+## Main results
+
+* `module.free.linear_map` : if `M` and `N` are finite and free, then `M →ₗ[R] N` is free.
+* `module.finite.of_basis` : A free module with a basis indexed by a `fintype` is finite.
+* `module.finite.linear_map` : if `M` and `N` are finite and free, then `M →ₗ[R] N`
+  is finite.
+-/
+
+universes u v w
+
+variables (R : Type u) (M : Type v) (N : Type w)
+
+namespace module.free
+
+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) :=
+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,
+end
+
+variables {R}
+
+instance _root_.module.finite.linear_map [module.finite R M] [module.finite R N] :
+  module.finite R (M →ₗ[R] N) :=
+begin
+  casesI subsingleton_or_nontrivial R,
+  { apply_instance },
+  classical,
+  have f := (linear_map.to_matrix (choose_basis R M) (choose_basis R N)).symm,
+  exact module.finite.of_surjective f.to_linear_map (linear_equiv.surjective f),
+end
+
+end comm_ring
+
+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) :=
+module.finite.equiv (add_monoid_hom_lequiv_int ℤ).symm
+
+instance 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
+end
+
+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) :=
+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, dim_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]
+end
+
+end comm_ring
+
+end module.free

src/linear_algebra/free_module/finite/rank.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
 
+import linear_algebra.finrank
 import linear_algebra.free_module.rank
 import linear_algebra.free_module.finite.basic
 
@@ -101,19 +102,6 @@ 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) :=
-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, dim_eq_card_basis b, ← mk_fintype, mk_to_nat_eq_card, finrank, finrank,
-    rank_eq_card_choose_basis_index, rank_eq_card_choose_basis_index, mk_to_nat_eq_card,
-    mk_to_nat_eq_card, card_prod, mul_comm]
-end
-
 /-- The finrank of `M ⊗[R] N` is `(finrank R M) * (finrank R N)`. -/
 @[simp] lemma finrank_tensor_product (M : Type v) (N : Type w) [add_comm_group M] [module R M]
   [module.free R M] [add_comm_group N] [module R N] [module.free R N] :

src/linear_algebra/multilinear/finite_dimensional.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import linear_algebra.multilinear.basic
-import linear_algebra.free_module.finite.basic
+import linear_algebra.free_module.finite.matrix
 
 /-! # Multilinear maps over finite dimensional spaces