feat(LinearAlgebra/Matrix): expand IsSymm/IsHermitian API (leanprover-community#36349)

Author: SnirBroshi

Mathlib/Algebra/Lie/Classical.lean

@@ -276,6 +276,7 @@ theorem jd_transform [Fintype l] : (PD l R)ᵀ * JD l R * PD l R = (2 : R) • S
   rw [h, PD, s_as_blocks, Matrix.fromBlocks_multiply, Matrix.fromBlocks_smul]
   simp [two_smul]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem pd_inv [Fintype l] [Invertible (2 : R)] : PD l R * ⅟(2 : R) • (PD l R)ᵀ = 1 := by
   rw [PD, Matrix.fromBlocks_transpose, Matrix.fromBlocks_smul,
     Matrix.fromBlocks_multiply]

Mathlib/Data/Matrix/Composition.lean

@@ -104,6 +104,10 @@ theorem comp_map_transpose (M : Matrix I J (Matrix K L R)) :
 theorem comp_symm_transpose (M : Matrix (I × K) (J × L) R) :
     (comp J I L K R).symm Mᵀ = (((comp I J K L R).symm M).map (·ᵀ))ᵀ := rfl
 
+theorem transpose_comp (M : Matrix I J (Matrix K L R)) :
+    (comp I J K L R M)ᵀ = comp J I L K R (Mᵀ.map (·ᵀ)) :=
+  rfl
+
 end Basic
 
 section Add

Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

@@ -145,6 +145,7 @@ theorem trace_eq_neg_charpoly_nextCoeff (M : Matrix n n R) : M.trace = -M.charpo
   nontriviality
   simp [trace_eq_neg_charpoly_coeff, nextCoeff]
 
+set_option backward.isDefEq.respectTransparency false in
 theorem det_eq_sign_charpoly_coeff (M : Matrix n n R) :
     M.det = (-1) ^ Fintype.card n * M.charpoly.coeff 0 := by
   rw [coeff_zero_eq_eval_zero, charpoly, eval_det, matPolyEquiv_charmatrix, ← det_smul]

Mathlib/LinearAlgebra/Matrix/ConjTranspose.lean

@@ -134,6 +134,11 @@ theorem conjTranspose_apply [Star α] (M : Matrix m n α) (i j) :
 theorem conjTranspose_conjTranspose [InvolutiveStar α] (M : Matrix m n α) : Mᴴᴴ = M :=
   Matrix.ext <| by simp
 
+variable (n α) in
+theorem conjTranspose_involutive [InvolutiveStar α] :
+    (conjTranspose : Matrix n n α → Matrix n n α).Involutive :=
+  conjTranspose_conjTranspose
+
 theorem conjTranspose_transpose [Star α] (M : Matrix m n α) :
     Mᴴᵀ = M.map star :=
   rfl

Mathlib/LinearAlgebra/Matrix/Defs.lean

@@ -169,6 +169,9 @@ instance addCommMonoid [AddCommMonoid α] : AddCommMonoid (Matrix m n α) :=
 instance neg [Neg α] : Neg (Matrix m n α) :=
   fast_instance% Pi.instNeg
 
+instance involutiveNeg [InvolutiveNeg α] : InvolutiveNeg (Matrix m n α) :=
+  Pi.involutiveNeg
+
 instance sub [Sub α] : Sub (Matrix m n α) :=
   fast_instance% Pi.instSub
 
@@ -351,6 +354,10 @@ theorem transpose_transpose (M : Matrix m n α) : Mᵀᵀ = M := by
   ext
   rfl
 
+variable (n α) in
+theorem transpose_involutive : (transpose : Matrix n n α → Matrix n n α).Involutive :=
+  transpose_transpose
+
 theorem transpose_injective : Function.Injective (transpose : Matrix m n α → Matrix n m α) :=
   fun _ _ h => ext fun i j => ext_iff.2 h j i
 
@@ -373,17 +380,14 @@ theorem transpose_sub [Sub α] (M : Matrix m n α) (N : Matrix m n α) : (M - N)
   simp
 
 @[simp]
-theorem transpose_smul {R : Type*} [SMul R α] (c : R) (M : Matrix m n α) : (c • M)ᵀ = c • Mᵀ := by
-  ext
+theorem transpose_smul {R : Type*} [SMul R α] (c : R) (M : Matrix m n α) : (c • M)ᵀ = c • Mᵀ :=
   rfl
 
 @[simp]
-theorem transpose_neg [Neg α] (M : Matrix m n α) : (-M)ᵀ = -Mᵀ := by
-  ext
+theorem transpose_neg [Neg α] (M : Matrix m n α) : (-M)ᵀ = -Mᵀ :=
   rfl
 
-theorem transpose_map {f : α → β} {M : Matrix m n α} : Mᵀ.map f = (M.map f)ᵀ := by
-  ext
+theorem transpose_map {f : α → β} {M : Matrix m n α} : Mᵀ.map f = (M.map f)ᵀ :=
   rfl
 
 end Transpose

Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean

@@ -164,6 +164,7 @@ noncomputable instance repsFintype (k : ℤ) : Fintype (reps k) := by
   ext i j
   simpa only [Subtype.mk.injEq] using congrFun₂ h i j
 
+set_option backward.isDefEq.respectTransparency false in
 @[simp]
 lemma S_smul_four (A : Δ m) : S • S • S • S • A = A := by
   simp only [smul_def, ← mul_assoc, S_mul_S_eq, neg_mul, one_mul, mul_neg, neg_neg, Subtype.coe_eta]

Mathlib/LinearAlgebra/Matrix/Hermitian.lean

@@ -64,8 +64,13 @@ theorem IsHermitian.ext_iff {A : Matrix n n α} : A.IsHermitian ↔ ∀ i j, sta
 
 @[simp]
 theorem IsHermitian.map {A : Matrix n n α} (h : A.IsHermitian) (f : α → β)
-    (hf : Function.Semiconj f star star) : (A.map f).IsHermitian :=
-  (conjTranspose_map f hf).symm.trans <| h.eq.symm ▸ rfl
+    (hf : Function.Semiconj f star star) : (A.map f).IsHermitian := by
+  rw [IsHermitian, ← conjTranspose_map f hf, h.eq]
+
+@[simp]
+theorem isHermitian_map_iff {A : Matrix n n α} {f : α → β} (hf : Function.Semiconj f star star)
+    (hinj : f.Injective) : (A.map f).IsHermitian ↔ A.IsHermitian := by
+  rw [IsHermitian, IsHermitian, ← conjTranspose_map f hf, map_injective hinj |>.eq_iff]
 
 @[simp, nontriviality]
 theorem IsHermitian.of_subsingleton {A : Matrix n n α} [Subsingleton α] : A.IsHermitian :=
@@ -76,7 +81,7 @@ theorem IsHermitian.transpose {A : Matrix n n α} (h : A.IsHermitian) : Aᵀ.IsH
   exact congr_arg Matrix.transpose h
 
 @[simp]
-theorem isHermitian_transpose_iff (A : Matrix n n α) : Aᵀ.IsHermitian ↔ A.IsHermitian :=
+theorem isHermitian_transpose_iff {A : Matrix n n α} : Aᵀ.IsHermitian ↔ A.IsHermitian :=
   ⟨by intro h; rw [← transpose_transpose A]; exact IsHermitian.transpose h, IsHermitian.transpose⟩
 
 theorem IsHermitian.conjTranspose {A : Matrix n n α} (h : A.IsHermitian) : Aᴴ.IsHermitian :=
@@ -91,14 +96,42 @@ theorem isHermitian_submatrix_equiv {A : Matrix n n α} (e : m ≃ n) :
     (A.submatrix e e).IsHermitian ↔ A.IsHermitian :=
   ⟨fun h => by simpa using h.submatrix e.symm, fun h => h.submatrix _⟩
 
+theorem IsHermitian.reindex {A : Matrix n n α} (h : A.IsHermitian) (f : n ≃ m) :
+    (A.reindex f f).IsHermitian := by
+  rw [reindex_apply]
+  apply submatrix h
+
+theorem isHermitian_reindex_iff {A : Matrix n n α} (f : n ≃ m) :
+    (A.reindex f f).IsHermitian ↔ A.IsHermitian := by
+  refine ⟨fun h ↦ ?_, (·.reindex f)⟩
+  simpa using h.reindex f.symm
+
+theorem conjTranspose_comp {I J K L : Type*} (M : Matrix I J (Matrix K L α)) :
+    (comp I J K L α M)ᴴ = comp J I L K α (Mᵀ.map (·ᴴ)) :=
+  rfl
+
+/-- When the inner matrices are square we can use the induced star operation -/
+theorem conjTranspose_comp' {I J K : Type*} (M : Matrix I J (Matrix K K α)) :
+    (comp I J K K α M)ᴴ = comp J I K K α Mᴴ :=
+  rfl
+
+theorem isHermitian_comp_iff {A : Matrix m m (Matrix n n α)} :
+    (A.comp m m n n α).IsHermitian ↔ A.IsHermitian := by
+  rw [IsHermitian, IsHermitian, conjTranspose_comp', comp .. |>.injective.eq_iff]
+
+theorem isHermitian_comp_iff_forall {A : Matrix m m (Matrix n n α)} :
+    (A.comp m m n n α).IsHermitian ↔ ∀ i j i' j', star (A j i j' i') = A i j i' j' := by
+  simp [IsHermitian.ext_iff]
+  grind
+
 end Star
 
 section InvolutiveStar
 
 variable [InvolutiveStar α]
 
 @[simp]
-theorem isHermitian_conjTranspose_iff (A : Matrix n n α) : Aᴴ.IsHermitian ↔ A.IsHermitian :=
+theorem isHermitian_conjTranspose_iff {A : Matrix n n α} : Aᴴ.IsHermitian ↔ A.IsHermitian :=
   IsSelfAdjoint.star_iff
 
 /-- A block matrix `A.from_blocks B C D` is Hermitian,
@@ -174,13 +207,52 @@ variable [AddGroup α] [StarAddMonoid α]
 theorem IsHermitian.neg {A : Matrix n n α} (h : A.IsHermitian) : (-A).IsHermitian :=
   IsSelfAdjoint.neg h
 
+@[simp]
+theorem isHermitian_neg_iff {A : Matrix n n α} : (-A).IsHermitian ↔ A.IsHermitian := by
+  refine ⟨fun h ↦ ?_, (·.neg)⟩
+  rw [← neg_neg A]
+  exact h.neg
+
 @[simp]
 theorem IsHermitian.sub {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
     (A - B).IsHermitian :=
   IsSelfAdjoint.sub hA hB
 
 end AddGroup
 
+section StarModule
+
+variable {R : Type*} [Star R] [Star α] [SMul R α] [StarModule R α]
+
+theorem IsHermitian.smul {A : Matrix n n α} (h : A.IsHermitian) {k : R} (hk : IsSelfAdjoint k) :
+    (k • A).IsHermitian := by
+  rw [IsHermitian, conjTranspose_smul, hk.star_eq, h.eq]
+
+end StarModule
+
+section MulAction_StarModule
+
+variable {R : Type*} [Monoid R] [Star R] [Star α] [MulAction R α] [StarModule R α]
+
+theorem IsHermitian.of_smul {A : Matrix n n α} {k : R} [Invertible k] (h : (k • A).IsHermitian)
+    (hk : IsSelfAdjoint k) : A.IsHermitian := by
+  rw [IsHermitian, conjTranspose_smul, hk.star_eq] at h
+  simpa using congr(⅟k • $h)
+
+/-- Assumes `IsSelfAdjoint ⅟k` instead of `IsSelfAdjoint k`.
+These are equivalent given `StarMul R` -/
+theorem IsHermitian.of_smul' {A : Matrix n n α} {k : R} [Invertible k] (h : (k • A).IsHermitian)
+    (hk : IsSelfAdjoint ⅟k) : A.IsHermitian := by
+  rw [← invOf_smul_smul k A]
+  exact h.smul hk
+
+@[simp]
+theorem isHermitian_smul_iff {A : Matrix n n α} {k : R} [Invertible k] (hk : IsSelfAdjoint k) :
+    (k • A).IsHermitian ↔ A.IsHermitian :=
+  ⟨(·.of_smul hk), (·.smul hk)⟩
+
+end MulAction_StarModule
+
 section NonUnitalSemiring
 
 variable [NonUnitalSemiring α] [StarRing α]
@@ -213,16 +285,22 @@ lemma IsHermitian.commute_iff [Fintype n] {A B : Matrix n n α}
 
 end NonUnitalSemiring
 
-section Semiring
+section NonAssocSemiring
 
-variable [Semiring α] [StarRing α]
+variable [NonAssocSemiring α] [StarRing α]
 
 /-- Note this is more general for matrices than `isSelfAdjoint_one` as it does not
 require `Fintype n`, which is necessary for `Monoid (Matrix n n R)`. -/
 @[simp]
 theorem isHermitian_one [DecidableEq n] : (1 : Matrix n n α).IsHermitian :=
   conjTranspose_one
 
+end NonAssocSemiring
+
+section Semiring
+
+variable [Semiring α] [StarRing α]
+
 @[simp]
 theorem isHermitian_natCast [DecidableEq n] (d : ℕ) : (d : Matrix n n α).IsHermitian :=
   conjTranspose_natCast _

Mathlib/LinearAlgebra/Matrix/SchurComplement.lean

@@ -227,6 +227,7 @@ section Block
 /-! #### General 2×2 block matrices -/
 
 
+set_option backward.isDefEq.respectTransparency false in
 /-- A block matrix is invertible if the bottom right corner and the corresponding Schur complement
 is. -/
 @[implicit_reducible]

Mathlib/LinearAlgebra/Matrix/Swap.lean

@@ -46,6 +46,9 @@ lemma swap_comm (i j : n) :
 lemma transpose_swap (i j : n) : (swap R i j).transpose = swap R i j := by
   simp [swap]
 
+theorem isSymm_swap (i j : n) : (swap R i j).IsSymm :=
+  transpose_swap i j
+
 @[simp]
 lemma conjTranspose_swap {R : Type*} [NonAssocSemiring R] [StarRing R] (i j : n) :
     (swap R i j).conjTranspose = swap R i j := by

Mathlib/LinearAlgebra/Matrix/Symmetric.lean

@@ -78,21 +78,43 @@ theorem IsSymm.pow [CommSemiring α] [Fintype n] [DecidableEq n] {A : Matrix n n
   rw [IsSymm, transpose_pow, h]
 
 @[simp]
-theorem IsSymm.map {A : Matrix n n α} (h : A.IsSymm) (f : α → β) : (A.map f).IsSymm :=
-  transpose_map.symm.trans (h.symm ▸ rfl)
+theorem IsSymm.map {A : Matrix n n α} (h : A.IsSymm) (f : α → β) : (A.map f).IsSymm := by
+  rw [IsSymm, ← transpose_map, h.eq]
 
 @[simp]
+theorem isSymm_map_iff {A : Matrix n n α} {f : α → β} (hf : f.Injective) :
+    (A.map f).IsSymm ↔ A.IsSymm := by
+  rw [IsSymm, IsSymm, ← transpose_map, map_injective hf |>.eq_iff]
+
 theorem IsSymm.transpose {A : Matrix n n α} (h : A.IsSymm) : Aᵀ.IsSymm :=
   congr_arg _ h
 
+@[simp]
+theorem isSymm_transpose_iff {A : Matrix n n α} : Aᵀ.IsSymm ↔ A.IsSymm := by
+  refine ⟨fun h ↦ ?_, (·.transpose)⟩
+  rw [← A.transpose_transpose]
+  exact h.transpose
+
 @[simp]
 theorem IsSymm.conjTranspose [Star α] {A : Matrix n n α} (h : A.IsSymm) : Aᴴ.IsSymm :=
   h.transpose.map _
 
+@[simp]
+theorem isSymm_conjTranspose_iff [InvolutiveStar α] {A : Matrix n n α} : Aᴴ.IsSymm ↔ A.IsSymm := by
+  refine ⟨fun h ↦ ?_, (·.conjTranspose)⟩
+  rw [← A.conjTranspose_conjTranspose]
+  exact h.conjTranspose
+
 @[simp]
 theorem IsSymm.neg [Neg α] {A : Matrix n n α} (h : A.IsSymm) : (-A).IsSymm :=
   (transpose_neg _).trans (congr_arg _ h)
 
+@[simp]
+theorem isSymm_neg_iff [InvolutiveNeg α] {A : Matrix n n α} : (-A).IsSymm ↔ A.IsSymm := by
+  refine ⟨fun h ↦ ?_, (·.neg)⟩
+  rw [← neg_neg A]
+  exact h.neg
+
 @[simp]
 theorem IsSymm.add {A B : Matrix n n α} [Add α] (hA : A.IsSymm) (hB : B.IsSymm) : (A + B).IsSymm :=
   (transpose_add _ _).trans (hA.symm ▸ hB.symm ▸ rfl)
@@ -105,10 +127,25 @@ theorem IsSymm.sub {A B : Matrix n n α} [Sub α] (hA : A.IsSymm) (hB : B.IsSymm
 theorem IsSymm.smul [SMul R α] {A : Matrix n n α} (h : A.IsSymm) (k : R) : (k • A).IsSymm :=
   (transpose_smul _ _).trans (congr_arg _ h)
 
+@[simp]
+theorem isSymm_smul_iff [Monoid R] [MulAction R α] {A : Matrix n n α} (k : R) [Invertible k] :
+    (k • A).IsSymm ↔ A.IsSymm := by
+  refine ⟨fun h ↦ ?_, (·.smul k)⟩
+  rw [← invOf_smul_smul k A]
+  exact h.smul ⅟k
+
 @[simp]
 theorem IsSymm.submatrix {A : Matrix n n α} (h : A.IsSymm) (f : m → n) : (A.submatrix f f).IsSymm :=
   (transpose_submatrix _ _ _).trans (h.symm ▸ rfl)
 
+theorem IsSymm.reindex {A : Matrix n n α} (h : A.IsSymm) (f : n ≃ m) : (A.reindex f f).IsSymm := by
+  rw [reindex_apply]
+  apply submatrix h
+
+theorem isSymm_reindex_iff {A : Matrix n n α} (f : n ≃ m) : (A.reindex f f).IsSymm ↔ A.IsSymm := by
+  refine ⟨fun h ↦ ?_, (·.reindex f)⟩
+  simpa using h.reindex f.symm
+
 /-- The diagonal matrix `diagonal v` is symmetric. -/
 @[simp]
 theorem isSymm_diagonal [DecidableEq n] [Zero α] (v : n → α) : (diagonal v).IsSymm :=
@@ -133,4 +170,14 @@ theorem isSymm_fromBlocks_iff {A : Matrix m m α} {B : Matrix m n α} {C : Matri
       (congr_arg toBlocks₂₂ h :)⟩,
     fun ⟨hA, hBC, _, hD⟩ => IsSymm.fromBlocks hA hBC hD⟩
 
+theorem isSymm_comp_iff {A : Matrix m m (Matrix n n α)} :
+    (A.comp m m n n α).IsSymm ↔ Aᵀ = A.map (·ᵀ) := by
+  rw [IsSymm, transpose_comp, transpose_map, comp .. |>.injective.eq_iff, eq_comm,
+    transpose_involutive _ _ |>.eq_iff]
+
+theorem isSymm_comp_iff_forall {A : Matrix m m (Matrix n n α)} :
+    (A.comp m m n n α).IsSymm ↔ ∀ i j i' j', A j i j' i' = A i j i' j' := by
+  simp [IsSymm.ext_iff]
+  grind
+
 end Matrix