feat(linear_algebra/free_module): add instances (#9072)

From LTE.

We prove that `M →ₗ[R] N` is free if both `M` and `N` are finite and free. This needs the quite long result that for a finite and free module any basis is finite.

Co-authored with @jcommelin

src/linear_algebra/free_module.lean

@@ -5,8 +5,10 @@ Authors: Riccardo Brasca
 -/
 
 import linear_algebra.direct_sum.finsupp
+import linear_algebra.matrix.to_lin
 import linear_algebra.std_basis
 import logic.small
+import ring_theory.finiteness
 
 /-!
 
@@ -27,7 +29,7 @@ universes u v w z
 
 variables (R : Type u) (M : Type v) (N : Type z)
 
-open_locale tensor_product direct_sum
+open_locale tensor_product direct_sum big_operators
 
 section basic
 
@@ -131,17 +133,44 @@ instance pi {ι : Type*} [fintype ι] {M : ι → Type*} [Π (i : ι), add_comm_
 [Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)] : module.free R (Π i, M i) :=
 of_basis $ pi.basis $ λ i, choose_basis R (M i)
 
+instance matrix {n : Type*} [fintype n] {m : Type*} [fintype m] :
+  module.free R (matrix n m R) :=
+of_basis $ matrix.std_basis R n m
+
 end semiring
 
+section ring
+
+variables [ring R] [add_comm_group M] [module R M] [module.free R M]
+
+/-- If a free module is finite, then any basis is finite. -/
+noncomputable
+instance [nontrivial R] [module.finite R M] :
+  fintype (module.free.choose_basis_index R M) :=
+begin
+  obtain ⟨h⟩ := id ‹module.finite R M›,
+  choose s hs using h,
+  exact basis_fintype_of_finite_spans ↑s hs (choose_basis _ _),
+end
+
+end ring
+
 section comm_ring
 
-variables [comm_ring R] [add_comm_group M] [module R M]
-variables [add_comm_group N] [module R N]
+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 tensor [module.free R M] [module.free R N] : module.free R (M ⊗[R] N) :=
+instance tensor : module.free R (M ⊗[R] N) :=
 of_equiv' (of_equiv' (finsupp.free R) (finsupp_tensor_finsupp' R _ _).symm)
   (tensor_product.congr (choose_basis R M).repr (choose_basis R N).repr).symm
 
+instance [nontrivial R] [module.finite R M] [module.finite R N] : module.free R (M →ₗ[R] N) :=
+begin
+  classical,
+  exact of_equiv
+    (linear_map.to_matrix (module.free.choose_basis R M) (module.free.choose_basis R N)).symm,
+end
+
 end comm_ring
 
 section division_ring

src/linear_algebra/matrix/diagonal.lean

@@ -35,7 +35,8 @@ lemma proj_diagonal (i : n) (w : n → R) :
 by ext j; simp [mul_vec_diagonal]
 
 lemma diagonal_comp_std_basis (w : n → R) (i : n) :
-  (diagonal w).to_lin'.comp (std_basis R (λ_:n, R) i) = (w i) • std_basis R (λ_:n, R) i :=
+  (diagonal w).to_lin'.comp (linear_map.std_basis R (λ_:n, R) i) =
+  (w i) • linear_map.std_basis R (λ_:n, R) i :=
 begin
   ext j,
   simp_rw [linear_map.comp_apply, to_lin'_apply, mul_vec_diagonal, linear_map.smul_apply,
@@ -57,7 +58,7 @@ variables {m n : Type*} [fintype m] [fintype n]
 variables {K : Type u} [field K] -- maybe try to relax the universe constraint
 
 lemma ker_diagonal_to_lin' [decidable_eq m] (w : m → K) :
-  ker (diagonal w).to_lin' = (⨆i∈{i | w i = 0 }, range (std_basis K (λi, K) i)) :=
+  ker (diagonal w).to_lin' = (⨆i∈{i | w i = 0 }, range (linear_map.std_basis K (λi, K) i)) :=
 begin
   rw [← comap_bot, ← infi_ker_proj],
   simp only [comap_infi, (ker_comp _ _).symm, proj_diagonal, ker_smul'],
@@ -67,7 +68,7 @@ begin
 end
 
 lemma range_diagonal [decidable_eq m] (w : m → K) :
-  (diagonal w).to_lin'.range = (⨆ i ∈ {i | w i ≠ 0}, (std_basis K (λi, K) i).range) :=
+  (diagonal w).to_lin'.range = (⨆ i ∈ {i | w i ≠ 0}, (linear_map.std_basis K (λi, K) i).range) :=
 begin
   dsimp only [mem_set_of_eq],
   rw [← map_top, ← supr_range_std_basis, map_supr],

src/linear_algebra/std_basis.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 import linear_algebra.basic
 import linear_algebra.basis
 import linear_algebra.pi
+import data.matrix.basic
 
 /-!
 # The standard basis
@@ -250,6 +251,11 @@ by { simp only [basis_fun, basis.coe_of_equiv_fun, linear_equiv.refl_symm,
   (pi.basis_fun R η).repr x i = x i :=
 by simp [basis_fun]
 
+/-- The standard basis on `matrix n m R`. -/
+noncomputable def _root_.matrix.std_basis (n : Type*) (m : Type*) [fintype m] [fintype n] :
+  basis (Σ (j : n), (λ (i : n), m) j) R (matrix n m R) :=
+pi.basis (λ (i : n), pi.basis_fun R m)
+
 end
 
 end module