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 betweenMatrix I J (Matrix K L R)
andI × K
byJ × L
matrices.Matrix.swap
is an equivalence between(I × J)
by(K × L)
matrices andJ × I
byL × K
matrices.
@[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))
(ik : I × K)
(jl : J × L)
:
(Matrix.compAddEquiv I J K L R) m ik jl = m ik.1 jl.1 ik.2 jl.2
@[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]
(n : Matrix (I × K) (J × L) R)
(i : I)
(j : J)
(k : K)
(l : L)
:
(Matrix.compAddEquiv I J K L R).symm n i j k l = n (i, k) (j, l)
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]
:
Equations
- Matrix.compAddEquiv I J K L R = { toEquiv := Matrix.comp I J K L R, map_add' := ⋯ }
Instances For
def
Matrix.compRingEquiv
(I : Type u_1)
(J : Type u_2)
(R : Type u_5)
[Semiring R]
[Fintype I]
[Fintype J]
:
Equations
- Matrix.compRingEquiv I J R = { toEquiv := (Matrix.compAddEquiv I I J J R).toEquiv, map_mul' := ⋯, map_add' := ⋯ }
Instances For
@[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_6)
[CommSemiring K]
[AddCommMonoid R]
[Module K R]
:
∀ (a : Matrix (I × K) (J × L) R), (Matrix.compLinearEquiv I J L R K).symm a = (Matrix.compAddEquiv I J K L R).symm a
@[simp]
theorem
Matrix.compLinearEquiv_apply
(I : Type u_1)
(J : Type u_2)
(L : Type u_4)
(R : Type u_5)
(K : Type u_6)
[CommSemiring K]
[AddCommMonoid R]
[Module K R]
:
∀ (a : Matrix I J (Matrix K L R)), (Matrix.compLinearEquiv I J L R K) a = (Matrix.compAddEquiv I J K L R) a
def
Matrix.compLinearEquiv
(I : Type u_1)
(J : Type u_2)
(L : Type u_4)
(R : Type u_5)
(K : Type u_6)
[CommSemiring K]
[AddCommMonoid R]
[Module K R]
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Matrix.compAlgEquiv_symm_apply
(I : Type u_1)
(J : Type u_2)
(R : Type u_5)
(K : Type u_6)
[CommSemiring K]
[Semiring R]
[Fintype I]
[Fintype J]
[Algebra K R]
[DecidableEq I]
[DecidableEq J]
(n : Matrix (I × J) (I × J) R)
(i : I)
(j : I)
(k : J)
(l : J)
:
(Matrix.compAlgEquiv I J R K).symm n i j k l = n (i, k) (j, l)
@[simp]
theorem
Matrix.compAlgEquiv_apply
(I : Type u_1)
(J : Type u_2)
(R : Type u_5)
(K : Type u_6)
[CommSemiring K]
[Semiring R]
[Fintype I]
[Fintype J]
[Algebra K R]
[DecidableEq I]
[DecidableEq J]
(m : Matrix I I (Matrix J J R))
(ik : I × J)
(jl : I × J)
:
(Matrix.compAlgEquiv I J R K) m ik jl = m ik.1 jl.1 ik.2 jl.2
def
Matrix.compAlgEquiv
(I : Type u_1)
(J : Type u_2)
(R : Type u_5)
(K : Type u_6)
[CommSemiring K]
[Semiring R]
[Fintype I]
[Fintype J]
[Algebra K R]
[DecidableEq I]
[DecidableEq J]
:
Equations
- Matrix.compAlgEquiv I J R K = { toEquiv := (Matrix.compRingEquiv I J R).toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }