feat(algebra/algebra/basic): lemmas about alg_hom and scalar towers (#…

…9249)

Co-authored-by: Chris Hughes <chrishughes24@gmail.com>

src/algebra/algebra/tower.lean

@@ -46,7 +46,7 @@ def lsmul : A →ₐ[R] module.End R M :=
 
 @[simp] lemma lsmul_coe (a : A) : (lsmul R M a : M → M) = (•) a := rfl
 
-@[simp] lemma lmul_algebra_map (x : R) :
+lemma lmul_algebra_map (x : R) :
   lmul R A (algebra_map R A x) = algebra.lsmul R A x :=
 eq.symm $ linear_map.ext $ smul_def'' x
 
@@ -123,6 +123,18 @@ ring_hom.ext $ λ _, rfl
 @[simp] lemma coe_to_alg_hom' : (to_alg_hom R S A : S → A) = algebra_map S A :=
 rfl
 
+variables {R S A B}
+
+@[simp, priority 900] lemma _root_.alg_hom.commutes_of_tower (f : A →ₐ[S] B) (r : R) :
+  f (algebra_map R A r) = algebra_map R B r :=
+by rw [algebra_map_apply R S A r, f.commutes, ← algebra_map_apply R S B]
+
+variables (R)
+
+@[simp, priority 900] lemma _root_.alg_hom.comp_algebra_map_of_tower (f : A →ₐ[S] B) :
+  (f : A →+* B).comp (algebra_map R A) = algebra_map R B :=
+ring_hom.ext f.commutes_of_tower
+
 variables (R) {S A B}
 
 -- conflicts with is_scalar_tower.subalgebra

src/linear_algebra/matrix/to_lin.lean

@@ -366,7 +366,7 @@ lemma linear_map.to_matrix_mul (f g : M₁ →ₗ[R] M₁) :
 by { rw [show (@has_mul.mul (M₁ →ₗ[R] M₁) _) = linear_map.comp, from rfl,
          linear_map.to_matrix_comp v₁ v₁ v₁ f g] }
 
-@[simp] lemma linear_map.to_matrix_algebra_map (x : R) : 
+@[simp] lemma linear_map.to_matrix_algebra_map (x : R) :
   linear_map.to_matrix v₁ v₁ (algebra_map R (module.End R M₁) x) = scalar n x :=
 by simp [module.algebra_map_End_eq_smul_id, linear_map.to_matrix_id]