feat(ring_theory/matrix): diagonal matrices

Joint work with Johan Commelin

ring_theory/matrix.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Ellen Arlt. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro
+Authors: Ellen Arlt, Blair Shi, Sean Leather, Mario Carneiro, Johan Commelin
 
 Matrices
 -/
@@ -37,22 +37,42 @@ instance : has_zero (matrix m n α) := ⟨λ _ _, 0⟩
 
 end zero
 
+section diagonal
+variables [decidable_eq n]
+
+def diagonal [has_zero α] (d : n → α) : matrix n n α := λ i j, if i = j then d i else 0
+
+@[simp] theorem diagonal_val_eq [has_zero α] {d : n → α} (i : n) : (diagonal d) i i = d i :=
+by simp [diagonal]
+
+@[simp] theorem diagonal_val_ne [has_zero α] {d : n → α} {i j : n} (h : i ≠ j) :
+  (diagonal d) i j = 0 := by simp [diagonal, h]
+
+theorem diagonal_val_ne' [has_zero α] {d : n → α} {i j : n} (h : j ≠ i) :
+  (diagonal d) i j = 0 := diagonal_val_ne h.symm
+
+@[simp] theorem diagonal_zero [has_zero α] : (diagonal (λ _, 0) : matrix n n α) = 0 :=
+by simp [diagonal]; refl
+
 section one
-variables [decidable_eq n] [has_zero α] [has_one α]
+variables [has_zero α] [has_one α]
 
-instance : has_one (matrix n n α) := ⟨λ i j, if i = j then 1 else 0⟩
+instance : has_one (matrix n n α) := ⟨diagonal (λ _, 1)⟩
+
+@[simp] theorem diagonal_one : (diagonal (λ _, 1) : matrix n n α) = 1 := rfl
 
 theorem one_val {i j} : (1 : matrix n n α) i j = if i = j then 1 else 0 := rfl
 
-@[simp] theorem one_val_eq (i) : (1 : matrix n n α) i i = 1 := by simp [one_val]
+@[simp] theorem one_val_eq (i) : (1 : matrix n n α) i i = 1 := diagonal_val_eq i
 
-@[simp] theorem one_val_ne {i j} (h : i ≠ j) : (1 : matrix n n α) i j = 0 :=
-by simp [one_val, h]
+@[simp] theorem one_val_ne {i j} : i ≠ j → (1 : matrix n n α) i j = 0 :=
+diagonal_val_ne
 
-theorem one_val_ne' {i j} (h : j ≠ i) : (1 : matrix n n α) i j = 0 :=
-one_val_ne h.symm
+theorem one_val_ne' {i j} : j ≠ i → (1 : matrix n n α) i j = 0 :=
+diagonal_val_ne'
 
 end one
+end diagonal
 
 section neg
 variables [has_neg α]
@@ -84,19 +104,28 @@ instance [add_monoid α] : add_monoid (matrix m n α) :=
   add_zero := by intros; ext; simp,
   ..matrix.add_semigroup }
 
+@[simp] theorem diagonal_add [decidable_eq n] [add_monoid α] (d₁ d₂ : n → α) :
+  diagonal d₁ + diagonal d₂ = diagonal (λ i, d₁ i + d₂ i) :=
+by ext i j; by_cases i = j; simp [h]
+
 instance [add_comm_monoid α] : add_comm_monoid (matrix m n α) :=
 { ..matrix.add_monoid, ..matrix.add_comm_semigroup }
 
 protected def mul [has_mul α] [add_comm_monoid α] (M : matrix l m α) (N : matrix m n α) :
   matrix l n α :=
 λ i k, finset.univ.sum (λ j, M i j * N j k)
 
-@[simp] theorem mul_val [has_mul α] [add_comm_monoid α] {M : matrix l m α} {N : matrix m n α} {i k} :
+theorem mul_val [has_mul α] [add_comm_monoid α] {M : matrix l m α} {N : matrix m n α} {i k} :
   (M.mul N) i k = finset.univ.sum (λ j, M i j * N j k) := rfl
 
+local attribute [simp] mul_val
+
 instance [has_mul α] [add_comm_monoid α] : has_mul (matrix n n α) := ⟨matrix.mul⟩
 
-@[simp] theorem mul_val' [has_mul α] [add_comm_monoid α] {M N : matrix n n α} {i k} :
+@[simp] theorem mul_eq_mul [has_mul α] [add_comm_monoid α] (M N : matrix n n α) :
+  M * N = M.mul N := rfl
+
+theorem mul_val' [has_mul α] [add_comm_monoid α] {M N : matrix n n α} {i k} :
   (M * N) i k = finset.univ.sum (λ j, M i j * N j k) := rfl
 
 section semigroup
@@ -113,27 +142,15 @@ instance : semigroup (matrix n n α) :=
 
 end semigroup
 
-section monoid
-variables [decidable_eq n] [decidable_eq m] [semiring α]
-
-protected theorem one_mul (M : matrix n m α) : (1 : matrix n n α).mul M = M :=
-by ext i j; simp; rw finset.sum_eq_single i; simp [one_val_ne'] {contextual := tt}
-
-protected theorem mul_one (M : matrix n m α) : M.mul (1 : matrix m m α) = M :=
-by ext i j; simp; rw finset.sum_eq_single j; simp {contextual := tt}
-
-instance : monoid (matrix n n α) :=
-{ one_mul := matrix.one_mul,
-  mul_one := matrix.mul_one,
-  ..matrix.has_one, ..matrix.semigroup }
-
-end monoid
-
 instance [add_group α] : add_group (matrix m n α) :=
 { zero := 0, add := (+), neg := has_neg.neg,
   add_left_neg := by intros; ext; simp,
   ..matrix.add_monoid }
 
+@[simp] theorem diagonal_neg [decidable_eq n] [add_group α] (d : n → α) :
+  -diagonal d = diagonal (λ i, -d i) :=
+by ext i j; by_cases i = j; simp [h]
+
 instance [add_comm_group α] : add_comm_group (matrix m n α) :=
 { ..matrix.add_group, ..matrix.add_comm_monoid }
 
@@ -152,14 +169,41 @@ by ext i j; simp [finset.sum_add_distrib, mul_add]
 theorem add_mul (L M : matrix m m α) (N : matrix m n α) : (L + M).mul N = L.mul N + M.mul N :=
 by ext i j; simp [finset.sum_add_distrib, add_mul]
 
-instance [decidable_eq n] [semiring α] : semiring (matrix n n α) :=
+@[simp] theorem diagonal_mul [decidable_eq m]
+  (d : m → α) (M : matrix m n α) (i j) : (diagonal d).mul M i j = d i * M i j :=
+by simp; rw finset.sum_eq_single i; simp [diagonal_val_ne'] {contextual := tt}
+
+@[simp] theorem mul_diagonal [decidable_eq n]
+  (d : n → α) (M : matrix m n α) (i j) : M.mul (diagonal d) i j = M i j * d j :=
+by simp; rw finset.sum_eq_single j; simp {contextual := tt}
+
+protected theorem one_mul [decidable_eq m] (M : matrix m n α) : (1 : matrix m m α).mul M = M :=
+by ext i j; rw [← diagonal_one, diagonal_mul, one_mul]
+
+protected theorem mul_one [decidable_eq n] (M : matrix m n α) : M.mul (1 : matrix n n α) = M :=
+by ext i j; rw [← diagonal_one, mul_diagonal, mul_one]
+
+instance [decidable_eq n] : monoid (matrix n n α) :=
+{ one_mul := matrix.one_mul,
+  mul_one := matrix.mul_one,
+  ..matrix.has_one, ..matrix.semigroup }
+
+instance [decidable_eq n] : semiring (matrix n n α) :=
 { mul_zero := mul_zero,
   zero_mul := zero_mul,
   left_distrib := mul_add,
   right_distrib := add_mul,
   ..matrix.add_comm_monoid,
   ..matrix.monoid }
 
+@[simp] theorem diagonal_mul_diagonal' [decidable_eq n] (d₁ d₂ : n → α) :
+  (diagonal d₁).mul (diagonal d₂) = diagonal (λ i, d₁ i * d₂ i) :=
+by ext i j; by_cases i = j; simp [h]
+
+theorem diagonal_mul_diagonal [decidable_eq n] (d₁ d₂ : n → α) :
+  diagonal d₁ * diagonal d₂ = diagonal (λ i, d₁ i * d₂ i) :=
+diagonal_mul_diagonal' _ _
+
 end semiring
 
 instance [decidable_eq n] [ring α] : ring (matrix n n α) :=