refactor(data/matrix/basic): merge duplicate algebra structures (#8486)

By putting the algebra instance in the same file as `scalar`, a future patch can probably remove `matrix.scalar` entirely (it's just another spelling of `algebra_map`).

Note that we actually had two instances of `algebra R (matrix n n R)` in different files, and the second one was strictly more general than the first. This removes the less general one.

Moving the imports around like this changes the number of simp lemmas available in downstream files, which can make `simp` slow enough to push a proof into a timeout.

A lot of files were expecting a transitive import of `algebra.algebra.basic` to import `data.fintype.card`, which it no longer does; hence the need to add this import explicitly.

There are no new lemmas or generalizations in this change; the old `matrix_algebra` has been deleted, and everything else has been moved with some variables renamed.

src/algebra/algebra/basic.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import tactic.nth_rewrite
-import data.matrix.basic
 import data.equiv.ring_aut
 import linear_algebra.tensor_product
 import ring_theory.subring
@@ -386,15 +385,6 @@ linear_map.ker_smul _ _ ha
 
 end module
 
-instance matrix_algebra (n : Type u) (R : Type v)
-  [decidable_eq n] [fintype n] [comm_semiring R] : algebra R (matrix n n R) :=
-{ commutes' := by { intros, simp [matrix.scalar], },
-  smul_def' := by { intros, simp [matrix.scalar], },
-  ..(matrix.scalar n) }
-
-@[simp] lemma matrix.algebra_map_eq_smul (n : Type u) {R : Type v} [decidable_eq n] [fintype n]
-  [comm_semiring R] (r : R) : (algebra_map R (matrix n n R)) r = r • 1 := rfl
-
 set_option old_structure_cmd true
 /-- Defining the homomorphism in the category R-Alg. -/
 @[nolint has_inhabited_instance]
@@ -1062,44 +1052,6 @@ end division_ring
 
 end alg_equiv
 
-namespace matrix
-
-/-! ### `matrix` section
-
-Specialize `matrix.one_map` and `matrix.zero_map` to `alg_hom` and `alg_equiv`.
-TODO: there should be a way to avoid restating these for each `foo_hom`.
--/
-
-variables {R A₁ A₂ n : Type*} [fintype n]
-
-section semiring
-
-variables [comm_semiring R] [semiring A₁] [algebra R A₁] [semiring A₂] [algebra R A₂]
-
-/-- A version of `matrix.one_map` where `f` is an `alg_hom`. -/
-@[simp] lemma alg_hom_map_one [decidable_eq n]
-  (f : A₁ →ₐ[R] A₂) : (1 : matrix n n A₁).map f = 1 :=
-map_one _ f.map_zero f.map_one
-
-/-- A version of `matrix.one_map` where `f` is an `alg_equiv`. -/
-@[simp] lemma alg_equiv_map_one [decidable_eq n]
-  (f : A₁ ≃ₐ[R] A₂) : (1 : matrix n n A₁).map f = 1 :=
-map_one _ f.map_zero f.map_one
-
-/-- A version of `matrix.zero_map` where `f` is an `alg_hom`. -/
-@[simp] lemma alg_hom_map_zero
-  (f : A₁ →ₐ[R] A₂) : (0 : matrix n n A₁).map f = 0 :=
-map_zero _ f.map_zero
-
-/-- A version of `matrix.zero_map` where `f` is an `alg_equiv`. -/
-@[simp] lemma alg_equiv_map_zero
-  (f : A₁ ≃ₐ[R] A₂) : (0 : matrix n n A₁).map f = 0 :=
-map_zero _ f.map_zero
-
-end semiring
-
-end matrix
-
 section nat
 
 variables {R : Type*} [semiring R]

src/algebra/lie/weights.lean

@@ -8,6 +8,7 @@ import algebra.lie.tensor_product
 import algebra.lie.character
 import algebra.lie.cartan_subalgebra
 import linear_algebra.eigenspace
+import ring_theory.tensor_product
 
 /-!
 # Weights and roots of Lie modules and Lie algebras

src/category_theory/preadditive/Mat.lean

@@ -175,16 +175,18 @@ instance has_finite_biproducts : has_finite_biproducts (Mat_ C) :=
         simp only [if_congr, if_true, dif_ctx_congr, finset.sum_dite_irrel, finset.mem_univ,
           finset.sum_const_zero, finset.sum_congr, finset.sum_dite_eq'],
         split_ifs with h h',
-        { substs h h', simp, },
-        { subst h, simp at h', simp [h'], },
+        { substs h h',
+          simp only [category_theory.eq_to_hom_refl, category_theory.Mat_.id_apply_self], },
+        { subst h,
+          simp only [id_apply_of_ne _ _ _ h', category_theory.eq_to_hom_refl], },
         { refl, },
       end, }
     begin
       funext i₁,
       dsimp at i₁ ⊢,
       rcases i₁ with ⟨j₁, i₁⟩,
       -- I'm not sure why we can't just `simp` by `finset.sum_apply`: something doesn't quite match
-      convert finset.sum_apply _ _ _,
+      convert finset.sum_apply _ _ _ using 1,
       { refl, },
       { apply heq_of_eq,
         symmetry,

src/data/matrix/basic.lean

@@ -8,6 +8,7 @@ import algebra.module.pi
 import algebra.module.linear_map
 import algebra.big_operators.ring
 import algebra.star.pi
+import algebra.algebra.basic
 import data.equiv.ring
 import data.fintype.card
 import data.matrix.dmatrix
@@ -517,6 +518,32 @@ map_zero _ f.map_zero
   (0 : matrix n n α).map f = 0 :=
 map_zero _ f.map_zero
 
+section algebra
+
+variables [comm_semiring R] [semiring α] [algebra R α] [semiring β] [algebra R β]
+
+/-- A version of `matrix.map_one` where `f` is an `alg_hom`. -/
+@[simp] lemma alg_hom_map_one [decidable_eq n]
+  (f : α →ₐ[R] β) : (1 : matrix n n α).map f = 1 :=
+map_one _ f.map_zero f.map_one
+
+/-- A version of `matrix.map_one` where `f` is an `alg_equiv`. -/
+@[simp] lemma alg_equiv_map_one [decidable_eq n]
+  (f : α ≃ₐ[R] β) : (1 : matrix n n α).map f = 1 :=
+map_one _ f.map_zero f.map_one
+
+/-- A version of `matrix.zero_map` where `f` is an `alg_hom`. -/
+@[simp] lemma alg_hom_map_zero
+  (f : α →ₐ[R] β) : (0 : matrix n n α).map f = 0 :=
+map_zero _ f.map_zero
+
+/-- A version of `matrix.zero_map` where `f` is an `alg_equiv`. -/
+@[simp] lemma alg_equiv_map_zero
+  (f : α ≃ₐ[R] β) : (0 : matrix n n α).map f = 0 :=
+map_zero _ f.map_zero
+
+end algebra
+
 end homs
 
 end matrix
@@ -800,6 +827,27 @@ by simp [commute, semiconj_by]
 
 end comm_semiring
 
+section algebra
+variables [comm_semiring R] [semiring α] [algebra R α] [decidable_eq n]
+
+instance : algebra R (matrix n n α) :=
+{ commutes' := λ r x, begin
+    ext, simp [matrix.scalar, matrix.mul_apply, matrix.one_apply, algebra.commutes, smul_ite], end,
+  smul_def' := λ r x, begin ext, simp [matrix.scalar, algebra.smul_def'' r], end,
+  ..((matrix.scalar n).comp (algebra_map R α)) }
+
+lemma algebra_map_matrix_apply {r : R} {i j : n} :
+  algebra_map R (matrix n n α) r i j = if i = j then algebra_map R α r else 0 :=
+begin
+  dsimp [algebra_map, algebra.to_ring_hom, matrix.scalar],
+  split_ifs with h; simp [h, matrix.one_apply_ne],
+end
+
+@[simp] lemma algebra_map_eq_smul (r : R) :
+  algebra_map R (matrix n n R) r = r • (1 : matrix n n R) := rfl
+
+end algebra
+
 /-- For two vectors `w` and `v`, `vec_mul_vec w v i j` is defined to be `w i * v j`.
     Put another way, `vec_mul_vec w v` is exactly `col w ⬝ row v`. -/
 def vec_mul_vec [has_mul α] (w : m → α) (v : n → α) : matrix m n α

src/group_theory/specific_groups/dihedral.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Shing Tak Lam. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Shing Tak Lam
 -/
+import data.fintype.card
 import data.zmod.basic
 import group_theory.order_of_element
 

src/linear_algebra/determinant.lean

@@ -11,7 +11,6 @@ import linear_algebra.matrix.reindex
 import linear_algebra.multilinear
 import linear_algebra.dual
 import ring_theory.algebra_tower
-import ring_theory.matrix_algebra
 
 /-!
 # Determinant of families of vectors

src/linear_algebra/free_module_pid.lean

@@ -259,8 +259,6 @@ open submodule.is_principal set submodule
 variables {ι : Type*} {R : Type*} [integral_domain R] [is_principal_ideal_ring R]
 variables {M : Type*} [add_comm_group M] [module R M] {b : ι → M}
 
-open_locale matrix
-
 /-- A submodule of a free `R`-module of finite rank is also a free `R`-module of finite rank,
 if `R` is a principal ideal domain. -/
 noncomputable def submodule.basis_of_pid {ι : Type*} [fintype ι]

src/linear_algebra/matrix/finite_dimensional.lean

@@ -3,6 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
+import data.matrix.basic
 import linear_algebra.finite_dimensional
 
 /-!

src/linear_algebra/matrix/to_lin.lean

@@ -7,7 +7,6 @@ import data.matrix.block
 import linear_algebra.matrix.finite_dimensional
 import linear_algebra.std_basis
 import ring_theory.algebra_tower
-import ring_theory.matrix_algebra
 
 /-!
 # Linear maps and matrices

src/linear_algebra/multilinear.lean

@@ -6,6 +6,8 @@ Authors: Sébastien Gouëzel
 import linear_algebra.basic
 import algebra.algebra.basic
 import algebra.big_operators.order
+import algebra.big_operators.ring
+import data.fintype.card
 import data.fintype.sort
 
 /-!

src/ring_theory/matrix_algebra.lean

@@ -3,11 +3,11 @@ 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 ring_theory.tensor_product
 
 /-!
-We provide the `R`-algebra structure on `matrix n n A` when `A` is an `R`-algebra,
-and show `matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R)`.
+We show `matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R)`.
 -/
 
 universes u v w
@@ -23,22 +23,6 @@ variables {R : Type u} [comm_semiring R]
 variables {A : Type v} [semiring A] [algebra R A]
 variables {n : Type w} [fintype n]
 
-section
-variables [decidable_eq n]
-
-instance : algebra R (matrix n n A) :=
-{ commutes' := λ r x, begin
-    ext, simp [matrix.scalar, matrix.mul_apply, matrix.one_apply, algebra.commutes, smul_ite], end,
-  smul_def' := λ r x, begin ext, simp [matrix.scalar, algebra.smul_def'' r], end,
-  ..((matrix.scalar n).comp (algebra_map R A)) }
-
-lemma algebra_map_matrix_apply {r : R} {i j : n} :
-  algebra_map R (matrix n n A) r i j = if i = j then algebra_map R A r else 0 :=
-begin
-  dsimp [algebra_map, algebra.to_ring_hom, matrix.scalar],
-  split_ifs with h; simp [h, matrix.one_apply_ne],
-end
-end
 
 variables (R A n)
 namespace matrix_equiv_tensor

src/ring_theory/polynomial/symmetric.lean

@@ -3,6 +3,7 @@ Copyright (c) 2020 Hanting Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hanting Zhang, Johan Commelin
 -/
+import data.fintype.card
 import data.mv_polynomial.rename
 import data.mv_polynomial.comm_ring
 import algebra.algebra.subalgebra

src/ring_theory/witt_vector/witt_polynomial.lean

@@ -5,6 +5,7 @@ Authors: Johan Commelin, Robert Y. Lewis
 -/
 
 import algebra.char_p.invertible
+import data.fintype.card
 import data.mv_polynomial.variables
 import data.mv_polynomial.comm_ring
 import data.mv_polynomial.expand

src/topology/algebra/infinite_sum.lean

@@ -8,6 +8,7 @@ import topology.instances.real
 import topology.algebra.module
 import algebra.indicator_function
 import data.equiv.encodable.lattice
+import data.fintype.card
 import data.nat.parity
 import order.filter.at_top_bot