# mathlibdocumentation

ring_theory.matrix_algebra

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

def matrix_equiv_tensor.to_fun (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) (a : A) (m : n R) :
n A

(Implementation detail). The bare function underlying (A ⊗[R] matrix n n R) →ₐ[R] matrix n n A, on pure tensors.

Equations
• a m = λ (i j : n), a * A) (m i j)
def matrix_equiv_tensor.to_fun_right_linear (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) (a : A) :
n R →ₗ[R] n A

(Implementation detail). The function underlying (A ⊗[R] matrix n n R) →ₐ[R] matrix n n A, as an R-linear map in the second tensor factor.

Equations
def matrix_equiv_tensor.to_fun_bilinear (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) :
A →ₗ[R] n R →ₗ[R] n A

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

Equations
def matrix_equiv_tensor.to_fun_linear (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) :
(matrix n n R) →ₗ[R] n A

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

Equations
def matrix_equiv_tensor.to_fun_alg_hom (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] :
(matrix n n R) →ₐ[R] n A

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

Equations
@[simp]
theorem matrix_equiv_tensor.to_fun_alg_hom_apply (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] (a : A) (m : n R) :
(a ⊗ₜ[R] m) = λ (i j : n), a * A) (m i j)
def matrix_equiv_tensor.inv_fun (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] (M : n 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 matrix_equiv_tensor.inv_fun_zero (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] :
0 = 0
@[simp]
theorem matrix_equiv_tensor.inv_fun_add (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] (M N : n A) :
(M + N) = M + N
@[simp]
theorem matrix_equiv_tensor.inv_fun_smul (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] (a : A) (M : n A) :
(λ (i j : n), a * M i j) = a ⊗ₜ[R] 1 * M
@[simp]
theorem matrix_equiv_tensor.inv_fun_algebra_map (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] (M : n R) :
(λ (i j : n), A) (M i j)) = 1 ⊗ₜ[R] M
theorem matrix_equiv_tensor.right_inv (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] (M : n A) :
M) = M
theorem matrix_equiv_tensor.left_inv (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] (M : (matrix n n R)) :
( M) = M
def matrix_equiv_tensor.equiv (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [decidable_eq n] [fintype n] :
(matrix n n R) n A

(Implementation detail)

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

Equations
def matrix_equiv_tensor (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [fintype n] [decidable_eq n] :
n A ≃ₐ[R] (matrix n n R)

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

Equations
@[simp]
theorem matrix_equiv_tensor_apply (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [fintype n] [decidable_eq n] (M : n A) :
n) M = finset.univ.sum (λ (p : n × n), M p.fst p.snd ⊗ₜ[R] 1)
@[simp]
theorem matrix_equiv_tensor_apply_std_basis (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [fintype n] [decidable_eq n] (i j : n) (x : A) :
n) x) = x ⊗ₜ[R]
@[simp]
theorem matrix_equiv_tensor_apply_symm (R : Type u) (A : Type v) [semiring A] [ A] (n : Type w) [fintype n] [decidable_eq n] (a : A) (M : n R) :
A n).symm) (a ⊗ₜ[R] M) = λ (i j : n), a * A) (M i j)