feat(data/matrix): std_basis_matrix (#3244)

The definition of
```
def std_basis_matrix (i : m) (j : n) (a : α) : matrix m n α :=
(λ i' j', if i' = i ∧ j' = j then a else 0)
```
and associated lemmas, and some refactoring of `src/ring_theory/matrix_algebra.lean` to use it.

This is work of @jalex-stark which I'm PR'ing as part of getting Cayley-Hamilton ready.

Co-authored-by: Jalex Stark <alexmaplegm@gmail.com>



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Author: kim-em

src/algebra/big_operators.lean

@@ -6,6 +6,7 @@ Authors: Johannes Hölzl
 
 import data.finset
 import data.nat.enat
+import data.equiv.mul_add
 import tactic.omega
 import tactic.abel
 
@@ -101,6 +102,11 @@ lemma monoid_hom.map_prod [comm_monoid β] [comm_monoid γ] (g : β →* γ) (f
   g (∏ x in s, f x) = ∏ x in s, g (f x) :=
 by simp only [finset.prod_eq_multiset_prod, g.map_multiset_prod, multiset.map_map]
 
+@[to_additive]
+lemma mul_equiv.map_prod [comm_monoid β] [comm_monoid γ] (g : β ≃* γ) (f : α → β) (s : finset α) :
+  g (∏ x in s, f x) = ∏ x in s, g (f x) :=
+g.to_monoid_hom.map_prod f s
+
 lemma ring_hom.map_list_prod [semiring β] [semiring γ] (f : β →+* γ) (l : list β) :
   f l.prod = (l.map f).prod :=
 f.to_monoid_hom.map_list_prod l
@@ -242,6 +248,12 @@ begin
   apply h, cc
 end
 
+/-- An uncurried version of `prod_product`. -/
+@[to_additive]
+lemma prod_product' {s : finset γ} {t : finset α} {f : γ → α → β} :
+  (∏ x in s.product t, f x.1 x.2) = ∏ x in s, ∏ y in t, f x y :=
+by rw prod_product
+
 @[to_additive]
 lemma prod_sigma {σ : α → Type*}
   {s : finset α} {t : Πa, finset (σ a)} {f : sigma σ → β} :

src/data/matrix/basic.lean

@@ -362,6 +362,22 @@ def scalar (n : Type u) [fintype n] [decidable_eq n] : α →+* matrix n n α :=
   map_one' := by simp,
   map_mul' := by { intros, ext, simp [mul_assoc], }, }
 
+section scalar
+
+variable [decidable_eq n]
+
+@[simp] lemma coe_scalar : (scalar n : α → matrix n n α) = λ a, a • 1 := rfl
+
+lemma scalar_apply_eq (a : α) (i : n) :
+  scalar n a i i = a :=
+by simp only [coe_scalar, mul_one, one_val_eq, smul_val]
+
+lemma scalar_apply_ne (a : α) (i j : n) (h : i ≠ j) :
+  scalar n a i j = 0 :=
+by simp only [h, coe_scalar, one_val_ne, ne.def, not_false_iff, smul_val, mul_zero]
+
+end scalar
+
 end semiring
 
 section comm_semiring
@@ -437,6 +453,79 @@ lemma vec_mul_vec_eq (w : m → α) (v : n → α) :
   vec_mul_vec w v = (col w) ⬝ (row v) :=
 by { ext i j, simp [vec_mul_vec, mul_val], refl }
 
+variables [decidable_eq m] [decidable_eq n]
+
+/--
+`std_basis_matrix i j a` is the matrix with `a` in the `i`-th row, `j`-th column,
+and zeroes elsewhere.
+-/
+def std_basis_matrix (i : m) (j : n) (a : α) : matrix m n α :=
+(λ i' j', if i' = i ∧ j' = j then a else 0)
+
+@[simp] lemma smul_std_basis_matrix (i : m) (j : n) (a b : α) :
+b • std_basis_matrix i j a = std_basis_matrix i j (b • a) :=
+by { unfold std_basis_matrix, ext, dsimp, simp }
+
+@[simp] lemma std_basis_matrix_zero (i : m) (j : n) :
+std_basis_matrix i j (0 : α) = 0 :=
+by { unfold std_basis_matrix, ext, simp }
+
+lemma std_basis_matrix_add (i : m) (j : n) (a b : α) :
+std_basis_matrix i j (a + b) = std_basis_matrix i j a + std_basis_matrix i j b :=
+begin
+  unfold std_basis_matrix, ext,
+  split_ifs with h; simp [h],
+end
+
+
+lemma matrix_eq_sum_elementary (x : matrix n m α) :
+x = ∑ (i : n) (j : m), std_basis_matrix i j (x i j) :=
+begin
+  ext, iterate 2 {rw finset.sum_apply},
+  rw ← finset.sum_subset, swap 4, exact {i},
+  { norm_num [std_basis_matrix] },
+  { simp },
+  intros, norm_num at a, norm_num,
+  convert finset.sum_const_zero,
+  ext, norm_num [std_basis_matrix],
+  rw if_neg, tauto!,
+end
+
+-- TODO: tie this up with the `basis` machinery of linear algebra
+-- this is not completely trivial because we are indexing by two types, instead of one
+
+-- TODO: add `std_basis_vec`
+lemma elementary_eq_basis_mul_basis (i : m) (j : n) :
+std_basis_matrix i j 1 = vec_mul_vec (λ i', ite (i = i') 1 0) (λ j', ite (j = j') 1 0) :=
+begin
+  ext, norm_num [std_basis_matrix, vec_mul_vec],
+  split_ifs; tauto,
+end
+
+@[elab_as_eliminator] protected lemma induction_on'
+  {X : Type*} [semiring X] {M : matrix n n X → Prop} (m : matrix n n X)
+  (h_zero : M 0)
+  (h_add : ∀p q, M p → M q → M (p + q))
+  (h_elementary : ∀ i j x, M (std_basis_matrix i j x)) :
+  M m :=
+begin
+  rw [matrix_eq_sum_elementary m, ← finset.sum_product'],
+  apply finset.sum_induction _ _ h_add h_zero,
+  { intros, apply h_elementary, }
+end
+
+@[elab_as_eliminator] protected lemma induction_on
+  [nonempty n] {X : Type*} [semiring X] {M : matrix n n X → Prop} (m : matrix n n X)
+  (h_add : ∀p q, M p → M q → M (p + q))
+  (h_elementary : ∀ i j x, M (std_basis_matrix i j x)) :
+  M m :=
+matrix.induction_on' m
+begin
+  have i : n := classical.choice (by assumption),
+  simpa using h_elementary i i 0,
+end
+h_add h_elementary
+
 end semiring
 
 section ring

src/ring_theory/algebra.lean

@@ -415,6 +415,10 @@ end
   [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
   ∀ x y, e (x - y) = e x - e y := e.to_add_equiv.map_sub
 
+lemma map_sum (e : A₁ ≃ₐ[R] A₂) {ι : Type*} (f : ι → A₁) (s : finset ι) :
+  e (∑ x in s, f x) = ∑ x in s, e (f x) :=
+e.to_add_equiv.map_sum f s
+
 instance has_coe_to_alg_hom : has_coe (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂) :=
   ⟨λ e, { map_one' := e.map_one, map_zero' := e.map_zero, ..e }⟩
 
@@ -462,6 +466,9 @@ def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃
 @[simp] lemma symm_apply_apply (e : A₁ ≃ₐ[R] A₂) : ∀ x, e.symm (e x) = x :=
   e.to_equiv.symm_apply_apply
 
+@[simp] lemma trans_apply (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) (x : A₁) :
+  (e₁.trans e₂) x = e₂ (e₁ x) := rfl
+
 @[simp] lemma comp_symm (e : A₁ ≃ₐ[R] A₂) :
   alg_hom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = alg_hom.id R A₂ :=
 by { ext, simp }

src/ring_theory/matrix_algebra.lean

@@ -18,6 +18,7 @@ open_locale big_operators
 
 open tensor_product
 open algebra.tensor_product
+open matrix
 
 variables {R : Type u} [comm_ring R]
 variables {A : Type v} [comm_ring A] [algebra R A]
@@ -90,7 +91,8 @@ variables [decidable_eq n]
 The function `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`, as an algebra homomorphism.
 -/
 def to_fun_alg_hom : (A ⊗[R] matrix n n R) →ₐ[R] matrix n n A :=
-alg_hom_of_linear_map_tensor_product (to_fun_linear R A n)
+alg_hom_of_linear_map_tensor_product
+(to_fun_linear R A n)
 begin
   intros, ext,
   simp only [to_fun_linear, to_fun_bilinear, to_fun_right_linear, to_fun, lift.tmul,
@@ -119,7 +121,7 @@ The bare function `matrix n n A → A ⊗[R] matrix n n R`.
 (We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)
 -/
 def inv_fun (M : matrix n n A) : A ⊗[R] matrix n n R :=
-∑ (p : n × n), M p.1 p.2 ⊗ₜ (λ i' j', if (i', j') = p then 1 else 0)
+∑ (p : n × n), M p.1 p.2 ⊗ₜ (std_basis_matrix p.1 p.2 1)
 
 @[simp] lemma inv_fun_zero : inv_fun R A n 0 = 0 :=
 by simp [inv_fun]
@@ -136,22 +138,17 @@ by simp [inv_fun,finset.mul_sum]
   inv_fun R A n (λ i j, algebra_map R A (M i j)) = 1 ⊗ₜ M :=
 begin
   dsimp [inv_fun],
-  simp only [algebra.algebra_map_eq_smul_one, smul_tmul, ←tmul_sum, (•), mul_boole],
-  congr, ext,
-  calc
-    (∑ (x : n × n), λ (i i_1 : n), ite ((i, i_1) = x) (M x.fst x.snd) 0) i j
-      = (∑ (x : n × n), λ (i_1 : n), ite ((i, i_1) = x) (M x.fst x.snd) 0) j : _
-     ... = (∑ (x : n × n), ite ((i, j) = x) (M x.fst x.snd) 0) : _
-     ... = M i j : _,
-  { apply congr_fun, dsimp, simp, },
-  { simp, },
-  { simp, },
+  simp only [algebra.algebra_map_eq_smul_one, smul_tmul, ←tmul_sum, mul_boole],
+  congr,
+  conv_rhs {rw matrix_eq_sum_elementary M},
+  convert finset.sum_product, simp,
 end
 
 lemma right_inv (M : matrix n n A) : (to_fun_alg_hom R A n) (inv_fun R A n M) = M :=
 begin
-  ext,
-  simp [inv_fun, alg_hom.map_sum, apply_ite (algebra_map R A)],
+  simp only [inv_fun, alg_hom.map_sum, std_basis_matrix, apply_ite ⇑(algebra_map R A),
+    mul_boole, to_fun_alg_hom_apply, ring_hom.map_zero, ring_hom.map_one],
+  convert finset.sum_product, apply matrix_eq_sum_elementary,
 end
 
 lemma left_inv (M : A ⊗[R] matrix n n R) : inv_fun R A n (to_fun_alg_hom R A n M) = M :=
@@ -187,9 +184,17 @@ open matrix_equiv_tensor
 
 @[simp] lemma matrix_equiv_tensor_apply (M : matrix n n A) :
   matrix_equiv_tensor R A n M =
-    ∑ (p : n × n), M p.1 p.2 ⊗ₜ (λ i' j', if (i', j') = p then 1 else 0) :=
+    ∑ (p : n × n), M p.1 p.2 ⊗ₜ (std_basis_matrix p.1 p.2 1) :=
 rfl
 
+@[simp] lemma matrix_equiv_tensor_apply_elementary (i j : n) (x : A):
+  matrix_equiv_tensor R A n (std_basis_matrix i j x) =
+    x ⊗ₜ (std_basis_matrix i j 1) :=
+begin
+  have t : ∀ (p : n × n), (p.1 = i ∧ p.2 = j) ↔ (p = (i, j)) := by tidy,
+  simp [ite_tmul, t, std_basis_matrix],
+end
+
 @[simp] lemma matrix_equiv_tensor_apply_symm (a : A) (M : matrix n n R) :
   (matrix_equiv_tensor R A n).symm (a ⊗ₜ M) =
     λ i j, a * algebra_map R A (M i j) :=