From 90475a9b99604f918292045f7ef7a2238db0f2cc Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 9 Sep 2021 07:32:08 +0000
Subject: [PATCH] refactor(data/matrix): put std_basis_matrix in its own file
 (#9088)

The authors here are recovered from the git history.

I've avoided the temptation to generalize typeclasses in this PR; the lemmas are copied to this file unmodified.
---
 src/data/matrix/basic.lean              | 76 --------------------
 src/data/matrix/basis.lean              | 94 +++++++++++++++++++++++++
 src/ring_theory/matrix_algebra.lean     |  2 +-
 src/ring_theory/polynomial_algebra.lean |  1 +
 4 files changed, 96 insertions(+), 77 deletions(-)
 create mode 100644 src/data/matrix/basis.lean

diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
index 14627c9b0fdbb..15e69ec7cbb8f 100644
--- a/src/data/matrix/basic.lean
+++ b/src/data/matrix/basic.lean
@@ -1048,82 +1048,6 @@ by { ext, rw [←diagonal_one, vec_mul_diagonal, mul_one] }
 
 end non_assoc_semiring
 
-section semiring
-variables [semiring α]
-
-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, 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_std_basis (x : matrix n m α) [fintype n] [fintype m] :
-  x = ∑ (i : n) (j : m), std_basis_matrix i j (x i j) :=
-begin
-  ext, symmetry,
-  iterate 2 { rw finset.sum_apply },
-  convert fintype.sum_eq_single i _,
-  { simp [std_basis_matrix] },
-  { intros j hj,
-    simp [std_basis_matrix, hj.symm] }
-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 std_basis_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
-
--- todo: the old proof used fintypes, I don't know `finsupp` but this feels generalizable
-@[elab_as_eliminator] protected lemma induction_on' [fintype n]
-  {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_std_basis : ∀ i j x, M (std_basis_matrix i j x)) :
-  M m :=
-begin
-  rw [matrix_eq_sum_std_basis m, ← finset.sum_product'],
-  apply finset.sum_induction _ _ h_add h_zero,
-  { intros, apply h_std_basis, }
-end
-
-@[elab_as_eliminator] protected lemma induction_on [fintype n]
-  [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_std_basis : ∀ 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_std_basis i i 0,
-end
-h_add h_std_basis
-
-end semiring
-
 section ring
 
 variables [ring α]
diff --git a/src/data/matrix/basis.lean b/src/data/matrix/basis.lean
new file mode 100644
index 0000000000000..42b0b89cbbd6c
--- /dev/null
+++ b/src/data/matrix/basis.lean
@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2020 Jalex Stark. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jalex Stark, Scott Morrison, Eric Wieser
+-/
+import data.matrix.basic
+
+/-!
+# Matrices with a single non-zero element.
+
+This file provides `matrix.std_basis_matrix`.
+-/
+
+variables {l m n : Type*}
+variables {R α : Type*}
+
+namespace matrix
+open_locale matrix
+open_locale big_operators
+
+variables [decidable_eq l] [decidable_eq m] [decidable_eq n]
+
+variables [semiring α]
+
+/--
+`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, 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_std_basis (x : matrix n m α) [fintype n] [fintype m] :
+  x = ∑ (i : n) (j : m), std_basis_matrix i j (x i j) :=
+begin
+  ext, symmetry,
+  iterate 2 { rw finset.sum_apply },
+  convert fintype.sum_eq_single i _,
+  { simp [std_basis_matrix] },
+  { intros j hj,
+    simp [std_basis_matrix, hj.symm] }
+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 std_basis_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
+
+-- todo: the old proof used fintypes, I don't know `finsupp` but this feels generalizable
+@[elab_as_eliminator] protected lemma induction_on' [fintype n]
+  {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_std_basis : ∀ i j x, M (std_basis_matrix i j x)) :
+  M m :=
+begin
+  rw [matrix_eq_sum_std_basis m, ← finset.sum_product'],
+  apply finset.sum_induction _ _ h_add h_zero,
+  { intros, apply h_std_basis, }
+end
+
+@[elab_as_eliminator] protected lemma induction_on [fintype n]
+  [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_std_basis : ∀ 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_std_basis i i 0,
+end
+h_add h_std_basis
+
+end matrix
diff --git a/src/ring_theory/matrix_algebra.lean b/src/ring_theory/matrix_algebra.lean
index dd9f981e5b5c1..989907f83b41e 100644
--- a/src/ring_theory/matrix_algebra.lean
+++ b/src/ring_theory/matrix_algebra.lean
@@ -3,7 +3,7 @@ Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import data.matrix.basic
+import data.matrix.basis
 import ring_theory.tensor_product
 
 /-!
diff --git a/src/ring_theory/polynomial_algebra.lean b/src/ring_theory/polynomial_algebra.lean
index b977392f2a406..6642bc9f4c74c 100644
--- a/src/ring_theory/polynomial_algebra.lean
+++ b/src/ring_theory/polynomial_algebra.lean
@@ -5,6 +5,7 @@ Authors: Scott Morrison
 -/
 import ring_theory.matrix_algebra
 import data.polynomial.algebra_map
+import data.matrix.basis
 
 /-!
 # Algebra isomorphism between matrices of polynomials and polynomials of matrices