feat(linear_algebra/matrix): linear maps are linearly equivalent to matrices (#1310)

* linear map to matrix (WIP)

* WIP

* feat (linear_algebra/matrix): lin_equiv_matrix

* feat (linear_algebra.basic): linear_equiv.arrow_congr, std_basis_eq_single

* change unnecessary vector_space assumption for equiv_fun_basis to module

* add docstrings and refactor

* add docstrings

* move instance to pi_instances

* add docstrings + name change

* remove duplicate instance

Author: CPutz

src/field_theory/finite_card.lean

@@ -14,7 +14,7 @@ namespace finite_field
 theorem card (p : ℕ) [char_p α p] : ∃ (n : ℕ+), nat.prime p ∧ fintype.card α = p^(n : ℕ) :=
 have hp : nat.prime p, from char_p.char_is_prime α p,
 have V : vector_space (zmodp p hp) α, from {..zmod.to_module'},
-let ⟨n, h⟩ := @vector_space.card_fintype' _ _ _ _ _ _ V _ _ in
+let ⟨n, h⟩ := @vector_space.card_fintype _ _ _ _ _ _ V _ _ in
 have hn : n > 0, from or.resolve_left (nat.eq_zero_or_pos n)
   (assume h0 : n = 0,
   have fintype.card α = 1, by rw[←nat.pow_zero (fintype.card _), ←h0]; exact h,

src/linear_algebra/basic.lean

@@ -1242,12 +1242,33 @@ of_linear ((a:α) • 1 : β →ₗ β) (((a⁻¹ : units α) : α) • 1 : β 
   (by rw [smul_comp, comp_smul, smul_smul, units.mul_inv, one_smul]; refl)
   (by rw [smul_comp, comp_smul, smul_smul, units.inv_mul, one_smul]; refl)
 
-def congr_right (f : γ ≃ₗ[α] δ) : (β →ₗ[α] γ) ≃ₗ (β →ₗ δ) :=
-of_linear
-  f.to_linear_map.congr_right
-  f.symm.to_linear_map.congr_right
-  (linear_map.ext $ λ _, linear_map.ext $ λ _, f.6 _)
-  (linear_map.ext $ λ _, linear_map.ext $ λ _, f.5 _)
+/-- A linear isomorphism between the domains and codomains of two spaces of linear maps gives a
+linear isomorphism between the two function spaces. -/
+def arrow_congr {α β₁ β₂ γ₁ γ₂ : Sort*} [comm_ring α]
+  [add_comm_group β₁] [add_comm_group β₂] [add_comm_group γ₁] [add_comm_group γ₂]
+  [module α β₁] [module α β₂] [module α γ₁] [module α γ₂]
+  (e₁ : β₁ ≃ₗ[α] β₂) (e₂ : γ₁ ≃ₗ[α] γ₂) :
+  (β₁ →ₗ[α] γ₁) ≃ₗ[α] (β₂ →ₗ[α] γ₂) :=
+{ to_fun := λ f, e₂.to_linear_map.comp $ f.comp e₁.symm.to_linear_map,
+  inv_fun := λ f, e₂.symm.to_linear_map.comp $ f.comp e₁.to_linear_map,
+  left_inv := λ f, by { ext x, unfold_coes,
+    change e₂.inv_fun (e₂.to_fun $ f.to_fun $ e₁.inv_fun $ e₁.to_fun x) = _,
+    rw [e₁.left_inv, e₂.left_inv] },
+  right_inv := λ f, by { ext x, unfold_coes,
+    change e₂.to_fun (e₂.inv_fun $ f.to_fun $ e₁.to_fun $ e₁.inv_fun x) = _,
+    rw [e₁.right_inv, e₂.right_inv] },
+  add := λ f g, by { ext x, change e₂.to_fun ((f + g) (e₁.inv_fun x)) = _,
+    rw [linear_map.add_apply, e₂.add], refl },
+  smul := λ c f, by { ext x, change e₂.to_fun ((c • f) (e₁.inv_fun x)) = _,
+    rw [linear_map.smul_apply, e₂.smul], refl } }
+
+/-- If γ and δ are linearly isomorphic then the two spaces of linear maps from β into γ and
+β into δ are linearly isomorphic. -/
+def congr_right (f : γ ≃ₗ[α] δ) : (β →ₗ[α] γ) ≃ₗ (β →ₗ δ) := arrow_congr (linear_equiv.refl β) f
+
+/-- If β and γ are linearly isomorphic then the two spaces of linear maps from β and γ to themselves
+are linearly isomorphic. -/
+def conj (e : β ≃ₗ[α] γ) : (β →ₗ[α] β) ≃ₗ[α] (γ →ₗ[α] γ) := arrow_congr e e
 
 end comm_ring
 
@@ -1528,6 +1549,16 @@ begin
   { exact hI i hiI }
 end
 
+lemma std_basis_eq_single [decidable_eq α] {a : α} :
+  (λ (i : ι), (std_basis α (λ _ : ι, α) i) a) = λ (i : ι), (finsupp.single i a) :=
+begin
+  ext i j,
+  rw [std_basis_apply, finsupp.single_apply],
+  split_ifs,
+  { rw [h, function.update_same] },
+  { rw [function.update_noteq (ne.symm h)], refl },
+end
+
 end
 
 end pi

src/linear_algebra/basis.lean

@@ -776,6 +776,22 @@ begin
   exact (submodule.mem_bot α).1 (subtype.mem x),
 end
 
+open fintype
+variables [fintype ι] (h : is_basis α v)
+
+/-- A module over α with a finite basis is linearly equivalent to functions from its basis to α. -/
+def equiv_fun_basis  : β ≃ₗ[α] (ι → α) :=
+linear_equiv.trans (module_equiv_finsupp h)
+  { to_fun := finsupp.to_fun,
+    add := λ x y, by ext; exact finsupp.add_apply,
+    smul := λ x y, by ext; exact finsupp.smul_apply,
+    ..finsupp.equiv_fun_on_fintype }
+
+theorem module.card_fintype [fintype α] [fintype β] :
+  card β = (card α) ^ (card ι) :=
+calc card β = card (ι → α)    : card_congr (equiv_fun_basis h).to_equiv
+        ... = card α ^ card ι : card_fun
+
 end module
 
 section vector_space
@@ -1006,27 +1022,15 @@ begin
 end
 
 open fintype
-variables (h : is_basis α v)
-
-local attribute [instance] submodule.module
-
-noncomputable def equiv_fun_basis [fintype ι] : β ≃ (ι → α) :=
-calc β ≃ (ι →₀ α) : (module_equiv_finsupp h).to_equiv
-   ... ≃ (ι → α)                              : finsupp.equiv_fun_on_fintype
-
-theorem vector_space.card_fintype [fintype ι] [fintype α] [fintype β] :
-  card β = (card α) ^ (card ι) :=
-calc card β = card (ι → α)    : card_congr (equiv_fun_basis h)
-        ... = card α ^ card ι : card_fun
 
-theorem vector_space.card_fintype' [fintype α] [fintype β] :
+theorem vector_space.card_fintype [fintype α] [fintype β] :
   ∃ n : ℕ, card β = (card α) ^ n :=
 begin
   apply exists.elim (exists_is_basis α β),
   intros b hb,
   haveI := classical.dec_pred (λ x, x ∈ b),
   use card b,
-  exact vector_space.card_fintype hb,
+  exact module.card_fintype hb,
 end
 
 end vector_space

src/linear_algebra/matrix.lean

@@ -1,26 +1,52 @@
 /-
 Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Author: Johannes Hölzl
+Author: Johannes Hölzl, Casper Putz
 
-Linear structures on function with finit support `α →₀ β` and multivariate polynomials.
+The equivalence between matrices and linear maps.
 -/
+
 import data.matrix.basic
 import linear_algebra.dimension linear_algebra.tensor_product
+
+/-!
+
+# Linear maps and matrices
+
+This file defines the maps to send matrices to a linear map,
+and to send linear maps between modules with a finite bases
+to matrices. This defines a linear equivalence between linear maps
+between finite-dimensional vector spaces and matrices indexed by
+the respective bases.
+
+Some results are proved about the linear map corresponding to a
+diagonal matrix (range, ker and rank).
+
+## Main definitions
+
+to_lin, to_matrix, lin_equiv_matrix
+
+## Tags
+
+linear_map, matrix, linear_equiv, diagonal
+
+-/
+
 noncomputable theory
 
-open lattice set linear_map submodule
+open set submodule
 
-namespace matrix
 universes u v
-variables {l m n o : Type u} [fintype l] [fintype m] [fintype n] [fintype o]
+variables {l m n : Type u} [fintype l] [fintype m] [fintype n]
 
-instance [decidable_eq m] [decidable_eq n] (α) [fintype α] : fintype (matrix m n α) :=
-by unfold matrix; apply_instance
+namespace matrix
 
-section ring
 variables {α : Type v} [comm_ring α]
+instance [decidable_eq m] [decidable_eq n] (α) [fintype α] : fintype (matrix m n α) :=
+by unfold matrix; apply_instance
 
+/-- Evaluation of matrices gives a linear map from matrix m n α to
+linear maps (n → α) →ₗ[α] (m → α). -/
 def eval : (matrix m n α) →ₗ[α] ((n → α) →ₗ[α] (m → α)) :=
 begin
   refine linear_map.mk₂ α mul_vec _ _ _ _,
@@ -43,6 +69,8 @@ begin
     refl }
 end
 
+/-- Evaluation of matrices gives a map from matrix m n α to
+linear maps (n → α) →ₗ[α] (m → α). -/
 def to_lin : matrix m n α → (n → α) →ₗ[α] (m → α) := eval.to_fun
 
 lemma to_lin_add (M N : matrix m n α) : (M + N).to_lin = M.to_lin + N.to_lin :=
@@ -72,8 +100,96 @@ begin
   rw [mul_assoc]
 end
 
-section
-open linear_map
+end matrix
+
+namespace linear_map
+
+variables {α : Type v} [comm_ring α]
+
+/-- The linear map from linear maps (n → α) →ₗ[α] (m → α) to matrix m n α. -/
+def to_matrixₗ [decidable_eq n] : ((n → α) →ₗ[α] (m → α)) →ₗ[α] matrix m n α :=
+begin
+  refine linear_map.mk (λ f i j, f (λ n, ite (j = n) 1 0) i) _ _,
+  { assume f g, simp only [add_apply], refl },
+  { assume f g, simp only [smul_apply], refl }
+end
+
+/-- The map from linear maps (n → α) →ₗ[α] (m → α) to matrix m n α. -/
+def to_matrix [decidable_eq n] : ((n → α) →ₗ[α] (m → α)) → matrix m n α := to_matrixₗ.to_fun
+
+end linear_map
+
+section lin_equiv_matrix
+
+variables {α : Type v} [comm_ring α] [decidable_eq n]
+
+open finsupp matrix linear_map
+
+/-- to_lin is the left inverse of to_matrix. -/
+lemma to_matrix_to_lin [decidable_eq α] {f : (n → α) →ₗ[α] (m → α)} :
+  to_lin (to_matrix f) = f :=
+begin
+  ext : 1,
+  -- Show that the two sides are equal by showing that they are equal on a basis
+  convert linear_eq_on (set.range _) _ (is_basis.mem_span (@pi.is_basis_fun α _ n _ _ _) _),
+  assume e he,
+  rw [@std_basis_eq_single α _ _ _ _ 1] at he,
+  cases (set.mem_range.mp he) with i h,
+  ext j,
+  change finset.univ.sum (λ k, (f.to_fun (single k 1).to_fun) j * (e k)) = _,
+  rw [←h],
+  conv_lhs { congr, skip, funext,
+    rw [mul_comm, ←smul_eq_mul, ←pi.smul_apply, ←linear_map.smul, single_apply],
+    rw [show f.to_fun (ite (i = k) (1:α) 0 • (single k 1).to_fun) = ite (i = k) (f.to_fun ((single k 1).to_fun)) 0,
+      { split_ifs, { rw [one_smul] }, { rw [zero_smul], exact linear_map.map_zero f } }] },
+  convert finset.sum_eq_single i _ _,
+  { rw [if_pos rfl], refl },
+  { assume _ _ hbi, rw [if_neg $ ne.symm hbi], refl },
+  { assume hi, exact false.elim (hi $ finset.mem_univ i) }
+end
+
+/-- to_lin is the right inverse of to_matrix. -/
+lemma to_lin_to_matrix {M : matrix m n α} : to_matrix (to_lin M) = M :=
+begin
+  ext,
+  change finset.univ.sum (λ y, M i y * ite (j = y) 1 0) = M i j,
+  have h1 : (λ y, M i y * ite (j = y) 1 0) = (λ y, ite (j = y) (M i y) 0),
+    { ext, split_ifs, exact mul_one _, exact ring.mul_zero _ },
+  have h2 : finset.univ.sum (λ y, ite (j = y) (M i y) 0) = (finset.singleton j).sum (λ y, ite (j = y) (M i y) 0),
+    { refine (finset.sum_subset _ _).symm,
+      { intros _ H, rwa finset.mem_singleton.1 H, exact finset.mem_univ _ },
+      { exact λ _ _ H, if_neg (mt (finset.mem_singleton.2 ∘ eq.symm) H) } },
+  rw [h1, h2, finset.sum_singleton],
+  exact if_pos rfl
+end
+
+/-- Linear maps (n → α) →ₗ[α] (m → α) are linearly equivalent to matrix  m n α. -/
+def lin_equiv_matrix' [decidable_eq α] : ((n → α) →ₗ[α] (m → α)) ≃ₗ[α] matrix m n α :=
+{ to_fun := to_matrix,
+  inv_fun := to_lin,
+  right_inv := λ _, to_lin_to_matrix,
+  left_inv := λ _, to_matrix_to_lin,
+  add := to_matrixₗ.add,
+  smul := to_matrixₗ.smul }
+
+/-- Given a basis of two modules β and γ over a commutative ring α, we get a linear equivalence
+between linear maps β →ₗ γ and matrices over α indexed by the bases. -/
+def lin_equiv_matrix {ι κ β γ : Type*} [decidable_eq α]
+  [add_comm_group β] [decidable_eq β] [module α β]
+  [add_comm_group γ] [decidable_eq γ] [module α γ]
+  [fintype ι] [decidable_eq ι] [fintype κ] [decidable_eq κ]
+  {v₁ : ι → β} {v₂ : κ → γ} (hv₁ : is_basis α v₁) (hv₂ : is_basis α v₂) :
+  (β →ₗ[α] γ) ≃ₗ[α] matrix κ ι α :=
+linear_equiv.trans (linear_equiv.arrow_congr (equiv_fun_basis hv₁) (equiv_fun_basis hv₂)) lin_equiv_matrix'
+
+end lin_equiv_matrix
+
+namespace matrix
+
+section ring
+
+variables {α : Type v} [comm_ring α]
+open linear_map matrix
 
 lemma proj_diagonal [decidable_eq m] (i : m) (w : m → α) :
   (proj i).comp (to_lin (diagonal w)) = (w i) • proj i :=
@@ -89,14 +205,14 @@ begin
   { subst h },
   { rw [std_basis_ne α (λ_:n, α) _ _ (ne.symm h), _root_.mul_zero, _root_.mul_zero] }
 end
-end
 
 end ring
 
 section vector_space
+
 variables {α : Type u} [discrete_field α] -- maybe try to relax the universe constraint
 
-open linear_map
+open linear_map matrix
 
 lemma rank_vec_mul_vec [decidable_eq n] (w : m → α) (v : n → α) :
   rank (vec_mul_vec w v).to_lin ≤ 1 :=