Mathlib.Data.Matrix.Composition

Matrix.comp definition

: Matrix I J (Matrix K L R) ≃ Matrix (I × K) (J × L) R

Full source

/-- I by J matrix where each entry is a K by L matrix is equivalent to
    I × K by J × L matrix -/
@[simps]
def comp : MatrixMatrix I J (Matrix K L R) ≃ Matrix (I × K) (J × L) R where
  toFun m ik jl := m ik.1 jl.1 ik.2 jl.2
  invFun n i j k l := n (i, k) (j, l)
  left_inv _ := rfl
  right_inv _ := rfl

Matrix flattening equivalence

Informal description

The function establishes an equivalence between an $I \times J$ matrix whose entries are $K \times L$ matrices over $R$ and an $(I \times K) \times (J \times L)$ matrix over $R$. Specifically, given a matrix $M$ of type $\text{Matrix}\, I\, J\, (\text{Matrix}\, K\, L\, R)$, the corresponding matrix in $\text{Matrix}\, (I \times K)\, (J \times L)\, R$ is defined by $(i,k,j,l) \mapsto M_{i,j,k,l}$. The inverse operation reconstructs the original nested matrix structure.

Matrix.comp_map_map theorem

(M : Matrix I J (Matrix K L R)) (f : R → R') : comp I J K L _ (M.map (fun M' => M'.map f)) = (comp I J K L _ M).map f

Full source

theorem comp_map_map (M : Matrix I J (Matrix K L R)) (f : R → R') :
  comp I J K L _ (M.map (fun M' => M'.map f)) = (comp I J K L _ M).map f := rfl

Compatibility of Matrix Flattening with Entrywise Mapping

Informal description

For any matrix $M \in \text{Matrix}\, I\, J\, (\text{Matrix}\, K\, L\, R)$ and any function $f : R \to R'$, the composition equivalence $\text{comp}$ satisfies: \[ \text{comp}\, I\, J\, K\, L\, R'\, (M.\text{map}\, (\lambda M', M'.\text{map}\, f)) = (\text{comp}\, I\, J\, K\, L\, R\, M).\text{map}\, f \] where $\text{map}$ applies $f$ to each entry of the matrix.

Matrix.comp_stdBasisMatrix_stdBasisMatrix theorem

 [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (i j k l r) :
  comp I J K L R (stdBasisMatrix i j (stdBasisMatrix k l r)) = stdBasisMatrix (i, k) (j, l) r

Full source

@[simp]
theorem comp_stdBasisMatrix_stdBasisMatrix
    [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (i j k l r) :
    comp I J K L R (stdBasisMatrix i j (stdBasisMatrix k l r))
      = stdBasisMatrix (i, k) (j, l) r := by
  ext ⟨i', k'⟩ ⟨j', l'⟩
  dsimp [comp_apply]
  obtain hi | rfl := ne_or_eq i i'
  · rw [StdBasisMatrix.apply_of_row_ne hi,
      StdBasisMatrix.apply_of_row_ne (ne_of_apply_ne Prod.fst hi), Matrix.zero_apply]
  obtain hj | rfl := ne_or_eq j j'
  · rw [StdBasisMatrix.apply_of_col_ne _ _ hj,
      StdBasisMatrix.apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]
  rw [StdBasisMatrix.apply_same]
  obtain hk | rfl := ne_or_eq k k'
  · rw [StdBasisMatrix.apply_of_row_ne hk,
      StdBasisMatrix.apply_of_row_ne (ne_of_apply_ne Prod.snd hk)]
  obtain hj | rfl := ne_or_eq l l'
  · rw [StdBasisMatrix.apply_of_col_ne _ _ hj,
      StdBasisMatrix.apply_of_col_ne _ _ (ne_of_apply_ne Prod.snd hj)]
  rw [StdBasisMatrix.apply_same, StdBasisMatrix.apply_same]

Composition of Standard Basis Matrices via $\text{comp}$ Equivalence

Informal description

Let $I, J, K, L$ be finite types with decidable equality, and let $R$ be a type with a zero element. For any indices $i \in I$, $j \in J$, $k \in K$, $l \in L$, and any element $r \in R$, the composition equivalence $\text{comp}$ maps the standard basis matrix $\text{stdBasisMatrix}_{i,j}(\text{stdBasisMatrix}_{k,l}(r))$ to the standard basis matrix $\text{stdBasisMatrix}_{(i,k),(j,l)}(r)$.

Matrix.comp_symm_stdBasisMatrix theorem

 [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (ii jj r) :
  (comp I J K L R).symm (stdBasisMatrix ii jj r) = (stdBasisMatrix ii.1 jj.1 (stdBasisMatrix ii.2 jj.2 r))

Full source

@[simp]
theorem comp_symm_stdBasisMatrix
    [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (ii jj r) :
    (comp I J K L R).symm (stdBasisMatrix ii jj r) =
      (stdBasisMatrix ii.1 jj.1 (stdBasisMatrix ii.2 jj.2 r)) :=
  (comp I J K L R).symm_apply_eq.2 <| comp_stdBasisMatrix_stdBasisMatrix _ _ _ _ _ |>.symm

Inverse of Matrix Flattening Equivalence on Standard Basis Matrices

Informal description

Let $I, J, K, L$ be finite types with decidable equality, and let $R$ be a type with a zero element. For any indices $(i,k) \in I \times K$, $(j,l) \in J \times L$, and any element $r \in R$, the inverse of the composition equivalence $\text{comp}$ maps the standard basis matrix $\text{stdBasisMatrix}_{(i,k),(j,l)}(r)$ to the standard basis matrix $\text{stdBasisMatrix}_{i,j}(\text{stdBasisMatrix}_{k,l}(r))$.

Matrix.comp_diagonal_diagonal theorem

 [DecidableEq I] [DecidableEq J] [Zero R] (d : I → J → R) :
  comp I I J J R (diagonal fun i => diagonal fun j => d i j) = diagonal fun ij => d ij.1 ij.2

Full source

@[simp]
theorem comp_diagonal_diagonal [DecidableEq I] [DecidableEq J] [Zero R] (d : I → J → R) :
    comp I I J J R (diagonal fun i => diagonal fun j => d i j)
      = diagonal fun ij => d ij.1 ij.2 := by
  ext ⟨i₁, j₁⟩ ⟨i₂, j₂⟩
  dsimp [comp_apply]
  obtain hi | rfl := ne_or_eq i₁ i₂
  · rw [diagonal_apply_ne _ hi, diagonal_apply_ne _ (ne_of_apply_ne Prod.fst hi),
      Matrix.zero_apply]
  rw [diagonal_apply_eq]
  obtain hj | rfl := ne_or_eq j₁ j₂
  · rw [diagonal_apply_ne _ hj, diagonal_apply_ne _ (ne_of_apply_ne Prod.snd hj)]
  rw [diagonal_apply_eq, diagonal_apply_eq]

Composition of Diagonal Matrices Preserves Diagonal Structure

Informal description

Let $I$ and $J$ be finite types with decidable equality, and let $R$ be a type with a zero element. Given a function $d : I \to J \to R$, the composition equivalence $\text{comp}$ maps the diagonal matrix of diagonal matrices (where the $(i,j)$-th entry is $d(i,j)$) to the diagonal matrix where the $((i,j),(i,j))$-th entry is $d(i,j)$. In other words, the following equality holds: $$ \text{comp}_{I,I,J,J}(R) \left( \text{diagonal} \left( \lambda i, \text{diagonal} (\lambda j, d(i,j)) \right) \right) = \text{diagonal} \left( \lambda (i,j), d(i,j) \right) $$

Matrix.comp_symm_diagonal theorem

 [DecidableEq I] [DecidableEq J] [Zero R] (d : I × J → R) :
  (comp I I J J R).symm (diagonal d) = diagonal fun i => diagonal fun j => d (i, j)

Full source

@[simp]
theorem comp_symm_diagonal [DecidableEq I] [DecidableEq J] [Zero R] (d : I × J → R) :
    (comp I I J J R).symm (diagonal d) = diagonal fun i => diagonal fun j => d (i, j) :=
  (comp I I J J R).symm_apply_eq.2 <| (comp_diagonal_diagonal fun i j => d (i, j)).symm

Inverse of Matrix Flattening Equivalence Preserves Diagonal Structure

Informal description

Let $I$ and $J$ be finite types with decidable equality, and let $R$ be a type with a zero element. For any function $d : I \times J \to R$, the inverse of the composition equivalence $\text{comp}$ maps the diagonal matrix with entries $d(i,j)$ to the diagonal matrix of diagonal matrices where the $(i,j)$-th entry is $d(i,j)$. In other words: $$(\text{comp}_{I,I,J,J}(R))^{-1} \left( \text{diagonal}\, d \right) = \text{diagonal} \left( \lambda i, \text{diagonal} (\lambda j, d(i,j)) \right)$$

Matrix.comp_transpose theorem

(M : Matrix I J (Matrix K L R)) : comp J I K L R Mᵀ = (comp _ _ _ _ R <| M.map (·ᵀ))ᵀ

Full source

theorem comp_transpose (M : Matrix I J (Matrix K L R)) :
  comp J I K L R Mᵀ = (comp _ _ _ _ R <| M.map (·ᵀ))ᵀ := rfl

Transpose Commutes with Matrix Flattening Equivalence

Informal description

For any matrix $M$ in $\text{Matrix}\, I\, J\, (\text{Matrix}\, K\, L\, R)$, the composition equivalence applied to the transpose of $M$ is equal to the transpose of the composition equivalence applied to the matrix obtained by transposing each entry of $M$. That is, \[ \text{comp}_{J,I,K,L,R}(M^\top) = \left(\text{comp}_{I,J,L,K,R} (M^\top_{\text{entrywise}})\right)^\top, \] where $M^\top_{\text{entrywise}}$ denotes the matrix obtained by transposing each $K \times L$ block of $M$.

Matrix.comp_map_transpose theorem

(M : Matrix I J (Matrix K L R)) : comp I J L K R (M.map (·ᵀ)) = (comp _ _ _ _ R Mᵀ)ᵀ

Full source

theorem comp_map_transpose (M : Matrix I J (Matrix K L R)) :
  comp I J L K R (M.map (·ᵀ)) = (comp _ _ _ _ R Mᵀ)ᵀ := rfl

Composition Equivalence Commutes with Blockwise Transpose

Informal description

For any matrix $M$ of type $\text{Matrix}\, I\, J\, (\text{Matrix}\, K\, L\, R)$, the composition equivalence $\text{comp}$ applied to the transpose of each block of $M$ is equal to the transpose of the composition equivalence applied to the transpose of $M$. In symbols: \[ \text{comp}_{I,J,L,K,R}(M^\top) = (\text{comp}_{J,I,K,L,R}(M^\top))^\top \] where $M^\top$ denotes the transpose of each block matrix in $M$.

Matrix.comp_symm_transpose theorem

(M : Matrix (I × K) (J × L) R) : (comp J I L K R).symm Mᵀ = (((comp I J K L R).symm M).map (·ᵀ))ᵀ

Full source

theorem comp_symm_transpose (M : Matrix (I × K) (J × L) R) :
  (comp J I L K R).symm Mᵀ = (((comp I J K L R).symm M).map (·ᵀ))ᵀ := rfl

Transpose Commutation with Matrix Flattening Inverse

Informal description

For any matrix $M$ of type $\text{Matrix}\, (I \times K)\, (J \times L)\, R$, the inverse of the flattening equivalence applied to the transpose of $M$ is equal to the transpose of the matrix obtained by first applying the inverse of the flattening equivalence to $M$ and then transposing each of its entries. In symbols: $$(\text{comp}\, J\, I\, L\, K\, R)^{-1}(M^\top) = \left(((\text{comp}\, I\, J\, K\, L\, R)^{-1} M).\text{map}(\cdot^\top)\right)^\top$$

Matrix.compAddEquiv definition

: Matrix I J (Matrix K L R) ≃+ Matrix (I × K) (J × L) R

Full source

/-- `Matrix.comp` as `AddEquiv` -/
def compAddEquiv : MatrixMatrix I J (Matrix K L R) ≃+ Matrix (I × K) (J × L) R where
  __ := Matrix.comp I J K L R
  map_add' _ _ := rfl

Additive equivalence for matrix flattening

Informal description

The additive equivalence `Matrix.compAddEquiv` maps an $I \times J$ matrix whose entries are $K \times L$ matrices over $R$ to an $(I \times K) \times (J \times L)$ matrix over $R$, preserving the additive structure. Specifically, given a matrix $M$ of type $\text{Matrix}\, I\, J\, (\text{Matrix}\, K\, L\, R)$, the corresponding matrix in $\text{Matrix}\, (I \times K)\, (J \times L)\, R$ is defined by $(i,k,j,l) \mapsto M_{i,j,k,l}$. The inverse operation reconstructs the original nested matrix structure.

Matrix.compAddEquiv_apply theorem

(M : Matrix I J (Matrix K L R)) : compAddEquiv I J K L R M = comp I J K L R M

Full source

@[simp]
theorem compAddEquiv_apply (M : Matrix I J (Matrix K L R)) :
    compAddEquiv I J K L R M = comp I J K L R M := rfl

Additive Equivalence of Matrix Flattening Matches Equivalence

Informal description

For any matrix $M$ of type $\text{Matrix}\, I\, J\, (\text{Matrix}\, K\, L\, R)$, the additive equivalence $\text{compAddEquiv}$ applied to $M$ equals the equivalence $\text{comp}$ applied to $M$, i.e., $$\text{compAddEquiv}\, I\, J\, K\, L\, R\, M = \text{comp}\, I\, J\, K\, L\, R\, M.$$

Matrix.compAddEquiv_symm_apply theorem

(M : Matrix (I × K) (J × L) R) : (compAddEquiv I J K L R).symm M = (comp I J K L R).symm M

Full source

@[simp]
theorem compAddEquiv_symm_apply (M : Matrix (I × K) (J × L) R) :
    (compAddEquiv I J K L R).symm M = (comp I J K L R).symm M := rfl

Inverse of Matrix Flattening Additive Equivalence Matches Inverse of Flattening Equivalence

Informal description

For any matrix $M$ of type $\text{Matrix}\, (I \times K)\, (J \times L)\, R$, the inverse of the additive equivalence $\text{compAddEquiv}$ maps $M$ to the same matrix as the inverse of the equivalence $\text{comp}$, i.e., $$(\text{compAddEquiv}\, I\, J\, K\, L\, R)^{-1}(M) = (\text{comp}\, I\, J\, K\, L\, R)^{-1}(M).$$

Matrix.compRingEquiv definition

: Matrix I I (Matrix J J R) ≃+* Matrix (I × J) (I × J) R

Full source

/-- `Matrix.comp` as `RingEquiv` -/
def compRingEquiv : MatrixMatrix I I (Matrix J J R) ≃+* Matrix (I × J) (I × J) R where
  __ := Matrix.compAddEquiv I I J J R
  map_mul' _ _ := by ext; exact (Matrix.sum_apply ..).trans <| .symm <| Fintype.sum_prod_type ..

Ring equivalence for matrix flattening

Informal description

The ring equivalence `Matrix.compRingEquiv` maps an $I \times I$ matrix whose entries are $J \times J$ matrices over $R$ to an $(I \times J) \times (I \times J)$ matrix over $R$, preserving both the additive and multiplicative structures. Specifically, given a matrix $M$ of type $\text{Matrix}\, I\, I\, (\text{Matrix}\, J\, J\, R)$, the corresponding matrix in $\text{Matrix}\, (I \times J)\, (I \times J)\, R$ is defined by $(i,k,j,l) \mapsto M_{i,j,k,l}$. The inverse operation reconstructs the original nested matrix structure.

Matrix.compRingEquiv_apply theorem

(M : Matrix I I (Matrix J J R)) : compRingEquiv I J R M = comp I I J J R M

Full source

@[simp]
theorem compRingEquiv_apply (M : Matrix I I (Matrix J J R)) :
    compRingEquiv I J R M = comp I I J J R M := rfl

Ring Equivalence of Matrix Flattening Preserves Matrix Structure

Informal description

For any $I \times I$ matrix $M$ whose entries are $J \times J$ matrices over a ring $R$, the ring equivalence $\text{compRingEquiv}$ maps $M$ to the same matrix as the flattening equivalence $\text{comp}$, i.e., $$\text{compRingEquiv}_{I,J,R}(M) = \text{comp}_{I,I,J,J,R}(M).$$

Matrix.compRingEquiv_symm_apply theorem

(M : Matrix (I × J) (I × J) R) : (compRingEquiv I J R).symm M = (comp I I J J R).symm M

Full source

@[simp]
theorem compRingEquiv_symm_apply (M : Matrix (I × J) (I × J) R) :
    (compRingEquiv I J R).symm M = (comp I I J J R).symm M := rfl

Inverse of Matrix Flattening Ring Equivalence Preserves Structure

Informal description

For any $(I \times J) \times (I \times J)$ matrix $M$ over a ring $R$, the inverse of the ring equivalence $\text{compRingEquiv}_{I,J,R}$ maps $M$ to the same matrix as the inverse of the flattening equivalence $\text{comp}_{I,I,J,J,R}$, i.e., $$(\text{compRingEquiv}_{I,J,R})^{-1}(M) = (\text{comp}_{I,I,J,J,R})^{-1}(M).$$

Matrix.compLinearEquiv definition

: Matrix I J (Matrix K L R) ≃ₗ[K] Matrix (I × K) (J × L) R

Full source

/-- `Matrix.comp` as `LinearEquiv` -/
@[simps!]
def compLinearEquiv : MatrixMatrix I J (Matrix K L R) ≃ₗ[K] Matrix (I × K) (J × L) R where
  __ := Matrix.compAddEquiv I J K L R
  map_smul' _ _ := rfl

Linear equivalence for matrix flattening

Informal description

The linear equivalence `Matrix.compLinearEquiv` maps an $I \times J$ matrix whose entries are $K \times L$ matrices over $R$ to an $(I \times K) \times (J \times L)$ matrix over $R$, preserving both the additive and scalar multiplication structures. Specifically, given a matrix $M$ of type $\text{Matrix}\, I\, J\, (\text{Matrix}\, K\, L\, R)$, the corresponding matrix in $\text{Matrix}\, (I \times K)\, (J \times L)\, R$ is defined by $(i,k,j,l) \mapsto M_{i,j,k,l}$. The inverse operation reconstructs the original nested matrix structure.

Matrix.compAlgEquiv definition

: Matrix I I (Matrix J J R) ≃ₐ[K] Matrix (I × J) (I × J) R

Full source

/-- `Matrix.comp` as `AlgEquiv` -/
def compAlgEquiv : MatrixMatrix I I (Matrix J J R) ≃ₐ[K] Matrix (I × J) (I × J) R where
  __ := Matrix.compRingEquiv I J R
  commutes' _ := comp_diagonal_diagonal _

Algebra equivalence for matrix flattening

Informal description

The algebra equivalence `Matrix.compAlgEquiv` maps an $I \times I$ matrix whose entries are $J \times J$ matrices over an algebra $R$ over a commutative semiring $K$ to an $(I \times J) \times (I \times J)$ matrix over $R$, preserving both the additive and multiplicative structures as well as the scalar multiplication by elements of $K$. Specifically, given a matrix $M$ of type $\text{Matrix}\, I\, I\, (\text{Matrix}\, J\, J\, R)$, the corresponding matrix in $\text{Matrix}\, (I \times J)\, (I \times J)\, R$ is defined by $(i,k,j,l) \mapsto M_{i,j,k,l}$. The inverse operation reconstructs the original nested matrix structure.

Matrix.compAlgEquiv_apply theorem

(M : Matrix I I (Matrix J J R)) : compAlgEquiv I J R K M = comp I I J J R M

Full source

@[simp]
theorem compAlgEquiv_apply (M : Matrix I I (Matrix J J R)) :
    compAlgEquiv I J R K M = comp I I J J R M := rfl

Matrix Flattening via Algebra Equivalence

Informal description

For any $I \times I$ matrix $M$ with entries in the space of $J \times J$ matrices over $R$, the algebra equivalence $\text{compAlgEquiv}_{I,J,R,K}(M)$ is equal to the flattened matrix $\text{comp}_{I,I,J,J,R}(M)$, which is an $(I \times J) \times (I \times J)$ matrix over $R$ defined by $(i,k,j,l) \mapsto M_{i,j,k,l}$.

Matrix.compAlgEquiv_symm_apply theorem

(M : Matrix (I × J) (I × J) R) : (compAlgEquiv I J R K).symm M = (comp I I J J R).symm M

Full source

@[simp]
theorem compAlgEquiv_symm_apply (M : Matrix (I × J) (I × J) R) :
    (compAlgEquiv I J R K).symm M = (comp I I J J R).symm M := rfl

Inverse of Matrix Flattening Algebra Equivalence

Informal description

For any $(I \times J) \times (I \times J)$ matrix $M$ over $R$, the inverse of the algebra equivalence `compAlgEquiv` applied to $M$ equals the inverse of the matrix flattening equivalence `comp` applied to $M$. That is, $(\text{compAlgEquiv}_{I,J,R,K})^{-1}(M) = (\text{comp}_{I,I,J,J,R})^{-1}(M)$.

Main results