mathlib documentation

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 #

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] [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
@[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
@[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') :
@[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] :
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₂')
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₂'))
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
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') :
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) :
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) :
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
@[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) :
@[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) :
@[simp]
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) :
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) :

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

Reindexing both indices along the same equivalence preserves the determinant.

For the simp version of this lemma, see det_minor_equiv_self.