# mathlibdocumentation

linear_algebra.matrix.reindex

# 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.reindex_linear_equiv R A: matrix.reindex is an R-linear equivalence between A-matrices.
• matrix.reindex_alg_equiv R: matrix.reindex is an R-algebra equivalence between R-matrices.

## Tags #

matrix, reindex

def matrix.reindex_linear_equiv {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [semiring R] [ A] (eₘ : m m') (eₙ : n n') :
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
@[simp]
theorem matrix.reindex_linear_equiv_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) [semiring R] [ A] (eₘ : m m') (eₙ : n n') (M : n A) :
eₘ eₙ) M = eₙ) M
@[simp]
theorem matrix.reindex_linear_equiv_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) [semiring R] [ A] (eₘ : m m') (eₙ : n n') :
eₘ eₙ).symm = eₙ.symm
@[simp]
theorem matrix.reindex_linear_equiv_refl_refl {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [semiring R] [ A] :
(equiv.refl n) = (matrix m n A)
theorem matrix.reindex_linear_equiv_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) [semiring R] [ A] (e₁ : m m') (e₂ : n n') (e₁' : m' m'') (e₂' : n' n'') :
e₁ e₂).trans e₁' e₂') = (e₁.trans e₁') (e₂.trans e₂')
theorem matrix.reindex_linear_equiv_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) [semiring R] [ A] (e₁ : m m') (e₂ : n n') (e₁' : m' m'') (e₂' : n' n'') :
e₁' e₂') e₁ e₂) = (e₁.trans e₁') (e₂.trans e₂'))
theorem matrix.reindex_linear_equiv_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) [semiring R] [ A] (e₁ : m m') (e₂ : n n') (e₁' : m' m'') (e₂' : n' n'') (M : n A) :
e₁' e₂') ( e₁ e₂) M) = (e₁.trans e₁') (e₂.trans e₂')) M
theorem matrix.reindex_linear_equiv_one {m : Type u_2} {m' : Type u_6} (R : Type u_11) (A : Type u_12) [semiring R] [ A] [decidable_eq m] [decidable_eq m'] [has_one A] (e : m m') :
e) 1 = 1
theorem matrix.reindex_linear_equiv_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) [semiring R] [semiring A] [ A] [fintype n] [fintype n'] (eₘ : m m') (eₙ : n n') (eₒ : o o') (M : n A) (N : o A) :
eₘ eₒ) (M N) = eₘ eₙ) M eₙ eₒ) N
theorem matrix.mul_reindex_linear_equiv_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) [semiring R] [semiring A] [ A] [fintype n] [fintype o] [decidable_eq o] (e₁ : o n) (e₂ : o n') (M : n A) :
M e₁ e₂) 1 = (e₁.symm.trans e₂)) M
def matrix.reindex_alg_equiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (e : m n) :
m R ≃ₐ[R] 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
@[simp]
theorem matrix.reindex_alg_equiv_apply {m : Type u_2} {n : Type u_3} (R : Type u_11) [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (e : m n) (M : m R) :
M = e) M
@[simp]
theorem matrix.reindex_alg_equiv_symm {m : Type u_2} {n : Type u_3} (R : Type u_11) [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (e : m n) :
@[simp]
theorem matrix.reindex_alg_equiv_refl {m : Type u_2} (R : Type u_11) [fintype m] [decidable_eq m] :
theorem matrix.reindex_alg_equiv_mul {m : Type u_2} {n : Type u_3} (R : Type u_11) [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (e : m n) (M N : m R) :
(M N) = M N
theorem matrix.det_reindex_linear_equiv_self {m : Type u_2} {n : Type u_3} (R : Type u_11) [comm_ring R] [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] (e : m n) (M : m R) :
( e) M).det = M.det

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_minor_equiv_self.

theorem matrix.det_reindex_alg_equiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [comm_ring R] [fintype m] [decidable_eq m] [fintype n] [decidable_eq n] (e : m n) (A : 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_minor_equiv_self.