feat(LinearAlgebra/Matrix): scalar if commutes with every nontrivial …

…transvection (#7815)

`M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix).

Also adds `iff` versions and corrects the names of the lemmas in #7810

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>



Co-authored-by: Wen Yang <yang-wen@139.com>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Data/Matrix/Basic.lean

@@ -1286,12 +1286,13 @@ theorem scalar_inj [Nonempty n] {r s : α} : scalar n r = scalar n s ↔ r = s :
   (diagonal_injective.comp Function.const_injective).eq_iff
 #align matrix.scalar_inj Matrix.scalar_inj
 
+theorem scalar_commute_iff [Fintype n] [DecidableEq n] {r : α} {M : Matrix n n α} :
+    Commute (scalar n r) M ↔ r • M = MulOpposite.op r • M := by
+  simp_rw [Commute, SemiconjBy, scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]
+
 theorem scalar_commute [Fintype n] [DecidableEq n] (r : α) (hr : ∀ r', Commute r r')
     (M : Matrix n n α) :
-    Commute (scalar n r) M := by
-  simp_rw [Commute, SemiconjBy, scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]
-  ext i j'
-  exact hr _
+    Commute (scalar n r) M := scalar_commute_iff.2 <| ext fun _ _ => hr _
 #align matrix.scalar.commute Matrix.scalar_commuteₓ
 
 end Scalar

Mathlib/Data/Matrix/Basis.lean

@@ -38,11 +38,11 @@ def stdBasisMatrix (i : m) (j : n) (a : α) : Matrix m n α := fun i' j' =>
 #align matrix.std_basis_matrix Matrix.stdBasisMatrix
 
 @[simp]
-theorem smul_stdBasisMatrix (i : m) (j : n) (a b : α) :
-    b • stdBasisMatrix i j a = stdBasisMatrix i j (b • a) := by
+theorem smul_stdBasisMatrix [SMulZeroClass R α] (r : R) (i : m) (j : n) (a : α) :
+    r • stdBasisMatrix i j a = stdBasisMatrix i j (r • a) := by
   unfold stdBasisMatrix
   ext
-  simp
+  simp [smul_ite]
 #align matrix.smul_std_basis_matrix Matrix.smul_stdBasisMatrix
 
 @[simp]
@@ -216,6 +216,8 @@ theorem mul_of_ne {k l : n} (h : j ≠ k) (d : α) :
 
 end
 
+end StdBasisMatrix
+
 section Commute
 
 variable [Fintype n]
@@ -255,8 +257,20 @@ theorem mem_range_scalar_of_commute_stdBasisMatrix {M : Matrix n n α}
     · rw [col_eq_zero_of_commute_stdBasisMatrix (hM hkl.symm) hkl]
     · rw [row_eq_zero_of_commute_stdBasisMatrix (hM hij) hkl.symm]
 
-end Commute
+theorem mem_range_scalar_iff_commute_stdBasisMatrix {M : Matrix n n α} :
+    M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), i ≠ j → Commute (stdBasisMatrix i j 1) M := by
+  refine ⟨fun ⟨r, hr⟩ i j _ => hr ▸ Commute.symm ?_, mem_range_scalar_of_commute_stdBasisMatrix⟩
+  rw [scalar_commute_iff]
+  simp
 
-end StdBasisMatrix
+/-- `M` is a scalar matrix if and only if it commutes with every `stdBasisMatrix`.​ -/
+theorem mem_range_scalar_iff_commute_stdBasisMatrix' {M : Matrix n n α} :
+    M ∈ Set.range (Matrix.scalar n) ↔ ∀ (i j : n), Commute (stdBasisMatrix i j 1) M := by
+  refine ⟨fun ⟨r, hr⟩ i j => hr ▸ Commute.symm ?_,
+    fun hM => mem_range_scalar_iff_commute_stdBasisMatrix.mpr <| fun i j _ => hM i j⟩
+  rw [scalar_commute_iff]
+  simp
+
+end Commute
 
 end Matrix

Mathlib/LinearAlgebra/Matrix/Transvection.lean

@@ -236,6 +236,22 @@ theorem prod_mul_reverse_inv_prod (L : List (TransvectionStruct n R)) :
     simp_rw [IH, Matrix.mul_one, t.mul_inv]
 #align matrix.transvection_struct.prod_mul_reverse_inv_prod Matrix.TransvectionStruct.prod_mul_reverse_inv_prod
 
+/-- `M` is a scalar matrix if it commutes with every nontrivial transvection (elementary matrix).-/
+theorem _root_.Matrix.mem_range_scalar_of_commute_transvectionStruct {M : Matrix n n R}
+    (hM : ∀ t : TransvectionStruct n R, Commute t.toMatrix M) :
+    M ∈ Set.range (Matrix.scalar n) := by
+  refine mem_range_scalar_of_commute_stdBasisMatrix ?_
+  intro i j hij
+  simpa [transvection, mul_add, add_mul] using (hM ⟨i, j, hij, 1⟩).eq
+
+theorem _root_.Matrix.mem_range_scalar_iff_commute_transvectionStruct {M : Matrix n n R} :
+    M ∈ Set.range (Matrix.scalar n) ↔ ∀ t : TransvectionStruct n R, Commute t.toMatrix M := by
+  refine ⟨fun h t => ?_, mem_range_scalar_of_commute_transvectionStruct⟩
+  rw [mem_range_scalar_iff_commute_stdBasisMatrix] at h
+  refine (Commute.one_left M).add_left ?_
+  convert (h _ _ t.hij).smul_left t.c using 1
+  rw [smul_stdBasisMatrix, smul_eq_mul, mul_one]
+
 end
 
 open Sum