From 497e692b946d93906900bb33a51fd243e7649406 Mon Sep 17 00:00:00 2001
From: Oliver Nash <oliver.nash@gmail.com>
Date: Sun, 26 Jan 2020 21:08:12 +0000
Subject: [PATCH] feat(linear_algebra/matrix): define the trace of a square
 matrix (#1883)

* feat(linear_algebra/matrix): define the trace of a square matrix

* Move ring carrier to correct universe

* Add lemma trace_one, and define diag as linear map

* Define diag and trace solely as linear functions

* Diag and trace for module-valued matrices

* Fix cyclic import

* Rename matrix.mul_sum' --> matrix.smul_sum

Co-Authored-By: Johan Commelin <johan@commelin.net>

* Trigger CI

Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
---
 src/data/matrix/basic.lean     |  5 +++--
 src/linear_algebra/matrix.lean | 36 +++++++++++++++++++++++++++++++++-
 src/ring_theory/algebra.lean   |  4 ++--
 3 files changed, 40 insertions(+), 5 deletions(-)

diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
index 65815ea356b0b..0b0dd902f5d15 100644
--- a/src/data/matrix/basic.lean
+++ b/src/data/matrix/basic.lean
@@ -8,7 +8,7 @@ Matrices
 import algebra.module algebra.pi_instances
 import data.fintype
 
-universes u v
+universes u v w
 
 def matrix (m n : Type u) [fintype m] [fintype n] (α : Type v) : Type (max u v) :=
 m → n → α
@@ -220,7 +220,8 @@ instance [decidable_eq n] [ring α] : ring (matrix n n α) :=
 { ..matrix.add_comm_group, ..matrix.semiring }
 
 instance [semiring α] : has_scalar α (matrix m n α) := pi.has_scalar
-instance [ring α] : module α (matrix m n α) := pi.module _
+instance {β : Type w} [ring α] [add_comm_group β] [module α β] :
+  module α (matrix m n β) := pi.module _
 
 @[simp] lemma smul_val [semiring α] (a : α) (A : matrix m n α) (i : m) (j : n) : (a • A) i j = a * A i j := rfl
 
diff --git a/src/linear_algebra/matrix.lean b/src/linear_algebra/matrix.lean
index 75e1d5bb07f8a..f1b8719097277 100644
--- a/src/linear_algebra/matrix.lean
+++ b/src/linear_algebra/matrix.lean
@@ -36,7 +36,7 @@ noncomputable theory
 
 open set submodule
 
-universes u v
+universes u v w
 variables {l m n : Type u} [fintype l] [fintype m] [fintype n]
 
 namespace matrix
@@ -187,6 +187,40 @@ end linear_equiv_matrix
 
 namespace matrix
 
+section trace
+
+variables {R : Type v} {M : Type w} [ring R] [add_comm_group M] [module R M]
+
+/--
+The diagonal of a square matrix.
+-/
+def diag : (matrix n n M) →ₗ[R] n → M := {
+  to_fun := λ A i, A i i,
+  add    := by { intros, ext, refl, },
+  smul   := by { intros, ext, refl, } }
+
+@[simp] lemma diag_one [decidable_eq n] :
+  (diag : (matrix n n R) →ₗ[R] n → R) 1 = λ i, 1 := by {
+    dunfold diag, ext, simp [one_val_eq], }
+
+protected lemma smul_sum {α : Type u} {s : finset α} {f : α → M} {c : R} :
+  c • s.sum f = s.sum (λx, c • f x) := (s.sum_hom _).symm
+
+/--
+The trace of a square matrix.
+-/
+def trace : (matrix n n M) →ₗ[R] M := {
+  to_fun := finset.univ.sum ∘ (diag : (matrix n n M) →ₗ[R] n → M),
+  add    := by { intros, apply finset.sum_add_distrib, },
+  smul   := by { intros, simp [matrix.smul_sum], } }
+
+@[simp] lemma trace_one [decidable_eq n] :
+  (trace : (matrix n n R) →ₗ[R] R) 1 = fintype.card n := by {
+    have h : @trace n _ R R _ _ _ 1 = finset.univ.sum (@diag n _ R R _ _ _ 1) := rfl,
+    rw [h, diag_one, finset.sum_const, add_monoid.smul_one], refl, }
+
+end trace
+
 section ring
 
 variables {R : Type v} [comm_ring R]
diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean
index 7dda0a004de8b..2e1722a732211 100644
--- a/src/ring_theory/algebra.lean
+++ b/src/ring_theory/algebra.lean
@@ -156,8 +156,8 @@ set_option class.instance_max_depth 40
 instance matrix_algebra (n : Type u) (R : Type v)
   [fintype n] [decidable_eq n] [comm_ring R] : algebra R (matrix n n R) :=
 { to_fun    := (λ r, r • 1),
-  hom       := { map_one := by simp,
-                 map_mul := by { intros, simp [mul_smul], },
+  hom       := { map_one := by { ext, simp, },
+                 map_mul := by { intros, ext, simp [mul_assoc], },
                  map_add := by { intros, simp [add_smul], } },
   commutes' := by { intros, simp },
   smul_def' := by { intros, simp } }