chore(ring_theory/matrix_algebra): golf using matrix.map (#15040)

This replaces terms of the form `λ i j, a * algebra_map R A (m i j)` with the defeq `a • m.map (algebra_map R A)`, as then we get access to the API about `map`.

This also leverages existing bundled maps to avoid reproving linearity in the auxiliary constructions, removing `to_fun` and `to_fun_right_linear` as we can construct `to_fun_bilinear` directly with ease.

Author: eric-wieser

src/ring_theory/matrix_algebra.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Scott Morrison
+Authors: Scott Morrison, Eric Wieser
 -/
 import data.matrix.basis
 import ring_theory.tensor_product
@@ -27,39 +27,16 @@ variables {n : Type w}
 variables (R A n)
 namespace matrix_equiv_tensor
 
-/--
-(Implementation detail).
-The bare function underlying `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`, on pure tensors.
--/
-def to_fun (a : A) (m : matrix n n R) : matrix n n A :=
-λ i j, a * algebra_map R A (m i j)
-
-/--
-(Implementation detail).
-The function underlying `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`,
-as an `R`-linear map in the second tensor factor.
--/
-def to_fun_right_linear (a : A) : matrix n n R →ₗ[R] matrix n n A :=
-{ to_fun := to_fun R A n a,
-  map_add' := λ x y, by { dsimp only [to_fun], ext, simp [mul_add], },
-  map_smul' := λ r x,
-  begin
-    dsimp only [to_fun],
-    ext,
-    simp only [pi.smul_apply, ring_hom.map_mul, algebra.id.smul_eq_mul],
-    dsimp,
-    rw [algebra.smul_def r, ←_root_.mul_assoc, ←_root_.mul_assoc, algebra.commutes],
-  end, }
-
 /--
 (Implementation detail).
 The function underlying `(A ⊗[R] matrix n n R) →ₐ[R] matrix n n A`,
 as an `R`-bilinear map.
 -/
 def to_fun_bilinear : A →ₗ[R] matrix n n R →ₗ[R] matrix n n A :=
-{ to_fun := to_fun_right_linear R A n,
-  map_add' := λ x y, by { ext, simp [to_fun_right_linear, to_fun, add_mul], },
-  map_smul' := λ r x, by { ext, simp [to_fun_right_linear, to_fun] }, }
+(algebra.lsmul R (matrix n n A)).to_linear_map.compl₂ (algebra.linear_map R A).map_matrix
+
+@[simp] lemma to_fun_bilinear_apply (a : A) (m : matrix n n R) :
+  to_fun_bilinear R A n a m = a • m.map (algebra_map R A) := rfl
 
 /--
 (Implementation detail).
@@ -78,28 +55,23 @@ 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)
 begin
-  intros, ext,
-  simp_rw [to_fun_linear, to_fun_bilinear, lift.tmul],
+  intros,
+  simp_rw [to_fun_linear, lift.tmul, to_fun_bilinear_apply, mul_eq_mul, matrix.map_mul],
+  ext,
   dsimp,
-  simp_rw [to_fun_right_linear],
-  dsimp,
-  simp_rw [to_fun, matrix.mul_mul_left, pi.smul_apply, smul_eq_mul, matrix.mul_apply,
-    ←_root_.mul_assoc _ a₂ _, algebra.commutes, _root_.mul_assoc a₂ _ _, ←finset.mul_sum,
-    ring_hom.map_sum, ring_hom.map_mul, _root_.mul_assoc],
+  simp_rw [matrix.mul_apply, matrix.map, pi.smul_apply, smul_eq_mul, finset.mul_sum,
+    _root_.mul_assoc, algebra.left_comm],
 end
 begin
-  intros, ext,
-  simp only [to_fun_linear, to_fun_bilinear, to_fun_right_linear, to_fun, matrix.one_apply,
-    algebra_map_matrix_apply, lift.tmul, linear_map.coe_mk],
-  split_ifs; simp,
+  intros,
+  simp_rw [to_fun_linear, lift.tmul, to_fun_bilinear_apply,
+    matrix.map_one (algebra_map R A) (map_zero _) (map_one _), algebra_map_smul,
+    algebra.algebra_map_eq_smul_one],
 end
 
 @[simp] lemma to_fun_alg_hom_apply (a : A) (m : matrix n n R) :
-  to_fun_alg_hom R A n (a ⊗ₜ m) = λ i j, a * algebra_map R A (m i j) :=
-begin
-  simp [to_fun_alg_hom, alg_hom_of_linear_map_tensor_product, to_fun_linear],
-  refl,
-end
+  to_fun_alg_hom R A n (a ⊗ₜ m) = a • m.map (algebra_map R A) :=
+by simp [to_fun_alg_hom, alg_hom_of_linear_map_tensor_product, to_fun_linear]
 
 /--
 (Implementation detail.)
@@ -118,11 +90,11 @@ by simp [inv_fun]
 by simp [inv_fun, add_tmul, finset.sum_add_distrib]
 
 @[simp] lemma inv_fun_smul (a : A) (M : matrix n n A) :
-  inv_fun R A n (λ i j, a * M i j) = (a ⊗ₜ 1) * inv_fun R A n M :=
+  inv_fun R A n (a • M) = (a ⊗ₜ 1) * inv_fun R A n M :=
 by simp [inv_fun,finset.mul_sum]
 
 @[simp] lemma inv_fun_algebra_map (M : matrix n n R) :
-  inv_fun R A n (λ i j, algebra_map R A (M i j)) = 1 ⊗ₜ M :=
+  inv_fun R A n (M.map (algebra_map R A)) = 1 ⊗ₜ M :=
 begin
   dsimp [inv_fun],
   simp only [algebra.algebra_map_eq_smul_one, smul_tmul, ←tmul_sum, mul_boole],
@@ -133,17 +105,17 @@ end
 
 lemma right_inv (M : matrix n n A) : (to_fun_alg_hom R A n) (inv_fun R A n M) = M :=
 begin
-  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],
+  simp only [inv_fun, alg_hom.map_sum, std_basis_matrix, apply_ite ⇑(algebra_map R A), smul_eq_mul,
+    mul_boole, to_fun_alg_hom_apply, ring_hom.map_zero, ring_hom.map_one, matrix.map, pi.smul_def],
   convert finset.sum_product, apply matrix_eq_sum_std_basis,
 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 :=
 begin
-  apply tensor_product.induction_on M,
+  induction M using tensor_product.induction_on with a m x y hx hy,
+  { simp, },
   { simp, },
-  { intros a m, simp, },
-  { intros x y hx hy, simp [alg_hom.map_sum, hx, hy], },
+  { simp [alg_hom.map_sum, hx, hy], },
 end
 
 /--