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
@[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) :
((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
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
@[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) :
(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
@[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] :
invFun R A n 0 = 0
@[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 N : Matrix n n A) :
invFun R A n (M + N) = invFun R A n M + invFun R A n N
@[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) :
invFun R A n (a M) = a ⊗ₜ[R] 1 * invFun R A n M
@[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) :
invFun R A n (M.map (algebraMap R A)) = 1 ⊗ₜ[R] M
theorem MatrixEquivTensor.right_inv (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) :
(toFunAlgHom R A n) (invFun R A n M) = M
theorem MatrixEquivTensor.left_inv (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [DecidableEq n] [Fintype n] (M : TensorProduct R A (Matrix n n R)) :
invFun R A n ((toFunAlgHom R A n) M) = 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
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.
@[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_stdBasisMatrix (R : Type u) [CommSemiring R] (A : Type v) [Semiring A] [Algebra R A] (n : Type w) [Fintype n] [DecidableEq n] (i j : n) (x : A) :
@[deprecated matrixEquivTensor_apply_stdBasisMatrix (since := "2024-08-11")]
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 j : n) (x : A) :

Alias of matrixEquivTensor_apply_stdBasisMatrix.

@[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