refactor(linear_algebra/matrix/hermitian): golf and generalize (#18565)

eric-wieser · eric-wieser · commit 9abfa6f0727d · 2023-03-19T20:21:11.000Z
A handful of these results can be proven trivially using results about `is_self_adjoint`.
This also generalizes the typeclass arguments throughout the file, though largely in a mathematically meaningless way.
diff --git a/src/algebra/star/pi.lean b/src/algebra/star/pi.lean
@@ -29,6 +29,9 @@ instance [Π i, has_star (f i)] : has_star (Π i, f i) :=
 
 lemma star_def [Π i, has_star (f i)] (x : Π i, f i) : star x = λ i, star (x i) := rfl
 
+instance [Π i, has_star (f i)] [∀ i, has_trivial_star (f i)] : has_trivial_star (Π i, f i) :=
+{ star_trivial  := λ _, funext $ λ _, star_trivial _ }
+
 instance [Π i, has_involutive_star (f i)] : has_involutive_star (Π i, f i) :=
 { star_involutive := λ _, funext $ λ _, star_star _ }
 
diff --git a/src/algebra/star/prod.lean b/src/algebra/star/prod.lean
@@ -29,6 +29,10 @@ instance [has_star R] [has_star S] : has_star (R × S) :=
 
 lemma star_def [has_star R] [has_star S] (x : R × S) : star x = (star x.1, star x.2) := rfl
 
+instance [has_star R] [has_star S] [has_trivial_star R] [has_trivial_star S] :
+  has_trivial_star (R × S) :=
+{ star_trivial := λ _, prod.ext (star_trivial _) (star_trivial _) }
+
 instance [has_involutive_star R] [has_involutive_star S] : has_involutive_star (R × S) :=
 { star_involutive := λ _, prod.ext (star_star _) (star_star _) }
 
diff --git a/src/algebra/star/self_adjoint.lean b/src/algebra/star/self_adjoint.lean
@@ -111,6 +111,17 @@ by simp only [is_self_adjoint_iff, star_sub, hx.star_eq, hy.star_eq]
 
 end add_group
 
+section add_comm_monoid
+variables [add_comm_monoid R] [star_add_monoid R]
+
+lemma _root_.is_self_adjoint_add_star_self (x : R) : is_self_adjoint (x + star x) :=
+by simp only [is_self_adjoint_iff, add_comm, star_add, star_star]
+
+lemma _root_.is_self_adjoint_star_add_self (x : R) : is_self_adjoint (star x + x) :=
+by simp only [is_self_adjoint_iff, add_comm, star_add, star_star]
+
+end add_comm_monoid
+
 section semigroup
 variables [semigroup R] [star_semigroup R]
 
diff --git a/src/linear_algebra/matrix/hermitian.lean b/src/linear_algebra/matrix/hermitian.lean
@@ -9,6 +9,8 @@ import analysis.inner_product_space.pi_L2
 
 This file defines hermitian matrices and some basic results about them.
 
+See also `is_self_adjoint`, which generalizes this definition to other star rings.
+
 ## Main definition
 
  * `matrix.is_hermitian` : a matrix `A : matrix n n α` is hermitian if `Aᴴ = A`.
@@ -27,56 +29,28 @@ open_locale matrix
 
 local notation `⟪`x`, `y`⟫` := @inner α _ _ x y
 
-section non_unital_semiring
-
-variables [non_unital_semiring α] [star_ring α] [non_unital_semiring β] [star_ring β]
+section has_star
+variables [has_star α] [has_star β]
 
 /-- A matrix is hermitian if it is equal to its conjugate transpose. On the reals, this definition
 captures symmetric matrices. -/
 def is_hermitian (A : matrix n n α) : Prop := Aᴴ = A
 
 lemma is_hermitian.eq {A : matrix n n α} (h : A.is_hermitian) : Aᴴ = A := h
 
+protected lemma is_hermitian.is_self_adjoint {A : matrix n n α} (h : A.is_hermitian) :
+  is_self_adjoint A := h
+
 @[ext]
 lemma is_hermitian.ext {A : matrix n n α} : (∀ i j, star (A j i) = A i j) → A.is_hermitian :=
 by { intros h, ext i j, exact h i j }
 
 lemma is_hermitian.apply {A : matrix n n α} (h : A.is_hermitian) (i j : n) : star (A j i) = A i j :=
-by { unfold is_hermitian at h, rw [← h, conj_transpose_apply, star_star, h] }
+congr_fun (congr_fun h _) _
 
 lemma is_hermitian.ext_iff {A : matrix n n α} : A.is_hermitian ↔ ∀ i j, star (A j i) = A i j :=
 ⟨is_hermitian.apply, is_hermitian.ext⟩
 
-lemma is_hermitian_mul_conj_transpose_self [fintype n] (A : matrix n n α) :
-  (A ⬝ Aᴴ).is_hermitian :=
-by rw [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose]
-
-lemma is_hermitian_transpose_mul_self [fintype n] (A : matrix n n α) :
-  (Aᴴ ⬝ A).is_hermitian :=
-by rw [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose]
-
-lemma is_hermitian_conj_transpose_mul_mul [fintype m] {A : matrix m m α} (B : matrix m n α)
-  (hA : A.is_hermitian) : (Bᴴ ⬝ A ⬝ B).is_hermitian :=
-by simp only [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose, hA.eq,
-  matrix.mul_assoc]
-
-lemma is_hermitian_mul_mul_conj_transpose [fintype m] {A : matrix m m α} (B : matrix n m α)
-  (hA : A.is_hermitian) : (B ⬝ A ⬝ Bᴴ).is_hermitian :=
-by simp only [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose, hA.eq,
-  matrix.mul_assoc]
-
-lemma is_hermitian_add_transpose_self (A : matrix n n α) :
-  (A + Aᴴ).is_hermitian :=
-by simp [is_hermitian, add_comm]
-
-lemma is_hermitian_transpose_add_self (A : matrix n n α) :
-  (Aᴴ + A).is_hermitian :=
-by simp [is_hermitian, add_comm]
-
-@[simp] lemma is_hermitian_zero :
-  (0 : matrix n n α).is_hermitian :=
-conj_transpose_zero
-
 @[simp] lemma is_hermitian.map {A : matrix n n α} (h : A.is_hermitian) (f : α → β)
   (hf : function.semiconj f star star) :
   (A.map f).is_hermitian :=
@@ -95,15 +69,6 @@ lemma is_hermitian.conj_transpose {A : matrix n n α} (h : A.is_hermitian) :
   Aᴴ.is_hermitian :=
 h.transpose.map _ $ λ _, rfl
 
-@[simp] lemma is_hermitian_conj_transpose_iff (A : matrix n n α) :
-  Aᴴ.is_hermitian ↔ A.is_hermitian :=
-⟨by { intro h, rw [← conj_transpose_conj_transpose A], exact is_hermitian.conj_transpose h },
-  is_hermitian.conj_transpose⟩
-
-@[simp] lemma is_hermitian.add {A B : matrix n n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
-  (A + B).is_hermitian :=
-(conj_transpose_add _ _).trans (hA.symm ▸ hB.symm ▸ rfl)
-
 @[simp] lemma is_hermitian.submatrix {A : matrix n n α} (h : A.is_hermitian) (f : m → n) :
   (A.submatrix f f).is_hermitian :=
 (conj_transpose_submatrix _ _ _).trans (h.symm ▸ rfl)
@@ -112,10 +77,14 @@ h.transpose.map _ $ λ _, rfl
   (A.submatrix e e).is_hermitian ↔ A.is_hermitian :=
 ⟨λ h, by simpa using h.submatrix e.symm, λ h, h.submatrix _⟩
 
-/-- The real diagonal matrix `diagonal v` is hermitian. -/
-@[simp] lemma is_hermitian_diagonal [decidable_eq n] (v : n → ℝ) :
-  (diagonal v).is_hermitian :=
-diagonal_conj_transpose _
+end has_star
+
+section has_involutive_star
+variables [has_involutive_star α]
+
+@[simp] lemma is_hermitian_conj_transpose_iff (A : matrix n n α) :
+  Aᴴ.is_hermitian ↔ A.is_hermitian :=
+is_self_adjoint.star_iff
 
 /-- A block matrix `A.from_blocks B C D` is hermitian,
     if `A` and `D` are hermitian and `Bᴴ = C`. -/
@@ -124,7 +93,8 @@ lemma is_hermitian.from_blocks
   (hA : A.is_hermitian) (hBC : Bᴴ = C) (hD : D.is_hermitian) :
   (A.from_blocks B C D).is_hermitian :=
 begin
-  have hCB : Cᴴ = B, {rw ← hBC, simp},
+  have hCB : Cᴴ = B,
+  { rw [← hBC, conj_transpose_conj_transpose] },
   unfold matrix.is_hermitian,
   rw from_blocks_conj_transpose,
   congr;
@@ -139,34 +109,100 @@ lemma is_hermitian_from_blocks_iff
        congr_arg to_blocks₁₂ h, congr_arg to_blocks₂₂ h⟩,
  λ ⟨hA, hBC, hCB, hD⟩, is_hermitian.from_blocks hA hBC hD⟩
 
-end non_unital_semiring
+end has_involutive_star
 
-section semiring
+section add_monoid
+variables [add_monoid α] [star_add_monoid α] [add_monoid β] [star_add_monoid β]
 
-variables [semiring α] [star_ring α] [semiring β] [star_ring β]
+/-- A diagonal matrix is hermitian if the entries are self-adjoint -/
+lemma is_hermitian_diagonal_of_self_adjoint [decidable_eq n]
+  (v : n → α) (h : is_self_adjoint v) :
+  (diagonal v).is_hermitian :=
+-- TODO: add a `pi.has_trivial_star` instance and remove the `funext`
+(diagonal_conj_transpose v).trans $ congr_arg _ h
 
-@[simp] lemma is_hermitian_one [decidable_eq n] :
-  (1 : matrix n n α).is_hermitian :=
-conj_transpose_one
+/-- A diagonal matrix is hermitian if the entries have the trivial `star` operation
+(such as on the reals). -/
+@[simp] lemma is_hermitian_diagonal [has_trivial_star α] [decidable_eq n] (v : n → α) :
+  (diagonal v).is_hermitian :=
+is_hermitian_diagonal_of_self_adjoint _ (is_self_adjoint.all _)
 
-end semiring
+@[simp] lemma is_hermitian_zero :
+  (0 : matrix n n α).is_hermitian :=
+is_self_adjoint_zero _
+
+@[simp] lemma is_hermitian.add {A B : matrix n n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
+  (A + B).is_hermitian :=
+is_self_adjoint.add hA hB
+
+end add_monoid
+
+section add_comm_monoid
+variables [add_comm_monoid α] [star_add_monoid α]
+
+lemma is_hermitian_add_transpose_self (A : matrix n n α) :
+  (A + Aᴴ).is_hermitian :=
+is_self_adjoint_add_star_self A
 
-section ring
+lemma is_hermitian_transpose_add_self (A : matrix n n α) :
+  (Aᴴ + A).is_hermitian :=
+is_self_adjoint_star_add_self A
+
+end add_comm_monoid
 
-variables [ring α] [star_ring α] [ring β] [star_ring β]
+section add_group
+variables [add_group α] [star_add_monoid α]
 
 @[simp] lemma is_hermitian.neg {A : matrix n n α} (h : A.is_hermitian) :
   (-A).is_hermitian :=
-(conj_transpose_neg _).trans (congr_arg _ h)
+is_self_adjoint.neg h
 
 @[simp] lemma is_hermitian.sub {A B : matrix n n α} (hA : A.is_hermitian) (hB : B.is_hermitian) :
   (A - B).is_hermitian :=
-(conj_transpose_sub _ _).trans (hA.symm ▸ hB.symm ▸ rfl)
+is_self_adjoint.sub hA hB
 
-end ring
+end add_group
 
-section comm_ring
+section non_unital_semiring
+variables [non_unital_semiring α] [star_ring α] [non_unital_semiring β] [star_ring β]
+
+/-- Note this is more general than `is_self_adjoint.mul_star_self` as `B` can be rectangular. -/
+lemma is_hermitian_mul_conj_transpose_self [fintype n] (A : matrix m n α) :
+  (A ⬝ Aᴴ).is_hermitian :=
+by rw [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose]
+
+/-- Note this is more general than `is_self_adjoint.star_mul_self` as `B` can be rectangular. -/
+lemma is_hermitian_transpose_mul_self [fintype m] (A : matrix m n α) :
+  (Aᴴ ⬝ A).is_hermitian :=
+by rw [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose]
 
+/-- Note this is more general than `is_self_adjoint.conjugate'` as `B` can be rectangular. -/
+lemma is_hermitian_conj_transpose_mul_mul [fintype m] {A : matrix m m α} (B : matrix m n α)
+  (hA : A.is_hermitian) : (Bᴴ ⬝ A ⬝ B).is_hermitian :=
+by simp only [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose, hA.eq,
+  matrix.mul_assoc]
+
+/-- Note this is more general than `is_self_adjoint.conjugate` as `B` can be rectangular. -/
+lemma is_hermitian_mul_mul_conj_transpose [fintype m] {A : matrix m m α} (B : matrix n m α)
+  (hA : A.is_hermitian) : (B ⬝ A ⬝ Bᴴ).is_hermitian :=
+by simp only [is_hermitian, conj_transpose_mul, conj_transpose_conj_transpose, hA.eq,
+  matrix.mul_assoc]
+
+end non_unital_semiring
+
+section semiring
+
+variables [semiring α] [star_ring α] [semiring β] [star_ring β]
+
+/-- Note this is more general for matrices than `is_self_adjoint_one` as it does not
+require `fintype n`, which is necessary for `monoid (matrix n n R)`. -/
+@[simp] lemma is_hermitian_one [decidable_eq n] :
+  (1 : matrix n n α).is_hermitian :=
+conj_transpose_one
+
+end semiring
+
+section comm_ring
 variables [comm_ring α] [star_ring α]
 
 lemma is_hermitian.inv [fintype m] [decidable_eq m] {A : matrix m m α}
