refactor(data/matrix): reverse the direction of matrix.minor_mul_equiv (#10657)

Vierkantor · Vierkantor · commit baab5d309155 · 2021-12-08T22:28:20.000Z
In #10350 this change was proposed, since we apparently use that backwards way more than we use it forwards. We also change `reindex_linear_equiv_mul`, which is similarly much more popular backwards than forwards. Closes: #10638
diff --git a/src/algebra/lie/matrix.lean b/src/algebra/lie/matrix.lean
@@ -73,7 +73,7 @@ types, `matrix.reindex`, is an equivalence of Lie algebras. -/
 def matrix.reindex_lie_equiv : matrix n n R ≃ₗ⁅R⁆ matrix m m R :=
 { to_fun := matrix.reindex e e,
   map_lie' := λ M N, by simp only [lie_ring.of_associative_ring_bracket, matrix.reindex_apply,
-    ←matrix.minor_mul_equiv _ _ _ _, matrix.mul_eq_mul, matrix.minor_sub, pi.sub_apply],
+    matrix.minor_mul_equiv, matrix.mul_eq_mul, matrix.minor_sub, pi.sub_apply],
   ..(matrix.reindex_linear_equiv R R e e) }
 
 @[simp] lemma matrix.reindex_lie_equiv_apply (M : matrix n n R) :
diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean
@@ -1382,18 +1382,19 @@ lemma minor_one_equiv [has_zero α] [has_one α] [decidable_eq m] [decidable_eq
   (1 : matrix m m α).minor e e = 1 :=
 minor_one e e.injective
 
+@[simp]
 lemma minor_mul_equiv [fintype n] [fintype o] [semiring α] {p q : Type*}
   (M : matrix m n α) (N : matrix n p α) (e₁ : l → m) (e₂ : o ≃ n) (e₃ : q → p)  :
-  (M ⬝ N).minor e₁ e₃ = (M.minor e₁ e₂) ⬝ (N.minor e₂ e₃) :=
-minor_mul M N e₁ e₂ e₃ e₂.bijective
+  (M.minor e₁ e₂) ⬝ (N.minor e₂ e₃) = (M ⬝ N).minor e₁ e₃ :=
+(minor_mul M N e₁ e₂ e₃ e₂.bijective).symm
 
 lemma mul_minor_one [fintype n] [fintype o] [semiring α] [decidable_eq o] (e₁ : n ≃ o) (e₂ : l → o)
   (M : matrix m n α) : M ⬝ (1 : matrix o o α).minor e₁ e₂ = minor M id (e₁.symm ∘ e₂) :=
 begin
   let A := M.minor id e₁.symm,
   have : M = A.minor id e₁,
   { simp only [minor_minor, function.comp.right_id, minor_id_id, equiv.symm_comp_self], },
-  rw [this, ←minor_mul_equiv],
+  rw [this, minor_mul_equiv],
   simp only [matrix.mul_one, minor_minor, function.comp.right_id, minor_id_id,
     equiv.symm_comp_self],
 end
@@ -1404,7 +1405,7 @@ begin
   let A := M.minor e₂.symm id,
   have : M = A.minor e₂ id,
   { simp only [minor_minor, function.comp.right_id, minor_id_id, equiv.symm_comp_self], },
-  rw [this, ←minor_mul_equiv],
+  rw [this, minor_mul_equiv],
   simp only [matrix.one_mul, minor_minor, function.comp.right_id, minor_id_id,
     equiv.symm_comp_self],
 end
diff --git a/src/linear_algebra/charpoly/to_matrix.lean b/src/linear_algebra/charpoly/to_matrix.lean
@@ -50,7 +50,7 @@ begin
   set Q := b'.to_matrix b,
 
   have hPQ : C.map_matrix (φ₁ P) ⬝ (C.map_matrix (φ₃ Q)) = 1,
-  { rw [ring_hom.map_matrix_apply, ring_hom.map_matrix_apply, ← matrix.map_mul, ←
+  { rw [ring_hom.map_matrix_apply, ring_hom.map_matrix_apply, ← matrix.map_mul,
       @reindex_linear_equiv_mul _ ι' _ _ _ _ R R, basis.to_matrix_mul_to_matrix_flip,
       reindex_linear_equiv_one, ← ring_hom.map_matrix_apply, ring_hom.map_one] },
 
@@ -59,7 +59,7 @@ begin
   ... = (scalar ι' X - C.map_matrix (φ (P ⬝ A' ⬝ Q))).det :
     by rw [basis_to_matrix_mul_linear_map_to_matrix_mul_basis_to_matrix]
   ... = (scalar ι' X - C.map_matrix (φ₁ P ⬝ φ₂ A' ⬝ φ₃ Q)).det :
-    by rw [reindex_linear_equiv_mul R R _ _ e, reindex_linear_equiv_mul R R e _ _]
+    by rw [reindex_linear_equiv_mul, reindex_linear_equiv_mul]
   ... = (scalar ι' X - (C.map_matrix (φ₁ P) ⬝ C.map_matrix A' ⬝ C.map_matrix (φ₃ Q))).det : by simp
   ... = (scalar ι' X ⬝ C.map_matrix (φ₁ P) ⬝ (C.map_matrix (φ₃ Q)) -
     (C.map_matrix (φ₁ P) ⬝ C.map_matrix A' ⬝ C.map_matrix (φ₃ Q))).det :
diff --git a/src/linear_algebra/determinant.lean b/src/linear_algebra/determinant.lean
@@ -83,8 +83,8 @@ lemma det_comm' [is_domain A] [decidable_eq m] [decidable_eq n]
 -- Although `m` and `n` are different a priori, we will show they have the same cardinality.
 -- This turns the problem into one for square matrices, which is easy.
 let e := index_equiv_of_inv hMM' hM'M in
-by rw [← det_minor_equiv_self e, minor_mul_equiv _ _ _ (equiv.refl n) _, det_comm,
-  ← minor_mul_equiv, equiv.coe_refl, minor_id_id]
+by rw [← det_minor_equiv_self e, ← minor_mul_equiv _ _ _ (equiv.refl n) _, det_comm,
+  minor_mul_equiv, equiv.coe_refl, minor_id_id]
 
 /-- If `M'` is a two-sided inverse for `M` (indexed differently), `det (M ⬝ N ⬝ M') = det N`. -/
 lemma det_conj [is_domain A] [decidable_eq m] [decidable_eq n]
diff --git a/src/linear_algebra/matrix/reindex.lean b/src/linear_algebra/matrix/reindex.lean
@@ -86,8 +86,8 @@ variables [semiring R] [semiring A] [module R A]
 
 lemma reindex_linear_equiv_mul [fintype n] [fintype n']
   (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : matrix m n A) (N : matrix n o A) :
-  reindex_linear_equiv R A eₘ eₒ (M ⬝ N) =
-    reindex_linear_equiv R A eₘ eₙ M ⬝ reindex_linear_equiv R A eₙ eₒ N :=
+  reindex_linear_equiv R A eₘ eₙ M ⬝ reindex_linear_equiv R A eₙ eₒ N =
+    reindex_linear_equiv R A eₘ eₒ (M ⬝ N) :=
 minor_mul_equiv M N _ _ _
 
 lemma mul_reindex_linear_equiv_one [fintype n] [fintype o] [decidable_eq o] (e₁ : o ≃ n)
@@ -107,7 +107,7 @@ a matrix's rows and columns with equivalent types, `matrix.reindex`, is an equiv
 -/
 def reindex_alg_equiv (e : m ≃ n) : matrix m m R ≃ₐ[R] matrix n n R :=
 { to_fun    := reindex e e,
-  map_mul'  := reindex_linear_equiv_mul R R e e e,
+  map_mul'  := λ a b, (reindex_linear_equiv_mul R R e e e a b).symm,
   commutes' := λ r, by simp [algebra_map, algebra.to_ring_hom, minor_smul],
   ..(reindex_linear_equiv R R e e) }
 
