Documentation

Mathlib.RingTheory.MatrixAlgebra

We show Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R).

noncomputable def MatrixEquivTensor.toFunBilinear (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) :
A →ₗ[R] Matrix n n R →ₗ[R] Matrix n n A

(Implementation detail). The function underlying (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an R-bilinear map.

Equations
Instances For
    @[simp]
    theorem MatrixEquivTensor.toFunBilinear_apply (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) (a : A) (m : Matrix n n R) :
    ((MatrixEquivTensor.toFunBilinear R A n) a) m = a m.map (algebraMap R A)
    noncomputable def MatrixEquivTensor.toFunLinear (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) :
    TensorProduct R A (Matrix n n R) →ₗ[R] Matrix n n A

    (Implementation detail). The function underlying (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an R-linear map.

    Equations
    Instances For
      noncomputable def MatrixEquivTensor.toFunAlgHom (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] :
      TensorProduct R A (Matrix n n R) →ₐ[R] Matrix n n A

      The function (A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A, as an algebra homomorphism.

      Equations
      Instances For
        @[simp]
        theorem MatrixEquivTensor.toFunAlgHom_apply (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] (a : A) (m : Matrix n n R) :
        (MatrixEquivTensor.toFunAlgHom R A n) (a ⊗ₜ[R] m) = a m.map (algebraMap R A)
        noncomputable def MatrixEquivTensor.invFun (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] (M : Matrix n n A) :
        TensorProduct R A (Matrix n n R)

        (Implementation detail.)

        The bare function Matrix n n A → A ⊗[R] Matrix n n R. (We don't need to show that it's an algebra map, thankfully --- just that it's an inverse.)

        Equations
        Instances For
          @[simp]
          theorem MatrixEquivTensor.invFun_zero (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] :
          @[simp]
          theorem MatrixEquivTensor.invFun_add (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] (M : Matrix n n A) (N : Matrix n n A) :
          @[simp]
          theorem MatrixEquivTensor.invFun_smul (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] (a : A) (M : Matrix n n A) :
          @[simp]
          theorem MatrixEquivTensor.invFun_algebraMap (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] (M : Matrix n n R) :
          MatrixEquivTensor.invFun R A n (M.map (algebraMap R A)) = 1 ⊗ₜ[R] M
          noncomputable def MatrixEquivTensor.equiv (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] :
          TensorProduct R A (Matrix n n R) Matrix n n A

          (Implementation detail)

          The equivalence, ignoring the algebra structure, (A ⊗[R] Matrix n n R) ≃ Matrix n n A.

          Equations
          Instances For
            noncomputable def matrixEquivTensor (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [Fintype n] [DecidableEq n] :
            Matrix n n A ≃ₐ[R] TensorProduct R A (Matrix n n R)

            The R-algebra isomorphism Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R).

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem matrixEquivTensor_apply (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [Fintype n] [DecidableEq n] (M : Matrix n n A) :
              (matrixEquivTensor R A n) M = p : n × n, M p.1 p.2 ⊗ₜ[R] Matrix.stdBasisMatrix p.1 p.2 1
              @[simp]
              theorem matrixEquivTensor_apply_std_basis (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [Fintype n] [DecidableEq n] (i : n) (j : n) (x : A) :
              @[simp]
              theorem matrixEquivTensor_apply_symm (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [Fintype n] [DecidableEq n] (a : A) (M : Matrix n n R) :
              (matrixEquivTensor R A n).symm (a ⊗ₜ[R] M) = M.map fun (x : R) => a * (algebraMap R A) x