feat(linear_algebra): det (M ⬝ N ⬝ M') = det N, where M' is an in…

…verse of `M` (#7633)

This is an important step towards showing the determinant of `linear_map.to_matrix` does not depend on the choice of basis.
    
The main difficulty is allowing the two indexing types of `M` to be (a priori) different. They are in bijection though (using `basis.index_equiv` from #7631), so using `reindex_linear_equiv` we can turn everything into square matrices and apply the "usual" proof.



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

src/linear_algebra/determinant.lean

@@ -3,9 +3,11 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen
 -/
+import linear_algebra.free_module
 import linear_algebra.matrix.basis
-import linear_algebra.matrix.to_linear_equiv
 import linear_algebra.matrix.diagonal
+import linear_algebra.matrix.to_linear_equiv
+import linear_algebra.matrix.reindex
 import linear_algebra.multilinear
 import linear_algebra.dual
 import ring_theory.algebra_tower
@@ -52,6 +54,47 @@ variables {M' : Type*} [add_comm_group M'] [module R M']
 variables {ι : Type*} [decidable_eq ι] [fintype ι]
 variables (e : basis ι R M)
 
+section conjugate
+
+variables {A : Type*} [integral_domain A]
+variables {m n : Type*} [fintype m] [fintype n]
+
+
+/-- If `R^m` and `R^n` are linearly equivalent, then `m` and `n` are also equivalent. -/
+def equiv_of_pi_lequiv_pi {R : Type*} [integral_domain R]
+  (e : (m → R) ≃ₗ[R] (n → R)) : m ≃ n :=
+basis.index_equiv (basis.of_equiv_fun e.symm) (pi.basis_fun _ _)
+
+/-- If `M` and `M'` are each other's inverse matrices, they are square matrices up to
+equivalence of types. -/
+def matrix.index_equiv_of_inv [decidable_eq m] [decidable_eq n]
+  {M : matrix m n A} {M' : matrix n m A}
+  (hMM' : M ⬝ M' = 1) (hM'M : M' ⬝ M = 1) :
+  m ≃ n :=
+equiv_of_pi_lequiv_pi (matrix.to_lin'_of_inv hMM' hM'M)
+
+/-- If `M'` is a two-sided inverse for `M` (indexed differently), `det (M ⬝ N ⬝ M') = det N`. -/
+lemma matrix.det_conj
+  [decidable_eq m] [decidable_eq n]
+  {M : matrix m n A} {M' : matrix n m A} {N : matrix n n A}
+  (hMM' : M ⬝ M' = 1) (hM'M : M' ⬝ M = 1) :
+  det (M ⬝ N ⬝ M') = det N :=
+begin
+  -- 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 (`matrix.det_units_conj`), which is easy.
+  let e : m ≃ n := matrix.index_equiv_of_inv hMM' hM'M,
+  let U : units (matrix n n A) :=
+    ⟨M.minor e.symm (equiv.refl _),
+     M'.minor (equiv.refl _) e.symm,
+     by rw [mul_eq_mul, ←minor_mul_equiv, hMM', minor_one_equiv],
+     by rw [mul_eq_mul, ←minor_mul_equiv, hM'M, minor_one_equiv]⟩,
+  rw [← matrix.det_units_conj U N, ← det_minor_equiv_self e.symm],
+  simp only [minor_mul_equiv _ _ _ (equiv.refl n) _, equiv.coe_refl, minor_id_id,
+             units.coe_mk, units.inv_mk]
+end
+
+end conjugate
+
 lemma linear_equiv.is_unit_det (f : M ≃ₗ[R] M') (v : basis ι R M) (v' : basis ι R M') :
   is_unit (linear_map.to_matrix v v' f).det :=
 begin

src/linear_algebra/matrix/reindex.lean

@@ -25,6 +25,8 @@ matrix, reindex
 
 namespace matrix
 
+open_locale matrix
+
 variables {l m n : Type*} [fintype l] [fintype m] [fintype n]
 variables {l' m' n' : Type*} [fintype l'] [fintype m'] [fintype n']
 variables {R : Type*}
@@ -50,12 +52,18 @@ rfl
   reindex_linear_equiv (equiv.refl m) (equiv.refl n) = linear_equiv.refl R _ :=
 linear_equiv.ext $ λ _, rfl
 
+lemma reindex_linear_equiv_mul {o o' : Type*} [fintype o] [fintype o'] [semiring R]
+  (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : matrix m n R) (N : matrix n o R) :
+  reindex_linear_equiv eₘ eₒ (M ⬝ N) =
+    reindex_linear_equiv eₘ eₙ M ⬝ reindex_linear_equiv eₙ eₒ N :=
+minor_mul_equiv M N _ _ _
+
 /-- For square matrices, the natural map that reindexes a matrix's rows and columns with equivalent
 types, `matrix.reindex`, is an equivalence of algebras. -/
 def reindex_alg_equiv [comm_semiring R] [decidable_eq m] [decidable_eq n]
   (e : m ≃ n) : matrix m m R ≃ₐ[R] matrix n n R :=
 { to_fun    := reindex e e,
-  map_mul'  := λ M N, minor_mul_equiv M N e.symm e.symm e.symm,
+  map_mul'  := reindex_linear_equiv_mul e e e,
   commutes' := λ r, by simp [algebra_map, algebra.to_ring_hom, minor_smul],
   ..(reindex_linear_equiv e e) }
 
@@ -73,6 +81,11 @@ rfl
   reindex_alg_equiv (equiv.refl m) = (alg_equiv.refl : _ ≃ₐ[R] _) :=
 alg_equiv.ext $ λ _, rfl
 
+lemma reindex_alg_equiv_mul [comm_semiring R] [decidable_eq m] [decidable_eq n]
+  (e : m ≃ n) (M : matrix m m R) (N : matrix m m R) :
+  reindex_alg_equiv e (M ⬝ N) = reindex_alg_equiv e M ⬝ reindex_alg_equiv e N :=
+(reindex_alg_equiv e).map_mul M N
+
 /-- Reindexing both indices along the same equivalence preserves the determinant.
 
 For the `simp` version of this lemma, see `det_minor_equiv_self`.
@@ -92,4 +105,3 @@ lemma det_reindex_alg_equiv [decidable_eq m] [decidable_eq n] [comm_ring R]
 det_reindex_self e A
 
 end matrix
-

src/linear_algebra/matrix/to_lin.lean

@@ -135,6 +135,11 @@ by { ext, rw [matrix.one_apply, linear_map.to_matrix'_apply, id_apply] }
   matrix.to_lin' (M ⬝ N) = (matrix.to_lin' M).comp (matrix.to_lin' N) :=
 by { ext, simp }
 
+/-- Shortcut lemma for `matrix.to_lin'_mul` and `linear_map.comp_apply` -/
+lemma matrix.to_lin'_mul_apply [decidable_eq m] (M : matrix l m R) (N : matrix m n R) (x) :
+  matrix.to_lin' (M ⬝ N) x = (matrix.to_lin' M (matrix.to_lin' N x)) :=
+by rw [matrix.to_lin'_mul, linear_map.comp_apply]
+
 lemma linear_map.to_matrix'_comp [decidable_eq l]
   (f : (n → R) →ₗ[R] (m → R)) (g : (l → R) →ₗ[R] (n → R)) :
   (f.comp g).to_matrix' = f.to_matrix' ⬝ g.to_matrix' :=
@@ -147,6 +152,19 @@ lemma linear_map.to_matrix'_mul [decidable_eq m]
   (f * g).to_matrix' = f.to_matrix' ⬝ g.to_matrix' :=
 linear_map.to_matrix'_comp f g
 
+/-- If `M` and `M'` are each other's inverse matrices, they provide an equivalence between `m → A`
+and `n → A` corresponding to `M.mul_vec` and `M'.mul_vec`. -/
+@[simps]
+def matrix.to_lin'_of_inv [decidable_eq m]
+  {M : matrix m n R} {M' : matrix n m R}
+  (hMM' : M ⬝ M' = 1) (hM'M : M' ⬝ M = 1) :
+  (m → R) ≃ₗ[R] (n → R) :=
+{ to_fun := matrix.to_lin' M',
+  inv_fun := M.to_lin',
+  left_inv := λ x, by rw [← matrix.to_lin'_mul_apply, hMM', matrix.to_lin'_one, id_apply],
+  right_inv := λ x, by rw [← matrix.to_lin'_mul_apply, hM'M, matrix.to_lin'_one, id_apply],
+  .. matrix.to_lin' M' }
+
 /-- Linear maps `(n → R) →ₗ[R] (n → R)` are algebra equivalent to `matrix n n R`. -/
 def linear_map.to_matrix_alg_equiv' : ((n → R) →ₗ[R] (n → R)) ≃ₐ[R] matrix n n R :=
 alg_equiv.of_linear_equiv linear_map.to_matrix' linear_map.to_matrix'_mul
@@ -346,6 +364,26 @@ begin
   repeat { rw linear_map.to_matrix_to_lin },
 end
 
+/-- Shortcut lemma for `matrix.to_lin_mul` and `linear_map.comp_apply`. -/
+lemma matrix.to_lin_mul_apply [decidable_eq m]
+  (A : matrix l m R) (B : matrix m n R) (x) :
+  matrix.to_lin v₁ v₃ (A ⬝ B) x =
+    (matrix.to_lin v₂ v₃ A) (matrix.to_lin v₁ v₂ B x) :=
+by rw [matrix.to_lin_mul v₁ v₂, linear_map.comp_apply]
+
+/-- If `M` and `M` are each other's inverse matrices, `matrix.to_lin M` and `matrix.to_lin M'`
+form a linear equivalence. -/
+@[simps]
+def matrix.to_lin_of_inv [decidable_eq m]
+  {M : matrix m n R} {M' : matrix n m R}
+  (hMM' : M ⬝ M' = 1) (hM'M : M' ⬝ M = 1) :
+  M₁ ≃ₗ[R] M₂ :=
+{ to_fun := matrix.to_lin v₁ v₂ M,
+  inv_fun := matrix.to_lin v₂ v₁ M',
+  left_inv := λ x, by rw [← matrix.to_lin_mul_apply, hM'M, matrix.to_lin_one, id_apply],
+  right_inv := λ x, by rw [← matrix.to_lin_mul_apply, hMM', matrix.to_lin_one, id_apply],
+  .. matrix.to_lin v₁ v₂ M }
+
 /-- Given a basis of a module `M₁` over a commutative ring `R`, we get an algebra
 equivalence between linear maps `M₁ →ₗ M₁` and square matrices over `R` indexed by the basis. -/
 def linear_map.to_matrix_alg_equiv :