From ada381d492060c41c5510881da72e49488d127f1 Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Fri, 19 Feb 2021 15:44:34 +0000
Subject: [PATCH] refactor(linear_algebra/pi): add `linear_map.single` to match
 `add_monoid_hom.single`

This changes the definition of `std_basis` to be exactly `linear_map.single`, but proves equality with the old definition.

In future, it might make sense to remove `std_basis` entirely.
---
 src/linear_algebra/pi.lean        | 15 ++++++++++++++-
 src/linear_algebra/std_basis.lean | 13 ++++++++++---
 2 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/src/linear_algebra/pi.lean b/src/linear_algebra/pi.lean
index 31cbe5a876e79..94a7545c1d397 100644
--- a/src/linear_algebra/pi.lean
+++ b/src/linear_algebra/pi.lean
@@ -15,8 +15,10 @@ It contains theorems relating these to each other, as well as to `linear_map.ker
 ## Main definitions
 
 - pi types in the codomain:
-  - `linear_map.proj`
   - `linear_map.pi`
+  - `linear_map.single`
+- pi types in the domain:
+  - `linear_map.proj`
 - `linear_map.diag`
 
 -/
@@ -70,6 +72,17 @@ begin
   exact (mem_bot _).2 (funext $ assume i, h i)
 end
 
+/-- The `linear_map` version of `add_monoid_hom.single` and `pi.single`. -/
+@[simps]
+def single [decidable_eq ι] (i : ι) : φ i →ₗ[R] (Πi, φ i) :=
+{ to_fun := pi.single i,
+  map_smul' := λ r x, begin
+    ext i', by_cases h : i' = i,
+    { subst h, simp only [pi.single_eq_same, pi.smul_apply], },
+    { simp only [h, pi.single_eq_of_ne, ne.def, not_false_iff], },
+  end,
+  .. add_monoid_hom.single φ i}
+
 section
 variables (R φ)
 
diff --git a/src/linear_algebra/std_basis.lean b/src/linear_algebra/std_basis.lean
index d745326503a86..ba85cbe727876 100644
--- a/src/linear_algebra/std_basis.lean
+++ b/src/linear_algebra/std_basis.lean
@@ -39,10 +39,10 @@ variables (R : Type*) {ι : Type*} [semiring R] (φ : ι → Type*)
   [Π i, add_comm_monoid (φ i)] [Π i, semimodule R (φ i)] [decidable_eq ι]
 
 /-- The standard basis of the product of `φ`. -/
-def std_basis (i : ι) : φ i →ₗ[R] (Πi, φ i) := pi (diag i)
+def std_basis : Π (i : ι), φ i →ₗ[R] (Πi, φ i) := single
 
 lemma std_basis_apply (i : ι) (b : φ i) : std_basis R φ i b = update 0 i b :=
-by ext j; rw [std_basis, pi_apply, diag, update_apply]; refl
+rfl
 
 lemma coe_std_basis (i : ι) : ⇑(std_basis R φ i) = pi.single i :=
 funext $ std_basis_apply R φ i
@@ -53,6 +53,13 @@ by rw [std_basis_apply, update_same]
 lemma std_basis_ne (i j : ι) (h : j ≠ i) (b : φ i) : std_basis R φ i b j = 0 :=
 by rw [std_basis_apply, update_noteq h]; refl
 
+lemma std_basis_eq_pi_diag (i : ι) : std_basis R φ i = pi (diag i) :=
+begin
+  ext x j,
+  convert (update_apply 0 x i j _).symm,
+  refl,
+end
+
 section ext
 
 variables {R φ} {M : Type*} [fintype ι] [add_comm_monoid M] [semimodule R M]
@@ -84,7 +91,7 @@ ker_eq_bot_of_injective $ assume f g hfg,
   by simpa only [std_basis_same]
 
 lemma proj_comp_std_basis (i j : ι) : (proj i).comp (std_basis R φ j) = diag j i :=
-by rw [std_basis, proj_pi]
+by rw [std_basis_eq_pi_diag, proj_pi]
 
 lemma proj_std_basis_same (i : ι) : (proj i).comp (std_basis R φ i) = id :=
 by ext b; simp