Documentation

Mathlib.Data.Matrix.Composition

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 #

@[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) :
(Matrix.comp I J K L R) m ik jl = m ik.1 jl.1 ik.2 jl.2
@[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) :
(Matrix.comp I J K L R).symm n i j k l = n (i, k) (j, l)
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
    @[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] :
    Matrix I J (Matrix K L R) ≃+ Matrix (I × K) (J × L) R

    Matrix.comp as AddEquiv

    Equations
    Instances For
      @[simp]
      theorem Matrix.compRingEquiv_symm_apply (I : Type u_1) (J : Type u_2) (R : Type u_5) [Semiring R] [Fintype I] [Fintype J] (n : Matrix (I × J) (I × J) R) (i : I) (j : I) (k : J) (l : J) :
      (Matrix.compRingEquiv I J R).symm n i j k l = n (i, k) (j, l)
      @[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)) (ik : I × J) (jl : I × J) :
      (Matrix.compRingEquiv I J R) m ik jl = m ik.1 jl.1 ik.2 jl.2
      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
      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] :
        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
          @[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] :
          Matrix I I (Matrix J J R) ≃ₐ[K] Matrix (I × J) (I × J) R

          Matrix.comp as AlgEquiv

          Equations
          Instances For