refactor(linear_algebra/pi): add linear_map.single to match add_monoid_hom.single (#6315)

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.

Author: eric-wieser

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, pi.smul_apply, smul_zero], },
+  end,
+  .. add_monoid_hom.single φ i}
+
 section
 variables (R φ)
 

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

src/ring_theory/power_series/basic.lean

@@ -121,11 +121,11 @@ by rw [coeff, monomial, linear_map.proj_apply, linear_map.std_basis_apply, funct
 
 @[simp] lemma coeff_monomial_same (n : σ →₀ ℕ) (a : R) :
   coeff R n (monomial R n a) = a :=
-linear_map.std_basis_same _ _ _ _
+linear_map.std_basis_same R _ n a
 
 lemma coeff_monomial_ne {m n : σ →₀ ℕ} (h : m ≠ n) (a : R) :
   coeff R m (monomial R n a) = 0 :=
-linear_map.std_basis_ne  _ _ _ _ h a
+linear_map.std_basis_ne R _ _ _ h a
 
 lemma eq_of_coeff_monomial_ne_zero {m n : σ →₀ ℕ} {a : R} (h : coeff R m (monomial R n a) ≠ 0) :
   m = n :=