# Composition of matrices #

This file shows that Mₙ(Mₘ(R)) ≃ Mₙₘ(R), Mₙ(Rᵒᵖ) ≃ₐ[K] Mₙ(R)ᵒᵖ and also different levels of equivalence when R is an AddCommMonoid, Semiring, and Algebra over a CommSemiring K.

## Main results #

- `Matrix.comp` is an equivalence between `Matrix I J (Matrix K L R)` and `I × K` by `J × L` matrices.
- `Matrix.swap` is an equivalence between `(I × J)` by `(K × L)` matrices and `J × I` by `L × K` matrices.

source
def Matrix.comp (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) :
Matrix I J (Matrix K L R) ≃ Matrix (I × K) (J × L) R

I by J matrix where each entry is a K by L matrix is equivalent to I × K by J × L matrix

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Matrix.comp_apply (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) (m : Matrix I J (Matrix K L R)) (ik : I × K) (jl : J × L) :
(comp I J K L R) m ik jl = m ik.1 jl.1 ik.2 jl.2
source
@[simp]
theorem Matrix.comp_symm_apply (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) (n : Matrix (I × K) (J × L) R) (i : I) (j : J) (k : K) (l : L) :
(comp I J K L R).symm n i j k l = n (i, k) (j, l)
source
theorem Matrix.comp_map_map {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (R' : Type u_6) (M : Matrix I J (Matrix K L R)) (f : R → R') :
(comp I J K L R') (M.map fun (M' : Matrix K L R) => M'.map f) = ((comp I J K L R) M).map f
source
@[simp]
theorem Matrix.comp_single_single {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (i : I) (j : J) (k : K) (l : L) (r : R) :
(comp I J K L R) (single i j (single k l r)) = single (i, k) (j, l) r
source
@[deprecated Matrix.comp_single_single (since := "2025-05-05")]
theorem Matrix.comp_stdBasisMatrix_stdBasisMatrix {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (i : I) (j : J) (k : K) (l : L) (r : R) :
(comp I J K L R) (single i j (single k l r)) = single (i, k) (j, l) r

Alias of `Matrix.comp_single_single`.

source
@[simp]
theorem Matrix.comp_symm_single {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (ii : I × K) (jj : J × L) (r : R) :
(comp I J K L R).symm (single ii jj r) = single ii.1 jj.1 (single ii.2 jj.2 r)
source
@[deprecated Matrix.comp_symm_single (since := "2025-05-05")]
theorem Matrix.comp_symm_stdBasisMatrix {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} [DecidableEq I] [DecidableEq J] [DecidableEq K] [DecidableEq L] [Zero R] (ii : I × K) (jj : J × L) (r : R) :
(comp I J K L R).symm (single ii jj r) = single ii.1 jj.1 (single ii.2 jj.2 r)

Alias of `Matrix.comp_symm_single`.

source
@[simp]
theorem Matrix.comp_diagonal_diagonal {I : Type u_1} {J : Type u_2} {R : Type u_5} [DecidableEq I] [DecidableEq J] [Zero R] (d : I → J → R) :
(comp I I J J R) (diagonal fun (i : I) => diagonal fun (j : J) => d i j) = diagonal fun (ij : I × J) => d ij.1 ij.2
source
@[simp]
theorem Matrix.comp_symm_diagonal {I : Type u_1} {J : Type u_2} {R : Type u_5} [DecidableEq I] [DecidableEq J] [Zero R] (d : I × J → R) :
(comp I I J J R).symm (diagonal d) = diagonal fun (i : I) => diagonal fun (j : J) => d (i, j)
source
theorem Matrix.comp_transpose {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix I J (Matrix K L R)) :
(comp J I K L R) M.transpose = ((comp I J L K R) (M.map fun (x : Matrix K L R) => x.transpose)).transpose
source
theorem Matrix.comp_map_transpose {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix I J (Matrix K L R)) :
(comp I J L K R) (M.map fun (x : Matrix K L R) => x.transpose) = ((comp J I K L R) M.transpose).transpose
source
theorem Matrix.comp_symm_transpose {I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix (I × K) (J × L) R) :
(comp J I L K R).symm M.transpose = (((comp I J K L R).symm M).map fun (x : Matrix K L R) => x.transpose).transpose
source
def Matrix.compAddEquiv (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) [AddCommMonoid R] :
Matrix I J (Matrix K L R) ≃+ Matrix (I × K) (J × L) R

`Matrix.comp` as `AddEquiv`

Equations

- Matrix.compAddEquiv I J K L R = { toEquiv := Matrix.comp I J K L R, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Matrix.compAddEquiv_apply (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) [AddCommMonoid R] (M : Matrix I J (Matrix K L R)) :
(compAddEquiv I J K L R) M = (comp I J K L R) M
source
@[simp]
theorem Matrix.compAddEquiv_symm_apply (I : Type u_1) (J : Type u_2) (K : Type u_3) (L : Type u_4) (R : Type u_5) [AddCommMonoid R] (M : Matrix (I × K) (J × L) R) :
(compAddEquiv I J K L R).symm M = (comp I J K L R).symm M
source
def Matrix.compRingEquiv (I : Type u_1) (J : Type u_2) (R : Type u_5) [Semiring R] [Fintype I] [Fintype J] :
Matrix I I (Matrix J J R) ≃+* Matrix (I × J) (I × J) R

`Matrix.comp` as `RingEquiv`

Equations

- Matrix.compRingEquiv I J R = { toEquiv := (Matrix.compAddEquiv I I J J R).toEquiv, map_mul' := ⋯, map_add' := ⋯ }

Instances For

source
@[simp]
theorem Matrix.compRingEquiv_apply (I : Type u_1) (J : Type u_2) (R : Type u_5) [Semiring R] [Fintype I] [Fintype J] (M : Matrix I I (Matrix J J R)) :
(compRingEquiv I J R) M = (comp I I J J R) M
source
@[simp]
theorem Matrix.compRingEquiv_symm_apply (I : Type u_1) (J : Type u_2) (R : Type u_5) [Semiring R] [Fintype I] [Fintype J] (M : Matrix (I × J) (I × J) R) :
(compRingEquiv I J R).symm M = (comp I I J J R).symm M
source
def Matrix.compLinearEquiv (I : Type u_1) (J : Type u_2) (L : Type u_4) (R : Type u_5) (K : Type u_7) [CommSemiring K] [AddCommMonoid R] [Module K R] :
Matrix I J (Matrix K L R) ≃ₗ[K] Matrix (I × K) (J × L) R

`Matrix.comp` as `LinearEquiv`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem Matrix.compLinearEquiv_apply (I : Type u_1) (J : Type u_2) (L : Type u_4) (R : Type u_5) (K : Type u_7) [CommSemiring K] [AddCommMonoid R] [Module K R] (a✝ : Matrix I J (Matrix K L R)) :
(compLinearEquiv I J L R K) a✝ = (comp I J K L R) a✝
source
@[simp]
theorem Matrix.compLinearEquiv_symm_apply (I : Type u_1) (J : Type u_2) (L : Type u_4) (R : Type u_5) (K : Type u_7) [CommSemiring K] [AddCommMonoid R] [Module K R] (a✝ : Matrix (I × K) (J × L) R) :
(compLinearEquiv I J L R K).symm a✝ = (comp I J K L R).symm a✝
source
def Matrix.compAlgEquiv (I : Type u_1) (J : Type u_2) (R : Type u_5) (K : Type u_7) [CommSemiring K] [Semiring R] [Fintype I] [Fintype J] [Algebra K R] [DecidableEq I] [DecidableEq J] :
Matrix I I (Matrix J J R) ≃ₐ[K] Matrix (I × J) (I × J) R

`Matrix.comp` as `AlgEquiv`

Equations

- Matrix.compAlgEquiv I J R K = { toEquiv := (Matrix.compRingEquiv I J R).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }

Instances For

source
@[simp]
theorem Matrix.compAlgEquiv_apply (I : Type u_1) (J : Type u_2) (R : Type u_5) (K : Type u_7) [CommSemiring K] [Semiring R] [Fintype I] [Fintype J] [Algebra K R] [DecidableEq I] [DecidableEq J] (M : Matrix I I (Matrix J J R)) :
(compAlgEquiv I J R K) M = (comp I I J J R) M
source
@[simp]
theorem Matrix.compAlgEquiv_symm_apply (I : Type u_1) (J : Type u_2) (R : Type u_5) (K : Type u_7) [CommSemiring K] [Semiring R] [Fintype I] [Fintype J] [Algebra K R] [DecidableEq I] [DecidableEq J] (M : Matrix (I × J) (I × J) R) :
(compAlgEquiv I J R K).symm M = (comp I I J J R).symm M
source
@[simp]
theorem Matrix.isUnit_comp_iff (I : Type u_1) (J : Type u_2) (R : Type u_5) [Semiring R] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {M : Matrix I I (Matrix J J R)} :
IsUnit ((comp I I J J R) M) ↔ IsUnit M
source
@[simp]
theorem Matrix.isUnit_comp_symm_iff (I : Type u_1) (J : Type u_2) (R : Type u_5) [Semiring R] [Fintype I] [Fintype J] [DecidableEq I] [DecidableEq J] {M : Matrix (I × J) (I × J) R} :
IsUnit ((comp I I J J R).symm M) ↔ IsUnit M