Mathlib.LinearAlgebra.Matrix.Reindex

Matrix.reindexLinearEquiv definition

(eₘ : m ≃ m') (eₙ : n ≃ n') : Matrix m n A ≃ₗ[R] Matrix m' n' A

Full source

/-- The natural map that reindexes a matrix's rows and columns with equivalent types,
`Matrix.reindex`, is a linear equivalence. -/
def reindexLinearEquiv (eₘ : m ≃ m') (eₙ : n ≃ n') : MatrixMatrix m n A ≃ₗ[R] Matrix m' n' A :=
  { reindex eₘ eₙ with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

Linear equivalence of matrix reindexing

Informal description

Given a commutative ring $ R $, types $ m, m', n, n' $, and an $ R $-algebra $ A $, the function `Matrix.reindexLinearEquiv` constructs an $ R $-linear equivalence between the space of $ m \times n $ matrices over $ A $ and the space of $ m' \times n' $ matrices over $ A $, induced by bijections $ e_m : m \simeq m' $ and $ e_n : n \simeq n' $. This equivalence reindexes the rows and columns of a matrix according to the given bijections.

Matrix.reindexLinearEquiv_apply theorem

(eₘ : m ≃ m') (eₙ : n ≃ n') (M : Matrix m n A) : reindexLinearEquiv R A eₘ eₙ M = reindex eₘ eₙ M

Full source

@[simp]
theorem reindexLinearEquiv_apply (eₘ : m ≃ m') (eₙ : n ≃ n') (M : Matrix m n A) :
    reindexLinearEquiv R A eₘ eₙ M = reindex eₘ eₙ M :=
  rfl

Application of Matrix Reindexing Linear Equivalence

Informal description

Given a commutative ring $R$, an $R$-algebra $A$, and bijections $e_m : m \simeq m'$ and $e_n : n \simeq n'$, the linear equivalence `reindexLinearEquiv R A eₘ eₙ` applied to a matrix $M$ of size $m \times n$ over $A$ is equal to the reindexed matrix `reindex eₘ eₙ M` of size $m' \times n'$.

Matrix.reindexLinearEquiv_symm theorem

 (eₘ : m ≃ m') (eₙ : n ≃ n') : (reindexLinearEquiv R A eₘ eₙ).symm = reindexLinearEquiv R A eₘ.symm eₙ.symm

Full source

@[simp]
theorem reindexLinearEquiv_symm (eₘ : m ≃ m') (eₙ : n ≃ n') :
    (reindexLinearEquiv R A eₘ eₙ).symm = reindexLinearEquiv R A eₘ.symm eₙ.symm :=
  rfl

Inverse of Matrix Reindexing Linear Equivalence via Symmetric Bijections

Informal description

Given a commutative ring $R$, an $R$-algebra $A$, and bijections $e_m : m \simeq m'$ and $e_n : n \simeq n'$, the inverse of the linear equivalence `reindexLinearEquiv R A eₘ eₙ` is equal to the linear equivalence `reindexLinearEquiv R A eₘ.symm eₙ.symm`, where $e_m^{-1}$ and $e_n^{-1}$ are the inverse bijections of $e_m$ and $e_n$ respectively.

Matrix.reindexLinearEquiv_refl_refl theorem

: reindexLinearEquiv R A (Equiv.refl m) (Equiv.refl n) = LinearEquiv.refl R _

Full source

@[simp]
theorem reindexLinearEquiv_refl_refl :
    reindexLinearEquiv R A (Equiv.refl m) (Equiv.refl n) = LinearEquiv.refl R _ :=
  LinearEquiv.ext fun _ => rfl

Identity Reindexing Yields Identity Matrix Equivalence

Informal description

The matrix reindexing linear equivalence applied to the identity equivalences on the row and column index types $m$ and $n$ is equal to the identity linear equivalence on the space of $m \times n$ matrices over $A$.

Matrix.reindexLinearEquiv_trans theorem

 (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
  (reindexLinearEquiv R A e₁ e₂).trans (reindexLinearEquiv R A e₁' e₂') =
    (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : _ ≃ₗ[R] _)

Full source

theorem reindexLinearEquiv_trans (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
    (reindexLinearEquiv R A e₁ e₂).trans (reindexLinearEquiv R A e₁' e₂') =
      (reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') : _ ≃ₗ[R] _) := by
  ext
  rfl

Composition of Matrix Reindexing Linear Equivalences via Equivalence Composition

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and let $m, m', m''$ and $n, n', n''$ be types. Given equivalences $e_1 : m \simeq m'$, $e_2 : n \simeq n'$, $e_1' : m' \simeq m''$, and $e_2' : n' \simeq n''$, the composition of the matrix reindexing linear equivalences $\text{reindexLinearEquiv}_{R,A}(e_1, e_2)$ and $\text{reindexLinearEquiv}_{R,A}(e_1', e_2')$ is equal to the matrix reindexing linear equivalence $\text{reindexLinearEquiv}_{R,A}(e_1 \circ e_1', e_2 \circ e_2')$.

Matrix.reindexLinearEquiv_comp theorem

 (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
  reindexLinearEquiv R A e₁' e₂' ∘ reindexLinearEquiv R A e₁ e₂ = reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂')

Full source

theorem reindexLinearEquiv_comp (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') :
    reindexLinearEquivreindexLinearEquiv R A e₁' e₂' ∘ reindexLinearEquiv R A e₁ e₂ =
      reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') := by
  rw [← reindexLinearEquiv_trans]
  rfl

Composition of Matrix Reindexing Linear Equivalences via Equivalence Composition

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and let $m, m', m''$ and $n, n', n''$ be types. Given bijections $e_1 : m \simeq m'$, $e_2 : n \simeq n'$, $e_1' : m' \simeq m''$, and $e_2' : n' \simeq n''$, the composition of the matrix reindexing linear equivalences $\text{reindexLinearEquiv}_{R,A}(e_1, e_2)$ and $\text{reindexLinearEquiv}_{R,A}(e_1', e_2')$ is equal to the matrix reindexing linear equivalence $\text{reindexLinearEquiv}_{R,A}(e_1 \circ e_1', e_2 \circ e_2')$.

Matrix.reindexLinearEquiv_comp_apply theorem

 (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'') (M : Matrix m n A) :
  (reindexLinearEquiv R A e₁' e₂') (reindexLinearEquiv R A e₁ e₂ M) =
    reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') M

Full source

theorem reindexLinearEquiv_comp_apply (e₁ : m ≃ m') (e₂ : n ≃ n') (e₁' : m' ≃ m'') (e₂' : n' ≃ n'')
    (M : Matrix m n A) :
    (reindexLinearEquiv R A e₁' e₂') (reindexLinearEquiv R A e₁ e₂ M) =
      reindexLinearEquiv R A (e₁.trans e₁') (e₂.trans e₂') M :=
  submatrix_submatrix _ _ _ _ _

Composition of Matrix Reindexing Equivalences

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $m, m', m'', n, n', n''$ be types. Given bijections $e₁ : m \simeq m'$, $e₂ : n \simeq n'$, $e₁' : m' \simeq m''$, $e₂' : n' \simeq n''$, and a matrix $M \in \text{Matrix}_{m \times n}(A)$, the following equality holds: \[ \text{reindex}(e₁', e₂') \circ \text{reindex}(e₁, e₂)(M) = \text{reindex}(e₁ \circ e₁', e₂ \circ e₂')(M) \] where $\text{reindex}(e_r, e_c)$ denotes the matrix reindexing operation via row bijection $e_r$ and column bijection $e_c$.

Matrix.reindexLinearEquiv_one theorem

[DecidableEq m] [DecidableEq m'] [One A] (e : m ≃ m') : reindexLinearEquiv R A e e (1 : Matrix m m A) = 1

Full source

theorem reindexLinearEquiv_one [DecidableEq m] [DecidableEq m'] [One A] (e : m ≃ m') :
    reindexLinearEquiv R A e e (1 : Matrix m m A) = 1 :=
  submatrix_one_equiv e.symm

Reindexing Preserves Identity Matrix: $\text{reindex}(e, e)(I) = I$

Informal description

Let $m$ and $m'$ be types with decidable equality, and let $A$ be a type with a multiplicative identity element. For any bijection $e : m \simeq m'$, the reindexing of the identity matrix (of size $m \times m$) via $e$ for both rows and columns yields the identity matrix (of size $m' \times m'$). That is, \[ \text{reindex}(e, e)(I_{m \times m}) = I_{m' \times m'} \] where $\text{reindex}(e_r, e_c)$ denotes the matrix reindexing operation via row bijection $e_r$ and column bijection $e_c$, and $I$ denotes the identity matrix.

Matrix.reindexLinearEquiv_mul theorem

 [Fintype n] [Fintype n'] (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o') (M : Matrix m n A) (N : Matrix n o A) :
  reindexLinearEquiv R A eₘ eₙ M * reindexLinearEquiv R A eₙ eₒ N = reindexLinearEquiv R A eₘ eₒ (M * N)

Full source

theorem reindexLinearEquiv_mul [Fintype n] [Fintype n'] (eₘ : m ≃ m') (eₙ : n ≃ n') (eₒ : o ≃ o')
    (M : Matrix m n A) (N : Matrix n o A) :
    reindexLinearEquiv R A eₘ eₙ M * reindexLinearEquiv R A eₙ eₒ N =
      reindexLinearEquiv R A eₘ eₒ (M * N) :=
  submatrix_mul_equiv M N _ _ _

Matrix Reindexing Preserves Multiplication: $\text{reindex}(e_m, e_n)(M) \cdot \text{reindex}(e_n, e_o)(N) = \text{reindex}(e_m, e_o)(M \cdot N)$

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $m, m', n, n', o, o'$ be types with finite cardinalities. Given bijections $e_m : m \simeq m'$, $e_n : n \simeq n'$, $e_o : o \simeq o'$, and matrices $M \in \text{Matrix}_{m \times n}(A)$, $N \in \text{Matrix}_{n \times o}(A)$, the following equality holds: \[ \text{reindex}(e_m, e_n)(M) \cdot \text{reindex}(e_n, e_o)(N) = \text{reindex}(e_m, e_o)(M \cdot N) \] where $\text{reindex}(e_r, e_c)$ denotes the matrix reindexing operation via row bijection $e_r$ and column bijection $e_c$, and $\cdot$ denotes matrix multiplication.

Matrix.mul_reindexLinearEquiv_one theorem

 [Fintype n] [DecidableEq o] (e₁ : o ≃ n) (e₂ : o ≃ n') (M : Matrix m n A) :
  M * (reindexLinearEquiv R A e₁ e₂ 1) = reindexLinearEquiv R A (Equiv.refl m) (e₁.symm.trans e₂) M

Full source

theorem mul_reindexLinearEquiv_one [Fintype n] [DecidableEq o] (e₁ : o ≃ n) (e₂ : o ≃ n')
    (M : Matrix m n A) :
    M * (reindexLinearEquiv R A e₁ e₂ 1) =
      reindexLinearEquiv R A (Equiv.refl m) (e₁.symm.trans e₂) M :=
  haveI := Fintype.ofEquiv _ e₁.symm
  mul_submatrix_one _ _ _

Matrix Multiplication with Reindexed Identity: $M \cdot \text{reindex}(e_1, e_2)(I) = \text{reindex}(\text{id}, e_1^{-1} \circ e_2)(M)$

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $m, n, n', o$ be types with $n$ and $o$ finite. Given bijections $e_1 : o \simeq n$ and $e_2 : o \simeq n'$, and a matrix $M \in \text{Matrix}_{m \times n}(A)$, the following equality holds: \[ M \cdot \text{reindex}(e_1, e_2)(I) = \text{reindex}(\text{id}_m, e_1^{-1} \circ e_2)(M) \] where $I$ is the identity matrix, $\text{reindex}(e_r, e_c)$ denotes matrix reindexing via row bijection $e_r$ and column bijection $e_c$, $\cdot$ denotes matrix multiplication, $\text{id}_m$ is the identity equivalence on $m$, and $\circ$ denotes equivalence composition.

Matrix.reindexAlgEquiv definition

(e : m ≃ n) : Matrix m m A ≃ₐ[R] Matrix n n A

Full source

/-- For square matrices with coefficients in an algebra over a commutative semiring, the natural
    map that reindexes a matrix's rows and columns with equivalent types,
    `Matrix.reindex`, is an equivalence of algebras. -/
def reindexAlgEquiv (e : m ≃ n) : MatrixMatrix m m A ≃ₐ[R] Matrix n n A :=
  { reindexLinearEquiv A A e e with
    toFun := reindex e e
    map_mul' := fun a b => (reindexLinearEquiv_mul A A e e e a b).symm
    commutes' := fun r => by simp [algebraMap, Algebra.algebraMap] }

Algebra equivalence of square matrix reindexing

Informal description

Given a commutative ring $ R $, types $ m $ and $ n $, and an $ R $-algebra $ A $, the function `Matrix.reindexAlgEquiv` constructs an $ R $-algebra equivalence between the space of $ m \times m $ matrices over $ A $ and the space of $ n \times n $ matrices over $ A $, induced by a bijection $ e : m \simeq n $. This equivalence reindexes the rows and columns of a matrix according to the given bijection.

Matrix.reindexAlgEquiv_apply theorem

(e : m ≃ n) (M : Matrix m m A) : reindexAlgEquiv R A e M = reindex e e M

Full source

@[simp]
theorem reindexAlgEquiv_apply (e : m ≃ n) (M : Matrix m m A) :
    reindexAlgEquiv R A e M = reindex e e M :=
  rfl

Matrix Reindexing Algebra Equivalence Application: $\text{reindexAlgEquiv}(e)(M) = \text{reindex}\,e\,e\,M$

Informal description

Given a commutative ring $R$, an $R$-algebra $A$, types $m$ and $n$, and a bijection $e : m \simeq n$, the application of the algebra equivalence `reindexAlgEquiv` to a square matrix $M$ of size $m \times m$ over $A$ is equal to reindexing both the rows and columns of $M$ according to $e$, i.e., $\text{reindexAlgEquiv}_{R,A}(e)(M) = \text{reindex}\,e\,e\,M$.

Matrix.reindexAlgEquiv_symm theorem

(e : m ≃ n) : (reindexAlgEquiv R A e).symm = reindexAlgEquiv R A e.symm

Full source

@[simp]
theorem reindexAlgEquiv_symm (e : m ≃ n) : (reindexAlgEquiv R A e).symm =
    reindexAlgEquiv R A e.symm :=
  rfl

Inverse of Matrix Reindexing Algebra Equivalence

Informal description

For any commutative ring $R$, $R$-algebra $A$, types $m$ and $n$, and bijection $e : m \simeq n$, the inverse of the algebra equivalence $\text{reindexAlgEquiv}_{R,A}(e)$ is equal to $\text{reindexAlgEquiv}_{R,A}(e^{-1})$, where $e^{-1}$ is the inverse bijection of $e$.

Matrix.reindexAlgEquiv_refl theorem

: reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl

Full source

@[simp]
theorem reindexAlgEquiv_refl : reindexAlgEquiv R A (Equiv.refl m) = AlgEquiv.refl :=
  AlgEquiv.ext fun _ => rfl

Reindexing Algebra Equivalence for Identity Bijection is Identity

Informal description

The reindexing algebra equivalence induced by the identity bijection $\text{refl}_m : m \simeq m$ is equal to the identity algebra equivalence on the space of $m \times m$ matrices over $A$.

Matrix.reindexAlgEquiv_mul theorem

 (e : m ≃ n) (M : Matrix m m A) (N : Matrix m m A) :
  reindexAlgEquiv R A e (M * N) = reindexAlgEquiv R A e M * reindexAlgEquiv R A e N

Full source

theorem reindexAlgEquiv_mul (e : m ≃ n) (M : Matrix m m A) (N : Matrix m m A) :
    reindexAlgEquiv R A e (M * N) = reindexAlgEquiv R A e M * reindexAlgEquiv R A e N :=
  map_mul ..

Reindexing Algebra Equivalence Preserves Matrix Multiplication

Informal description

Let $R$ be a commutative ring, $A$ an $R$-algebra, and $m$, $n$ be types with a bijection $e : m \simeq n$. For any two $m \times m$ matrices $M$ and $N$ over $A$, the reindexing algebra equivalence $\text{reindexAlgEquiv}_{R,A}(e)$ satisfies \[ \text{reindexAlgEquiv}_{R,A}(e)(M \cdot N) = \text{reindexAlgEquiv}_{R,A}(e)(M) \cdot \text{reindexAlgEquiv}_{R,A}(e)(N). \]

Matrix.det_reindexLinearEquiv_self theorem

 [CommRing R] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n] (e : m ≃ n) (M : Matrix m m R) :
  det (reindexLinearEquiv R R e e M) = det M

Full source

/-- Reindexing both indices along the same equivalence preserves the determinant.

For the `simp` version of this lemma, see `det_submatrix_equiv_self`.
-/
theorem det_reindexLinearEquiv_self [CommRing R] [Fintype m] [DecidableEq m] [Fintype n]
    [DecidableEq n] (e : m ≃ n) (M : Matrix m m R) : det (reindexLinearEquiv R R e e M) = det M :=
  det_reindex_self e M

Determinant Invariance under Linear Reindexing Equivalence

Informal description

Let $R$ be a commutative ring, and let $m$ and $n$ be finite types with decidable equality. Given a bijection $e : m \simeq n$ and an $m \times m$ matrix $M$ over $R$, the determinant of the matrix obtained by reindexing both rows and columns of $M$ via $e$ is equal to the determinant of $M$, i.e., \[ \det(\text{reindexLinearEquiv}_{R,R}(e,e)(M)) = \det(M). \]

Matrix.det_reindexAlgEquiv theorem

 (B : Type*) [CommSemiring R] [CommRing B] [Algebra R B] [Fintype m] [DecidableEq m] [Fintype n] [DecidableEq n]
  (e : m ≃ n) (A : Matrix m m B) : det (reindexAlgEquiv R B e A) = det A

Full source

/-- Reindexing both indices along the same equivalence preserves the determinant.

For the `simp` version of this lemma, see `det_submatrix_equiv_self`.
-/
theorem det_reindexAlgEquiv (B : Type*) [CommSemiring R] [CommRing B] [Algebra R B] [Fintype m]
    [DecidableEq m] [Fintype n] [DecidableEq n] (e : m ≃ n) (A : Matrix m m B) :
    det (reindexAlgEquiv R B e A) = det A :=
  det_reindex_self e A

Determinant Invariance under Matrix Reindexing Algebra Equivalence

Informal description

Let $R$ be a commutative semiring, $B$ a commutative ring with an $R$-algebra structure, and $m$, $n$ finite types with decidable equality. Given a bijection $e : m \simeq n$ and an $m \times m$ matrix $A$ over $B$, the determinant of the matrix obtained by reindexing both rows and columns of $A$ via $e$ is equal to the determinant of $A$, i.e., \[ \det(\text{reindexAlgEquiv}_{R,B}(e)(A)) = \det(A). \]

Mathlib.LinearAlgebra.Matrix.Reindex

Main definitions

Tags