feat(linear_algebra/matrix/reindex): add some lemmas (#7963)

From LTE
Added lemmas `reindex_linear_equiv_trans`, `reindex_linear_equiv_comp`, `reindex_linear_equiv_comp_apply`, `reindex_linear_equiv_one` and `mul_reindex_linear_equiv_mul_one` needed in LTE.



Co-authored-by: Filippo Nuccio <nuccio@cluster18-math.univ-lyon1.fr>
Co-authored-by: Filippo A. E. Nuccio <65080144+faenuccio@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/data/matrix/basic.lean

@@ -882,26 +882,27 @@ lemma star_mul (M N : matrix n n α) : star (M ⬝ N) = star N ⬝ star M := sta
 
 end star_ring
 
-/-- `M.minor row col` is the matrix obtained by reindexing the rows and the lines of
-    `M`, such that `M.minor row col i j = M (row i) (col j)`. Note that the total number
-    of row/colums doesn't have to be preserved. -/
-def minor (A : matrix m n α) (row : l → m) (col : o → n) : matrix l o α :=
-λ i j, A (row i) (col j)
+/-- Given maps `(r_reindex : l → m)` and  `(c_reindex : o → n)` reindexing the rows and columns of
+a matrix `M : matrix m n α`, the matrix `M.minor r_reindex c_reindex : matrix l o α` is defined
+by `(M.minor r_reindex c_reindex) i j = M (r_reindex i) (c_reindex j)` for `(i,j) : l × o`.
+Note that the total number of row and columns does not have to be preserved. -/
+def minor (A : matrix m n α) (r_reindex : l → m) (c_reindex : o → n) : matrix l o α :=
+λ i j, A (r_reindex i) (c_reindex j)
 
-@[simp] lemma minor_apply (A : matrix m n α) (row : l → m) (col : o → n) (i j) :
-  A.minor row col i j = A (row i) (col j) := rfl
+@[simp] lemma minor_apply (A : matrix m n α) (r_reindex : l → m) (c_reindex : o → n) (i j) :
+  A.minor r_reindex c_reindex i j = A (r_reindex i) (c_reindex j) := rfl
 
 @[simp] lemma minor_id_id (A : matrix m n α) :
   A.minor id id = A :=
 ext $ λ _ _, rfl
 
 @[simp] lemma minor_minor {l₂ o₂ : Type*} [fintype l₂] [fintype o₂] (A : matrix m n α)
-  (row₁ : l → m) (col₁ : o → n) (row₂ : l₂ → l) (col₂ : o₂ → o) :
-  (A.minor row₁ col₁).minor row₂ col₂ = A.minor (row₁ ∘ row₂) (col₁ ∘ col₂) :=
+  (r₁ : l → m) (c₁ : o → n) (r₂ : l₂ → l) (c₂ : o₂ → o) :
+  (A.minor r₁ c₁).minor r₂ c₂ = A.minor (r₁ ∘ r₂) (c₁ ∘ c₂) :=
 ext $ λ _ _, rfl
 
-@[simp] lemma transpose_minor (A : matrix m n α) (row : l → m) (col : o → n) :
-  (A.minor row col)ᵀ = Aᵀ.minor col row :=
+@[simp] lemma transpose_minor (A : matrix m n α) (r_reindex : l → m) (c_reindex : o → n) :
+  (A.minor r_reindex c_reindex)ᵀ = Aᵀ.minor c_reindex r_reindex :=
 ext $ λ _ _, rfl
 
 lemma minor_add [has_add α] (A B : matrix m n α) :
@@ -921,8 +922,8 @@ lemma minor_smul {R : Type*} [semiring R] [add_comm_monoid α] [module R α] (r
   (A : matrix m n α) :
   ((r • A : matrix m n α).minor : (l → m) → (o → n) → matrix l o α) = r • A.minor := rfl
 
-/-- If the minor doesn't repeat elements, then when applied to a diagonal matrix the result is
-diagonal. -/
+/-- Given a `(m × m)` diagonal matrix defined by a map `d : m → α`, if the reindexing map `e` is
+  injective, then the resulting matrix is again diagonal. -/
 lemma minor_diagonal [has_zero α] [decidable_eq m] [decidable_eq l] (d : m → α) (e : l → m)
   (he : function.injective e) :
   (diagonal d).minor e e = diagonal (d ∘ e) :=
@@ -944,6 +945,7 @@ lemma minor_mul [semiring α] {p q : Type*} [fintype p] [fintype q]
   (M ⬝ N).minor e₁ e₃ = (M.minor e₁ e₂) ⬝ (N.minor e₂ e₃) :=
 ext $ λ _ _, (he₂.sum_comp _).symm
 
+
 /-! `simp` lemmas for `matrix.minor`s interaction with `matrix.diagonal`, `1`, and `matrix.mul` for
 when the mappings are bundled. -/
 
@@ -974,6 +976,28 @@ lemma minor_mul_equiv [semiring α] {p q : Type*} [fintype p] [fintype q]
   (M ⬝ N).minor e₁ e₃ = (M.minor e₁ e₂) ⬝ (N.minor e₂ e₃) :=
 minor_mul M N e₁ e₂ e₃ e₂.bijective
 
+lemma mul_minor_one [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],
+  simp only [matrix.mul_one, minor_minor, function.comp.right_id, minor_id_id,
+    equiv.symm_comp_self],
+end
+
+lemma one_minor_mul [semiring α] [decidable_eq o] (e₁ : l → o) (e₂ : m ≃ o) (M : matrix m n α) :
+  ((1 : matrix o o α).minor e₁ e₂).mul M = minor M (e₂.symm ∘ e₁) id :=
+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],
+  simp only [matrix.one_mul, minor_minor, function.comp.right_id, minor_id_id,
+    equiv.symm_comp_self],
+end
+
 /-- The natural map that reindexes a matrix's rows and columns with equivalent types is an
 equivalence. -/
 def reindex (eₘ : m ≃ l) (eₙ : n ≃ o) : matrix m n α ≃ matrix l o α :=

src/linear_algebra/matrix/reindex.lean

@@ -25,10 +25,15 @@ matrix, reindex
 
 namespace matrix
 
+open equiv
+
 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 {m'' n'' : Type*} [fintype m''] [fintype n'']
 variables {R : Type*}
 
 /-- The natural map that reindexes a matrix's rows and columns with equivalent types,
@@ -52,14 +57,44 @@ 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]
+lemma reindex_linear_equiv_trans [semiring R] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'')
+  (e₂' : n' ≃ n'') : (reindex_linear_equiv e₁ e₂).trans (reindex_linear_equiv e₁' e₂') =
+   (reindex_linear_equiv (e₁.trans e₁') (e₂.trans e₂') : _ ≃ₗ[R] _) :=
+by { ext, refl }
+
+lemma reindex_linear_equiv_comp [semiring R] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'')
+  (e₂' : n' ≃ n'') :
+  (reindex_linear_equiv e₁' e₂' : _ ≃ₗ[R] _) ∘ (reindex_linear_equiv e₁ e₂ : _ ≃ₗ[R] _)
+  = reindex_linear_equiv (e₁.trans e₁') (e₂.trans e₂') :=
+by { rw [← reindex_linear_equiv_trans], refl }
+
+lemma reindex_linear_equiv_comp_apply [semiring R] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'')
+  (e₂' : n' ≃ n'') (M : matrix m n R) :
+  (reindex_linear_equiv e₁' e₂') (reindex_linear_equiv e₁ e₂ M) =
+    reindex_linear_equiv (e₁.trans e₁') (e₂.trans e₂') M :=
+minor_minor _ _ _ _ _
+
+lemma reindex_linear_equiv_one [semiring R] [decidable_eq m] [decidable_eq m']
+  (e : m ≃ m') : (reindex_linear_equiv e e (1 : matrix m m R)) = 1 :=
+minor_one_equiv e.symm
+
+variables {o o' : Type*} [fintype o] [fintype o']
+
+lemma reindex_linear_equiv_mul [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. -/
+lemma mul_reindex_linear_equiv_one [semiring R] [decidable_eq o] (e₁ : o ≃ n) (e₂ : o ≃ n')
+  (M : matrix m n R) : M.mul (reindex_linear_equiv e₁ e₂ 1) =
+    reindex_linear_equiv (equiv.refl m) (e₁.symm.trans e₂) M :=
+mul_minor_one _ _ _
+
+/--
+For square matrices with coefficients in commutative semirings, 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,