feat(linear_algebra/matrix): det (reindex e e A) = det A (#4875)

This PR includes four flavours of this lemma: `det_reindex_self'` is the `simp` lemma that doesn't include the actual term `reindex` as a subexpression (because that would be already `simp`ed away by `reindex_apply`). `det_reindex_self`, `det_reindex_linear_equiv_self` and `det_reindex_alg_equiv` include their respective function in the lemma statement.




Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/equiv/basic.lean

@@ -238,6 +238,9 @@ def equiv_congr {δ} (ab : α ≃ β) (cd : γ ≃ δ) : (α ≃ γ) ≃ (β ≃
 def perm_congr {α : Type*} {β : Type*} (e : α ≃ β) : perm α ≃ perm β :=
 equiv_congr e e
 
+@[simp] lemma perm_congr_apply {α β : Type*} (e : α ≃ β) (p : equiv.perm α) (x) :
+e.perm_congr p x = e (p (e.symm x)) := rfl
+
 protected lemma image_eq_preimage {α β} (e : α ≃ β) (s : set α) : e '' s = e.symm ⁻¹' s :=
 set.ext $ assume x, set.mem_image_iff_of_inverse e.left_inv e.right_inv
 

src/group_theory/perm/sign.lean

@@ -782,6 +782,11 @@ begin
   refl
 end
 
+@[simp] lemma sign_perm_congr {m n : Type*} [fintype m] [fintype n]
+  (e : m ≃ n) (p : equiv.perm m) :
+  (e.perm_congr p).sign = p.sign :=
+equiv.perm.sign_eq_sign_of_equiv _ _ e.symm (by simp)
+
 end
 
 end sign

src/linear_algebra/matrix.lean

@@ -720,6 +720,60 @@ lemma reindex_transpose (eₘ : m ≃ m') (eₙ : n ≃ n') (M : matrix m n R) :
   (reindex eₘ eₙ M)ᵀ = (reindex eₙ eₘ Mᵀ) :=
 rfl
 
+/-- `simp` version of `det_reindex_self`
+
+`det_reindex_self` is not a good simp lemma because `reindex_apply` fires before.
+So we have this lemma to continue from there. -/
+@[simp]
+lemma det_reindex_self' [decidable_eq m] [decidable_eq n] [comm_ring R]
+  (e : m ≃ n) (A : matrix m m R) :
+  det (λ i j, A (e.symm i) (e.symm j)) = det A :=
+begin
+  unfold det,
+  apply finset.sum_bij' (λ σ _, equiv.perm_congr e.symm σ) _ _ (λ σ _, equiv.perm_congr e σ),
+  { intros σ _, ext, simp only [equiv.symm_symm, equiv.perm_congr_apply, equiv.apply_symm_apply] },
+  { intros σ _, ext, simp only [equiv.symm_symm, equiv.perm_congr_apply, equiv.symm_apply_apply] },
+  { intros σ _, apply finset.mem_univ },
+  { intros σ _, apply finset.mem_univ },
+  intros σ _,
+  simp_rw [equiv.perm_congr_apply, equiv.symm_symm],
+  congr,
+  { convert (equiv.perm.sign_perm_congr e.symm σ).symm },
+  apply finset.prod_bij' (λ i _, e.symm i) _ _ (λ i _, e i),
+  { intros, simp_rw equiv.apply_symm_apply },
+  { intros, simp_rw equiv.symm_apply_apply },
+  { intros, apply finset.mem_univ },
+  { intros, apply finset.mem_univ },
+  { intros, simp_rw equiv.apply_symm_apply },
+end
+
+/-- Reindexing both indices along the same equivalence preserves the determinant.
+
+For the `simp` version of this lemma, see `det_reindex_self'`.
+-/
+lemma det_reindex_self [decidable_eq m] [decidable_eq n] [comm_ring R]
+  (e : m ≃ n) (A : matrix m m R) :
+  det (reindex e e A) = det A :=
+det_reindex_self' e A
+
+/-- Reindexing both indices along the same equivalence preserves the determinant.
+
+For the `simp` version of this lemma, see `det_reindex_self'`.
+-/
+lemma det_reindex_linear_equiv_self [decidable_eq m] [decidable_eq n] [comm_ring R]
+  (e : m ≃ n) (A : matrix m m R) :
+  det (reindex_linear_equiv e e A) = det A :=
+det_reindex_self' e A
+
+/-- Reindexing both indices along the same equivalence preserves the determinant.
+
+For the `simp` version of this lemma, see `det_reindex_self'`.
+-/
+lemma det_reindex_alg_equiv [decidable_eq m] [decidable_eq n] [comm_ring R]
+  (e : m ≃ n) (A : matrix m m R) :
+  det (reindex_alg_equiv e A) = det A :=
+det_reindex_self' e A
+
 end reindexing
 
 end matrix