# Changing the index type of a matrix #

This file concerns the map Matrix.reindex, mapping a m by n matrix to an m' by n' matrix, as long as m ≃ m' and n ≃ n'.

## Main definitions #

• Matrix.reindexLinearEquiv R A: Matrix.reindex is an R-linear equivalence between A-matrices.
• Matrix.reindexAlgEquiv R: Matrix.reindex is an R-algebra equivalence between R-matrices.

## Tags #

matrix, reindex

def Matrix.reindexLinearEquiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [] [] [Module R A] (eₘ : m m') (eₙ : n n') :
Matrix m n A ≃ₗ[R] Matrix m' n' A

The natural map that reindexes a matrix's rows and columns with equivalent types, Matrix.reindex, is a linear equivalence.

Equations
• = let __src := Matrix.reindex eₘ eₙ; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := }
Instances For
@[simp]
theorem Matrix.reindexLinearEquiv_apply {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [] [] [Module R A] (eₘ : m m') (eₙ : n n') (M : Matrix m n A) :
() M = (Matrix.reindex eₘ eₙ) M
@[simp]
theorem Matrix.reindexLinearEquiv_symm {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [] [] [Module R A] (eₘ : m m') (eₙ : n n') :
().symm = Matrix.reindexLinearEquiv R A eₘ.symm eₙ.symm
@[simp]
theorem Matrix.reindexLinearEquiv_refl_refl {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [] [] [Module R A] :
theorem Matrix.reindexLinearEquiv_trans {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) (A : Type u_12) [] [] [Module R A] (e₁ : m m') (e₂ : n n') (e₁' : m' m'') (e₂' : n' n'') :
≪≫ₗ Matrix.reindexLinearEquiv R A e₁' e₂' = Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')
theorem Matrix.reindexLinearEquiv_comp {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) (A : Type u_12) [] [] [Module R A] (e₁ : m m') (e₂ : n n') (e₁' : m' m'') (e₂' : n' n'') :
(Matrix.reindexLinearEquiv R A e₁' e₂') () = (Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂'))
theorem Matrix.reindexLinearEquiv_comp_apply {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} {m'' : Type u_9} {n'' : Type u_10} (R : Type u_11) (A : Type u_12) [] [] [Module R A] (e₁ : m m') (e₂ : n n') (e₁' : m' m'') (e₂' : n' n'') (M : Matrix m n A) :
(Matrix.reindexLinearEquiv R A e₁' e₂') (() M) = (Matrix.reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')) M
theorem Matrix.reindexLinearEquiv_one {m : Type u_2} {m' : Type u_6} (R : Type u_11) (A : Type u_12) [] [] [Module R A] [] [] [One A] (e : m m') :
() 1 = 1
theorem Matrix.reindexLinearEquiv_mul {m : Type u_2} {n : Type u_3} {o : Type u_4} {m' : Type u_6} {n' : Type u_7} {o' : Type u_8} (R : Type u_11) (A : Type u_12) [] [] [Module R A] [] [Fintype n'] (eₘ : m m') (eₙ : n n') (eₒ : o o') (M : Matrix m n A) (N : Matrix n o A) :
() M * () N = () (M * N)
theorem Matrix.mul_reindexLinearEquiv_one {m : Type u_2} {n : Type u_3} {o : Type u_4} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [] [] [Module R A] [] [] (e₁ : o n) (e₂ : o n') (M : Matrix m n A) :
M * () 1 = (Matrix.reindexLinearEquiv R A () (e₁.symm.trans e₂)) M
def Matrix.reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [] [] [] [] [] (e : m n) :
Matrix m m R ≃ₐ[R] Matrix n n R

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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem Matrix.reindexAlgEquiv_apply {m : Type u_2} {n : Type u_3} (R : Type u_11) [] [] [] [] [] (e : m n) (M : Matrix m m R) :
() M = () M
@[simp]
theorem Matrix.reindexAlgEquiv_symm {m : Type u_2} {n : Type u_3} (R : Type u_11) [] [] [] [] [] (e : m n) :
().symm = Matrix.reindexAlgEquiv R e.symm
@[simp]
theorem Matrix.reindexAlgEquiv_refl {m : Type u_2} (R : Type u_11) [] [] [] :
= AlgEquiv.refl
theorem Matrix.reindexAlgEquiv_mul {m : Type u_2} {n : Type u_3} (R : Type u_11) [] [] [] [] [] (e : m n) (M : Matrix m m R) (N : Matrix m m R) :
() (M * N) = () M * () N
theorem Matrix.det_reindexLinearEquiv_self {m : Type u_2} {n : Type u_3} (R : Type u_11) [] [] [] [] [] (e : m n) (M : Matrix m m R) :
(() M).det = M.det

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_submatrix_equiv_self.

theorem Matrix.det_reindexAlgEquiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [] [] [] [] [] (e : m n) (A : Matrix m m R) :
(() A).det = A.det

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_submatrix_equiv_self.