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

source

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] [add_comm_monoid A] [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

matrix.reindex_linear_equiv R A eₘ eₙ = {to_fun := (matrix.reindex eₘ eₙ).to_fun, map_add' := _, map_smul' := _, inv_fun := (matrix.reindex eₘ eₙ).inv_fun, left_inv := _, right_inv := _}

source

@[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] [add_comm_monoid A] [module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') (M : matrix m n A) :

⇑(matrix.reindex_linear_equiv R A eₘ eₙ) M = ⇑(matrix.reindex eₘ eₙ) M

source

@[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] [add_comm_monoid A] [module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') :

(matrix.reindex_linear_equiv R A eₘ eₙ).symm = matrix.reindex_linear_equiv R A eₘ.symm eₙ.symm

source

@[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] [add_comm_monoid A] [module R A] :

matrix.reindex_linear_equiv R A (equiv.refl m) (equiv.refl n) = linear_equiv.refl R (matrix m n A)

source

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] [add_comm_monoid A] [module R A] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :

(matrix.reindex_linear_equiv R A e₁ e₂).trans (matrix.reindex_linear_equiv R A e₁' e₂') = matrix.reindex_linear_equiv R A (e₁.trans e₁') (e₂.trans e₂')

source

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] [add_comm_monoid A] [module R A] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :

⇑(matrix.reindex_linear_equiv R A e₁' e₂') ∘ ⇑(matrix.reindex_linear_equiv R A e₁ e₂) = ⇑(matrix.reindex_linear_equiv R A (e₁.trans e₁') (e₂.trans e₂'))

source

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] [add_comm_monoid A] [module R A] (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') (M : matrix m n A) :

⇑(matrix.reindex_linear_equiv R A e₁' e₂') (⇑(matrix.reindex_linear_equiv R A e₁ e₂) M) = ⇑(matrix.reindex_linear_equiv R A (e₁.trans e₁') (e₂.trans e₂')) M

source

theorem matrix.reindex_linear_equiv_one {m : Type u_2} {m' : Type u_6} (R : Type u_11) (A : Type u_12) [semiring R] [add_comm_monoid A] [module R A] [decidable_eq m] [decidable_eq m'] [has_one A] (e : m ≃ m') :

⇑(matrix.reindex_linear_equiv R A e e) 1 = 1

source

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] [module R A] [fintype n] [fintype n'] (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : matrix m n A) (N : matrix n o A) :

⇑(matrix.reindex_linear_equiv R A eₘ eₙ) M ⬝ ⇑(matrix.reindex_linear_equiv R A eₙ eₒ) N = ⇑(matrix.reindex_linear_equiv R A eₘ eₒ) (M ⬝ N)

source

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] [module R A] [fintype n] [fintype o] [decidable_eq o] (e₁ : o ≃ n) (e₂ : o ≃ n') (M : matrix m n A) :

M ⬝ ⇑(matrix.reindex_linear_equiv R A e₁ e₂) 1 = ⇑(matrix.reindex_linear_equiv R A (equiv.refl m) (e₁.symm.trans e₂)) M

source

def matrix.reindex_alg_equiv {m : Type u_2} {n : Type u_3} (R : Type u_11) [comm_semiring R] [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (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

matrix.reindex_alg_equiv R e = {to_fun := ⇑(matrix.reindex e e), inv_fun := (matrix.reindex_linear_equiv R R e e).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}

source

@[simp]

theorem matrix.reindex_alg_equiv_apply {m : Type u_2} {n : Type u_3} (R : Type u_11) [comm_semiring R] [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (e : m ≃ n) (M : matrix m m R) :

⇑(matrix.reindex_alg_equiv R e) M = ⇑(matrix.reindex e e) M

source

@[simp]

theorem matrix.reindex_alg_equiv_symm {m : Type u_2} {n : Type u_3} (R : Type u_11) [comm_semiring R] [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (e : m ≃ n) :

(matrix.reindex_alg_equiv R e).symm = matrix.reindex_alg_equiv R e.symm

source

@[simp]

theorem matrix.reindex_alg_equiv_refl {m : Type u_2} (R : Type u_11) [comm_semiring R] [fintype m] [decidable_eq m] :

matrix.reindex_alg_equiv R (equiv.refl m) = alg_equiv.refl

source

theorem matrix.reindex_alg_equiv_mul {m : Type u_2} {n : Type u_3} (R : Type u_11) [comm_semiring R] [fintype n] [fintype m] [decidable_eq m] [decidable_eq n] (e : m ≃ n) (M N : matrix m m R) :

⇑(matrix.reindex_alg_equiv R e) (M ⬝ N) = ⇑(matrix.reindex_alg_equiv R e) M ⬝ ⇑(matrix.reindex_alg_equiv R e) N

source

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 : matrix m m R) :

(⇑(matrix.reindex_linear_equiv R R e 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.

source

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 : matrix m m R) :

(⇑(matrix.reindex_alg_equiv R e) 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.