feat(data/matrix): add matrix.map and supporting lemmas (#3352)

As [requested](https://github.com/leanprover-community/mathlib/pull/3276/files#r452366674).



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/data/matrix/basic.lean

@@ -15,10 +15,11 @@ open_locale big_operators
 def matrix (m n : Type u) [fintype m] [fintype n] (α : Type v) : Type (max u v) :=
 m → n → α
 
-namespace matrix
 variables {l m n o : Type u} [fintype l] [fintype m] [fintype n] [fintype o]
 variables {α : Type v}
 
+namespace matrix
+
 section ext
 variables {M N : matrix m n α}
 
@@ -30,6 +31,13 @@ ext_iff.mp
 
 end ext
 
+/-- Apply a function to each matrix entry. -/
+def map (M : matrix m n α) {β : Type w} (f : α → β) : matrix m n β := λ i j, f (M i j)
+
+@[simp]
+lemma map_apply {M : matrix m n α} {β : Type w} {f : α → β} {i : m} {j : n} :
+  M.map f i j = f (M i j) := rfl
+
 def transpose (M : matrix m n α) : matrix n m α
 | x y := M y x
 
@@ -56,6 +64,29 @@ instance [add_comm_group α] : add_comm_group (matrix m n α) := pi.add_comm_gro
 @[simp] theorem neg_val [has_neg α] (M : matrix m n α) (i j) : (- M) i j = - M i j := rfl
 @[simp] theorem add_val [has_add α] (M N : matrix m n α) (i j) : (M + N) i j = M i j + N i j := rfl
 
+@[simp] lemma map_zero [has_zero α] {β : Type w} [has_zero β] {f : α → β} (h : f 0 = 0) :
+  (0 : matrix m n α).map f = 0 :=
+by { ext, simp [h], }
+
+lemma map_add [add_monoid α] {β : Type w} [add_monoid β] (f : α →+ β)
+  (M N : matrix m n α) : (M + N).map f = M.map f + N.map f :=
+by { ext, simp, }
+
+end matrix
+
+def add_monoid_hom.map_matrix [add_monoid α] {β : Type w} [add_monoid β] (f : α →+ β) :
+  matrix m n α →+ matrix m n β :=
+{ to_fun := λ M, M.map f,
+  map_zero' := by simp,
+  map_add' := matrix.map_add f, }
+
+@[simp] lemma add_monoid_hom.map_matrix_apply [add_monoid α] {β : Type w} [add_monoid β]
+  (f : α →+ β) (M : matrix m n α) : f.map_matrix M = M.map f := rfl
+
+open_locale matrix
+
+namespace matrix
+
 section diagonal
 variables [decidable_eq n]
 
@@ -88,6 +119,11 @@ end
   diagonal d₁ + diagonal d₂ = diagonal (λ i, d₁ i + d₂ i) :=
 by ext i j; by_cases h : i = j; simp [h]
 
+@[simp] lemma diagonal_map {β : Type w} [has_zero α] [has_zero β]
+  {f : α → β} (h : f 0 = 0) {d : n → α} :
+  (diagonal d).map f = diagonal (λ m, f (d m)) :=
+by { ext, simp only [diagonal, map_apply], split_ifs; simp [h], }
+
 section one
 variables [has_zero α] [has_one α]
 
@@ -105,6 +141,11 @@ diagonal_val_ne
 theorem one_val_ne' {i j} : j ≠ i → (1 : matrix n n α) i j = 0 :=
 diagonal_val_ne'
 
+@[simp] lemma one_map {β : Type w} [has_zero β] [has_one β]
+  {f : α → β} (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
+  (1 : matrix n n α).map f = (1 : matrix n n β) :=
+by { ext, simp only [one_val, map_apply], split_ifs; simp [h₀, h₁], }
+
 end one
 
 section numeral
@@ -284,6 +325,11 @@ theorem diagonal_mul_diagonal' [decidable_eq n] (d₁ d₂ : n → α) :
   diagonal d₁ * diagonal d₂ = diagonal (λ i, d₁ i * d₂ i) :=
 diagonal_mul_diagonal _ _
 
+lemma map_mul {L : matrix m n α} {M : matrix n o α}
+  {β : Type w} [semiring β] {f : α →+* β} :
+(L ⬝ M).map f = L.map f ⬝ M.map f :=
+by { ext, simp [mul_val, ring_hom.map_sum], }
+
 lemma is_add_monoid_hom_mul_left (M : matrix l m α) :
   is_add_monoid_hom (λ x : matrix m n α, M ⬝ x) :=
 { to_is_add_hom := ⟨matrix.mul_add _⟩, map_zero := matrix.mul_zero _ }
@@ -312,6 +358,22 @@ rfl
 
 end semiring
 
+end matrix
+
+def ring_hom.map_matrix [decidable_eq m] [semiring α] {β : Type w} [semiring β] (f : α →+* β) :
+  matrix m m α →+* matrix m m β :=
+{ to_fun := λ M, M.map f,
+  map_one' := by simp,
+  map_mul' := λ L M, matrix.map_mul,
+  ..(f.to_add_monoid_hom).map_matrix }
+
+@[simp] lemma ring_hom.map_matrix_apply [decidable_eq m] [semiring α] {β : Type w} [semiring β]
+  (f : α →+* β) (M : matrix m m α) : f.map_matrix M = M.map f := rfl
+
+open_locale matrix
+
+namespace matrix
+
 section ring
 variables [ring α]
 
@@ -478,7 +540,7 @@ begin
 end
 
 
-lemma matrix_eq_sum_elementary (x : matrix n m α) :
+lemma matrix_eq_sum_std_basis (x : matrix n m α) :
 x = ∑ (i : n) (j : m), std_basis_matrix i j (x i j) :=
 begin
   ext, iterate 2 {rw finset.sum_apply},
@@ -495,7 +557,7 @@ end
 -- this is not completely trivial because we are indexing by two types, instead of one
 
 -- TODO: add `std_basis_vec`
-lemma elementary_eq_basis_mul_basis (i : m) (j : n) :
+lemma std_basis_eq_basis_mul_basis (i : m) (j : n) :
 std_basis_matrix i j 1 = vec_mul_vec (λ i', ite (i = i') 1 0) (λ j', ite (j = j') 1 0) :=
 begin
   ext, norm_num [std_basis_matrix, vec_mul_vec],
@@ -506,25 +568,25 @@ end
   {X : Type*} [semiring X] {M : matrix n n X → Prop} (m : matrix n n X)
   (h_zero : M 0)
   (h_add : ∀p q, M p → M q → M (p + q))
-  (h_elementary : ∀ i j x, M (std_basis_matrix i j x)) :
+  (h_std_basis : ∀ i j x, M (std_basis_matrix i j x)) :
   M m :=
 begin
-  rw [matrix_eq_sum_elementary m, ← finset.sum_product'],
+  rw [matrix_eq_sum_std_basis m, ← finset.sum_product'],
   apply finset.sum_induction _ _ h_add h_zero,
-  { intros, apply h_elementary, }
+  { intros, apply h_std_basis, }
 end
 
 @[elab_as_eliminator] protected lemma induction_on
   [nonempty n] {X : Type*} [semiring X] {M : matrix n n X → Prop} (m : matrix n n X)
   (h_add : ∀p q, M p → M q → M (p + q))
-  (h_elementary : ∀ i j x, M (std_basis_matrix i j x)) :
+  (h_std_basis : ∀ i j x, M (std_basis_matrix i j x)) :
   M m :=
 matrix.induction_on' m
 begin
   have i : n := classical.choice (by assumption),
-  simpa using h_elementary i i 0,
+  simpa using h_std_basis i i 0,
 end
-h_add h_elementary
+h_add h_std_basis
 
 end semiring
 
@@ -577,25 +639,28 @@ end
   (M + N)ᵀ = Mᵀ + Nᵀ  :=
 by { ext i j, simp }
 
-@[simp] lemma transpose_sub [add_comm_group α] (M : matrix m n α) (N : matrix m n α) :
+@[simp] lemma transpose_sub [add_group α] (M : matrix m n α) (N : matrix m n α) :
   (M - N)ᵀ = Mᵀ - Nᵀ  :=
 by { ext i j, simp }
 
-@[simp] lemma transpose_mul [comm_ring α] (M : matrix m n α) (N : matrix n l α) :
+@[simp] lemma transpose_mul [comm_semiring α] (M : matrix m n α) (N : matrix n l α) :
   (M ⬝ N)ᵀ = Nᵀ ⬝ Mᵀ  :=
 begin
   ext i j,
   apply dot_product_comm
 end
 
-@[simp] lemma transpose_smul [comm_ring α] (c : α)(M : matrix m n α) :
+@[simp] lemma transpose_smul [semiring α] (c : α) (M : matrix m n α) :
   (c • M)ᵀ = c • Mᵀ :=
 by { ext i j, refl }
 
-@[simp] lemma transpose_neg [comm_ring α] (M : matrix m n α) :
+@[simp] lemma transpose_neg [has_neg α] (M : matrix m n α) :
   (- M)ᵀ = - Mᵀ  :=
 by ext i j; refl
 
+lemma transpose_map {β : Type w} {f : α → β} {M : matrix m n α} : Mᵀ.map f = (M.map f)ᵀ :=
+by { ext, refl }
+
 end transpose
 
 def minor (A : matrix m n α) (row : l → m) (col : o → n) : matrix l o α :=
@@ -672,8 +737,7 @@ end row_col
 end matrix
 
 namespace ring_hom
-variables {α β : Type*} [semiring α] [semiring β]
-variables {m n o : Type u} [fintype m] [fintype n] [fintype o]
+variables {β : Type*} [semiring α] [semiring β]
 
 lemma map_matrix_mul (M : matrix m n α) (N : matrix n o α) (i : m) (j : o) (f : α →+* β) :
   f (matrix.mul M N i j) = matrix.mul (λ i j, f (M i j)) (λ i j, f (N i j)) i j :=

src/ring_theory/matrix_algebra.lean

@@ -141,15 +141,15 @@ begin
   dsimp [inv_fun],
   simp only [algebra.algebra_map_eq_smul_one, smul_tmul, ←tmul_sum, mul_boole],
   congr,
-  conv_rhs {rw matrix_eq_sum_elementary M},
+  conv_rhs {rw matrix_eq_sum_std_basis M},
   convert finset.sum_product, simp,
 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],
-  convert finset.sum_product, apply matrix_eq_sum_elementary,
+  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 :=
@@ -188,7 +188,7 @@ open matrix_equiv_tensor
     ∑ (p : n × n), M p.1 p.2 ⊗ₜ (std_basis_matrix p.1 p.2 1) :=
 rfl
 
-@[simp] lemma matrix_equiv_tensor_apply_elementary (i j : n) (x : A):
+@[simp] lemma matrix_equiv_tensor_apply_std_basis (i j : n) (x : A):
   matrix_equiv_tensor R A n (std_basis_matrix i j x) =
     x ⊗ₜ (std_basis_matrix i j 1) :=
 begin

src/ring_theory/polynomial_algebra.lean

@@ -276,7 +276,7 @@ lemma mat_poly_equiv_coeff_apply_aux_1 (i j : n) (k : ℕ) (x : R) :
     monomial k (std_basis_matrix i j x) :=
 begin
   simp only [mat_poly_equiv, alg_equiv.trans_apply,
-    matrix_equiv_tensor_apply_elementary],
+    matrix_equiv_tensor_apply_std_basis],
   apply (poly_equiv_tensor R (matrix n n R)).injective,
   simp only [alg_equiv.apply_symm_apply],
   convert algebra.tensor_product.comm_tmul _ _ _ _ _,