Changing the index type of a matrix #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.reindexis anR-linear equivalence betweenA-matrices.matrix.reindex_alg_equiv R:matrix.reindexis anR-algebra equivalence betweenR-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]
[add_comm_monoid A]
[module R A]
(eₘ : m ≃ m')
(eₙ : n ≃ n') :
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 := _}
@[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') :
(matrix.reindex_linear_equiv R A eₘ eₙ).symm = matrix.reindex_linear_equiv R A 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]
[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)
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') :
⇑(matrix.reindex_linear_equiv R A e 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]
[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).mul (⇑(matrix.reindex_linear_equiv R A eₙ eₒ) N) = ⇑(matrix.reindex_linear_equiv R A eₘ eₒ) (M.mul 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]
[module R A]
[fintype n]
[decidable_eq o]
(e₁ : o ≃ n)
(e₂ : o ≃ n')
(M : matrix m n A) :
M.mul (⇑(matrix.reindex_linear_equiv R A e₁ e₂) 1) = ⇑(matrix.reindex_linear_equiv R A (equiv.refl m) (e₁.symm.trans e₂)) M
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) :
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' := _}
@[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
@[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_refl
{m : Type u_2}
(R : Type u_11)
[comm_semiring R]
[fintype m]
[decidable_eq m] :
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.mul N) = (⇑(matrix.reindex_alg_equiv R e) M).mul (⇑(matrix.reindex_alg_equiv R e) 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 : 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_submatrix_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) :
(⇑(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_submatrix_equiv_self.