refactor(linear_algebra/matrix/trace): unbundle matrix.diag (#13687)

The bundling makes it awkward to work with, as the base ring has to be specified even though it doesn't affect the computation.
This brings it in line with `matrix.diagonal`.

The bundled version is now available as `matrix.diag_linear_map`.

This adds a handful of missing lemmas about `diag` inspired by those about `diagonal`; almost all of which are just `rfl`.

archive/100-theorems-list/83_friendship_graphs.lean

@@ -256,7 +256,7 @@ begin
   -- but the trace is 1 mod p when computed the other way
   rw adj_matrix_pow_mod_p_of_regular hG dmod hd hp2,
   dunfold fintype.card at Vmod,
-  simp only [matrix.trace, diag_apply, mul_one, nsmul_eq_mul, linear_map.coe_mk, sum_const],
+  simp only [matrix.trace, matrix.diag, mul_one, nsmul_eq_mul, linear_map.coe_mk, sum_const],
   rw [Vmod, ← nat.cast_one, zmod.nat_coe_zmod_eq_zero_iff_dvd, nat.dvd_one,
     nat.min_fac_eq_one_iff],
   linarith,

src/analysis/matrix.lean

@@ -85,7 +85,7 @@ begin
   refine le_antisymm (finset.sup_le $ λ j hj, _) _,
   { obtain rfl | hij := eq_or_ne i j,
     { rw diagonal_apply_eq },
-    { rw [diagonal_apply_ne hij, nnnorm_zero],
+    { rw [diagonal_apply_ne _ hij, nnnorm_zero],
       exact zero_le _ }, },
   { refine eq.trans_le _ (finset.le_sup (finset.mem_univ i)),
     rw diagonal_apply_eq }

src/data/matrix/basic.lean

@@ -204,14 +204,14 @@ Note that bundled versions exist as:
 def diagonal [has_zero α] (d : n → α) : matrix n n α
 | i j := if i = j then d i else 0
 
-@[simp] theorem diagonal_apply_eq [has_zero α] {d : n → α} (i : n) : (diagonal d) i i = d i :=
+@[simp] theorem diagonal_apply_eq [has_zero α] (d : n → α) (i : n) : (diagonal d) i i = d i :=
 by simp [diagonal]
 
-@[simp] theorem diagonal_apply_ne [has_zero α] {d : n → α} {i j : n} (h : i ≠ j) :
+@[simp] theorem diagonal_apply_ne [has_zero α] (d : n → α) {i j : n} (h : i ≠ j) :
   (diagonal d) i j = 0 := by simp [diagonal, h]
 
-theorem diagonal_apply_ne' [has_zero α] {d : n → α} {i j : n} (h : j ≠ i) :
-  (diagonal d) i j = 0 := diagonal_apply_ne h.symm
+theorem diagonal_apply_ne' [has_zero α] (d : n → α) {i j : n} (h : j ≠ i) :
+  (diagonal d) i j = 0 := diagonal_apply_ne d h.symm
 
 lemma diagonal_injective [has_zero α] : function.injective (diagonal : (n → α) → matrix n n α) :=
 λ d₁ d₂ h, funext $ λ i, by simpa using matrix.ext_iff.mpr h i i
@@ -225,7 +225,7 @@ begin
   ext i j,
   by_cases h : i = j,
   { simp [h, transpose] },
-  { simp [h, transpose, diagonal_apply_ne' h] }
+  { simp [h, transpose, diagonal_apply_ne' _ h] }
 end
 
 @[simp] theorem diagonal_add [add_zero_class α] (d₁ d₂ : n → α) :
@@ -277,13 +277,13 @@ instance : has_one (matrix n n α) := ⟨diagonal (λ _, 1)⟩
 
 theorem one_apply {i j} : (1 : matrix n n α) i j = if i = j then 1 else 0 := rfl
 
-@[simp] theorem one_apply_eq (i) : (1 : matrix n n α) i i = 1 := diagonal_apply_eq i
+@[simp] theorem one_apply_eq (i) : (1 : matrix n n α) i i = 1 := diagonal_apply_eq _ i
 
 @[simp] theorem one_apply_ne {i j} : i ≠ j → (1 : matrix n n α) i j = 0 :=
-diagonal_apply_ne
+diagonal_apply_ne _
 
 theorem one_apply_ne' {i j} : j ≠ i → (1 : matrix n n α) i j = 0 :=
-diagonal_apply_ne'
+diagonal_apply_ne' _
 
 @[simp] lemma map_one [has_zero β] [has_one β]
   (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) :
@@ -320,6 +320,56 @@ end numeral
 
 end diagonal
 
+section diag
+
+/-- The diagonal of a square matrix. -/
+@[simp] def diag (A : matrix n n α) (i : n) : α := A i i
+
+@[simp] lemma diag_diagonal [decidable_eq n] [has_zero α] (a : n → α) : diag (diagonal a) = a :=
+funext $ @diagonal_apply_eq _ _ _ _ a
+
+@[simp] lemma diag_transpose (A : matrix n n α) : diag Aᵀ = diag A := rfl
+
+@[simp] theorem diag_zero [has_zero α] : diag (0 : matrix n n α) = 0 := rfl
+
+@[simp] theorem diag_add [has_add α] (A B : matrix n n α) : diag (A + B) = diag A + diag B := rfl
+
+@[simp] theorem diag_sub [has_sub α] (A B : matrix n n α) : diag (A - B) = diag A - diag B := rfl
+
+@[simp] theorem diag_neg [has_neg α] (A : matrix n n α) : diag (-A) = -diag A := rfl
+
+@[simp] theorem diag_smul [has_scalar R α] (r : R) (A : matrix n n α) : diag (r • A) = r • diag A :=
+rfl
+
+@[simp] theorem diag_one [decidable_eq n] [has_zero α] [has_one α] : diag (1 : matrix n n α) = 1 :=
+diag_diagonal _
+
+variables (n α)
+
+/-- `matrix.diag` as an `add_monoid_hom`. -/
+@[simps]
+def diag_add_monoid_hom [add_zero_class α] : matrix n n α →+ (n → α) :=
+{ to_fun := diag,
+  map_zero' := diag_zero,
+  map_add' := diag_add,}
+
+variables (R)
+
+/-- `matrix.diag` as a `linear_map`. -/
+@[simps]
+def diag_linear_map [semiring R] [add_comm_monoid α] [module R α] : matrix n n α →ₗ[R] (n → α) :=
+{ map_smul' := diag_smul,
+  .. diag_add_monoid_hom n α,}
+
+variables {n α R}
+
+lemma diag_map {f : α → β} {A : matrix n n α} : diag (A.map f) = f ∘ diag A := rfl
+
+@[simp] lemma diag_conj_transpose [add_monoid α] [star_add_monoid α] (A : matrix n n α) :
+  diag Aᴴ = star (diag A) := rfl
+
+end diag
+
 section dot_product
 
 variable [fintype m]
@@ -368,15 +418,15 @@ section non_unital_non_assoc_semiring_decidable
 variables [decidable_eq m] [non_unital_non_assoc_semiring α] (u v w : m → α)
 
 @[simp] lemma diagonal_dot_product (i : m) : diagonal v i ⬝ᵥ w = v i * w i :=
-have ∀ j ≠ i, diagonal v i j * w j = 0 := λ j hij, by simp [diagonal_apply_ne' hij],
+have ∀ j ≠ i, diagonal v i j * w j = 0 := λ j hij, by simp [diagonal_apply_ne' _ hij],
 by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp
 
 @[simp] lemma dot_product_diagonal (i : m) : v ⬝ᵥ diagonal w i = v i * w i :=
-have ∀ j ≠ i, v j * diagonal w i j = 0 := λ j hij, by simp [diagonal_apply_ne' hij],
+have ∀ j ≠ i, v j * diagonal w i j = 0 := λ j hij, by simp [diagonal_apply_ne' _ hij],
 by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp
 
 @[simp] lemma dot_product_diagonal' (i : m) : v ⬝ᵥ (λ j, diagonal w j i) = v i * w i :=
-have ∀ j ≠ i, v j * diagonal w j i = 0 := λ j hij, by simp [diagonal_apply_ne hij],
+have ∀ j ≠ i, v j * diagonal w j i = 0 := λ j hij, by simp [diagonal_apply_ne _ hij],
 by convert finset.sum_eq_single i (λ j _, this j) _ using 1; simp
 
 @[simp] lemma single_dot_product (x : α) (i : m) : pi.single i x ⬝ᵥ v = x * v i :=
@@ -525,6 +575,9 @@ lemma smul_eq_diagonal_mul [fintype m] [decidable_eq m] (M : matrix m n α) (a :
   a • M = diagonal (λ _, a) ⬝ M :=
 by { ext, simp }
 
+@[simp] lemma diag_col_mul_row (a b : n → α) : diag (col a ⬝ row b) = a * b :=
+by { ext, simp [matrix.mul_apply, col, row] }
+
 /-- Left multiplication by a matrix, as an `add_monoid_hom` from matrices to matrices. -/
 @[simps] def add_monoid_hom_mul_left [fintype m] (M : matrix l m α) :
   matrix m n α →+ matrix l n α :=
@@ -1153,7 +1206,7 @@ begin
   unfold has_one.one transpose,
   by_cases i = j,
   { simp only [h, diagonal_apply_eq] },
-  { simp only [diagonal_apply_ne h, diagonal_apply_ne (λ p, h (symm p))] }
+  { simp only [diagonal_apply_ne _ h, diagonal_apply_ne' _ h] }
 end
 
 @[simp] lemma transpose_add [has_add α] (M : matrix m n α) (N : matrix m n α) :
@@ -1392,7 +1445,7 @@ ext $ λ i j, begin
   rw minor_apply,
   by_cases h : i = j,
   { rw [h, diagonal_apply_eq, diagonal_apply_eq], },
-  { rw [diagonal_apply_ne h, diagonal_apply_ne (he.ne h)], },
+  { rw [diagonal_apply_ne _ h, diagonal_apply_ne _ (he.ne h)], },
 end
 
 lemma minor_one [has_zero α] [has_one α] [decidable_eq m] [decidable_eq l] (e : l → m)
@@ -1406,6 +1459,7 @@ lemma minor_mul [fintype n] [fintype o] [has_mul α] [add_comm_monoid α] {p q :
   (M ⬝ N).minor e₁ e₃ = (M.minor e₁ e₂) ⬝ (N.minor e₂ e₃) :=
 ext $ λ _ _, (he₂.sum_comp _).symm
 
+lemma diag_minor (A : matrix m m α) (e : l → m) : diag (A.minor e e) = A.diag ∘ e := rfl
 
 /-! `simp` lemmas for `matrix.minor`s interaction with `matrix.diagonal`, `1`, and `matrix.mul` for
 when the mappings are bundled. -/

src/data/matrix/basis.lean

@@ -121,10 +121,10 @@ section
 
 variables (i j : n) (c : α) (i' j' : n)
 
-@[simp] lemma diag_zero (h : j ≠ i) : diag n α α (std_basis_matrix i j c) = 0 :=
+@[simp] lemma diag_zero (h : j ≠ i) : diag (std_basis_matrix i j c) = 0 :=
 funext $ λ k, if_neg $ λ ⟨e₁, e₂⟩, h (e₂.trans e₁.symm)
 
-@[simp] lemma diag_same : diag n α α (std_basis_matrix i i c) = pi.single i c :=
+@[simp] lemma diag_same : diag (std_basis_matrix i i c) = pi.single i c :=
 by { ext j, by_cases hij : i = j; try {rw hij}; simp [hij] }
 
 variable [fintype n]

src/linear_algebra/matrix/is_diag.lean

@@ -33,22 +33,21 @@ def is_diag [has_zero α] (A : matrix n n α) : Prop := ∀ ⦃i j⦄, i ≠ j 
 
 @[simp] lemma is_diag_diagonal [has_zero α] [decidable_eq n] (d : n → α) :
   (diagonal d).is_diag :=
-λ i j, matrix.diagonal_apply_ne
+λ i j, matrix.diagonal_apply_ne _
 
-/-- Diagonal matrices are generated by `matrix.diagonal`. -/
-lemma is_diag.exists_diagonal [has_zero α] [decidable_eq n] {A : matrix n n α} (h : A.is_diag) :
-  ∃ d, diagonal d = A :=
-begin
-  refine ⟨λ i, A i i, ext $ λ i j, _⟩,
+/-- Diagonal matrices are generated by the `matrix.diagonal` of their `matrix.diag`. -/
+lemma is_diag.diagonal_diag [has_zero α] [decidable_eq n] {A : matrix n n α} (h : A.is_diag) :
+  diagonal (diag A) = A :=
+ext $ λ i j, begin
   obtain rfl | hij := decidable.eq_or_ne i j,
-  { rw diagonal_apply_eq },
-  { rw [diagonal_apply_ne hij, h hij] },
+  { rw [diagonal_apply_eq, diag] },
+  { rw [diagonal_apply_ne _ hij, h hij] },
 end
 
-/-- `matrix.is_diag.exists_diagonal` as an iff. -/
-lemma is_diag_iff_exists_diagonal [has_zero α] [decidable_eq n] (A : matrix n n α) :
-  A.is_diag ↔ (∃ d, diagonal d = A) :=
-⟨is_diag.exists_diagonal, λ ⟨d, hd⟩, hd ▸ is_diag_diagonal d⟩
+/-- `matrix.is_diag.diagonal_diag` as an iff. -/
+lemma is_diag_iff_diagonal_diag [has_zero α] [decidable_eq n] (A : matrix n n α) :
+  A.is_diag ↔ diagonal (diag A) = A :=
+⟨is_diag.diagonal_diag, λ hd, hd ▸ is_diag_diagonal (diag A)⟩
 
 /-- Every matrix indexed by a subsingleton is diagonal. -/
 lemma is_diag_of_subsingleton [has_zero α] [subsingleton n] (A : matrix n n α) : A.is_diag :=

src/linear_algebra/matrix/trace.lean

@@ -31,46 +31,26 @@ universes u v w
 variables {m : Type*} (n : Type*) {p : Type*}
 variables (R : Type*) (M : Type*) [semiring R] [add_comm_monoid 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,
-  map_add'  := by { intros, ext, refl, },
-  map_smul' := by { intros, ext, refl, } }
-
-variables {n} {R} {M}
-
-@[simp] lemma diag_apply (A : matrix n n M) (i : n) : diag n R M A i = A i i := rfl
-
-@[simp] lemma diag_one [decidable_eq n] :
-  diag n R R 1 = λ i, 1 := by { dunfold diag, ext, simp [one_apply_eq] }
-
-@[simp] lemma diag_transpose (A : matrix n n M) : diag n R M Aᵀ = diag n R M A := rfl
-
-@[simp] lemma diag_col_mul_row (a b : n → R) : diag n R R (col a ⬝ row b) = a * b :=
-by { ext, simp [matrix.mul_apply] }
-
 variables (n) (R) (M)
 
 /--
 The trace of a square matrix.
 -/
 def trace [fintype n] : (matrix n n M) →ₗ[R] M :=
-{ to_fun    := λ A, ∑ i, diag n R M A i,
+{ to_fun    := λ A, ∑ i, diag A i,
   map_add'  := by { intros, apply finset.sum_add_distrib, },
   map_smul' := by { intros, simp [finset.smul_sum], } }
 
 variables {n} {R} {M} [fintype n] [fintype m] [fintype p]
 
-@[simp] lemma trace_diag (A : matrix n n M) : trace n R M A = ∑ i, diag n R M A i := rfl
+@[simp] lemma trace_diag (A : matrix n n M) : trace n R M A = ∑ i, diag A i := rfl
 
 lemma trace_apply (A : matrix n n M) : trace n R M A = ∑ i, A i i := rfl
 
 @[simp] lemma trace_one [decidable_eq n] :
   trace n R R 1 = fintype.card n :=
-have h : trace n R R 1 = ∑ i, diag n R R 1 i := rfl,
-by simp_rw [h, diag_one, finset.sum_const, nsmul_one]; refl
+have h : trace n R R 1 = ∑ i, diag 1 i := rfl,
+by simp_rw [h, diag_one, pi.one_def, finset.sum_const, nsmul_one]; refl
 
 @[simp] lemma trace_transpose (A : matrix n n M) : trace n R M Aᵀ = trace n R M A := rfl
 

src/topology/algebra/matrix.lean

@@ -137,9 +137,8 @@ lemma continuous.matrix_reindex {A : X → matrix l n R}
 hA.matrix_minor _ _
 
 @[continuity]
-lemma continuous.matrix_diag [semiring S] [add_comm_monoid R] [module S R]
-  {A : X → matrix n n R} (hA : continuous A) :
-  continuous (λ x, matrix.diag n S R (A x)) :=
+lemma continuous.matrix_diag {A : X → matrix n n R} (hA : continuous A) :
+  continuous (λ x, matrix.diag (A x)) :=
 continuous_pi $ λ _, hA.matrix_elem _ _
 
 @[continuity]