We provide the R-algebra structure on matrix n n A when A is an R-algebra,
and show matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R).
@[instance]
def
matrix.algebra
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
{n : Type w}
[fintype n]
[decidable_eq n] :
Equations
- matrix.algebra = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := ((matrix.scalar n).comp (algebra_map R A)).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
theorem
algebra_map_matrix_apply
{R : Type u}
[comm_semiring R]
{A : Type v}
[semiring A]
[algebra R A]
{n : Type w}
[fintype n]
[decidable_eq n]
{r : R}
{i j : n} :
⇑(algebra_map R (matrix n n A)) r i j = ite (i = j) (⇑(algebra_map R A) r) 0
def
matrix_equiv_tensor.to_fun
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n] :
(Implementation detail).
The bare function underlying (A ⊗[R] matrix n n R) →ₐ[R] matrix n n A, on pure tensors.
Equations
- matrix_equiv_tensor.to_fun R A n a m = λ (i j : n), a * ⇑(algebra_map R A) (m i j)
def
matrix_equiv_tensor.to_fun_right_linear
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n] :
(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
- matrix_equiv_tensor.to_fun_right_linear R A n a = {to_fun := matrix_equiv_tensor.to_fun R A n a, map_add' := _, map_smul' := _}
def
matrix_equiv_tensor.to_fun_bilinear
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n] :
(Implementation detail).
The function underlying (A ⊗[R] matrix n n R) →ₐ[R] matrix n n A,
as an R-bilinear map.
Equations
- matrix_equiv_tensor.to_fun_bilinear R A n = {to_fun := matrix_equiv_tensor.to_fun_right_linear R A n _inst_4, map_add' := _, map_smul' := _}
def
matrix_equiv_tensor.to_fun_linear
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n] :
tensor_product 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
def
matrix_equiv_tensor.to_fun_alg_hom
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n] :
tensor_product 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.
@[simp]
theorem
matrix_equiv_tensor.to_fun_alg_hom_apply
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(a : A)
(m : matrix n n R) :
⇑(matrix_equiv_tensor.to_fun_alg_hom R A n) (a ⊗ₜ[R] m) = λ (i j : n), a * ⇑(algebra_map R A) (m i j)
def
matrix_equiv_tensor.inv_fun
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n] :
matrix n n A → tensor_product 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
- matrix_equiv_tensor.inv_fun R A n M = finset.univ.sum (λ (p : n × n), M p.fst p.snd ⊗ₜ[R] matrix.std_basis_matrix p.fst p.snd 1)
@[simp]
theorem
matrix_equiv_tensor.inv_fun_zero
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n] :
matrix_equiv_tensor.inv_fun R A n 0 = 0
@[simp]
theorem
matrix_equiv_tensor.inv_fun_add
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(M N : matrix n n A) :
matrix_equiv_tensor.inv_fun R A n (M + N) = matrix_equiv_tensor.inv_fun R A n M + matrix_equiv_tensor.inv_fun R A n N
@[simp]
theorem
matrix_equiv_tensor.inv_fun_smul
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(a : A)
(M : matrix n n A) :
matrix_equiv_tensor.inv_fun R A n (λ (i j : n), a * M i j) = (a ⊗ₜ[R] 1) * matrix_equiv_tensor.inv_fun R A n M
@[simp]
theorem
matrix_equiv_tensor.inv_fun_algebra_map
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(M : matrix n n R) :
matrix_equiv_tensor.inv_fun R A n (λ (i j : n), ⇑(algebra_map R A) (M i j)) = 1 ⊗ₜ[R] M
theorem
matrix_equiv_tensor.right_inv
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(M : matrix n n A) :
⇑(matrix_equiv_tensor.to_fun_alg_hom R A n) (matrix_equiv_tensor.inv_fun R A n M) = M
theorem
matrix_equiv_tensor.left_inv
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(M : tensor_product R A (matrix n n R)) :
matrix_equiv_tensor.inv_fun R A n (⇑(matrix_equiv_tensor.to_fun_alg_hom R A n) M) = M
def
matrix_equiv_tensor.equiv
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n] :
tensor_product 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
- matrix_equiv_tensor.equiv R A n = {to_fun := ⇑(matrix_equiv_tensor.to_fun_alg_hom R A n), inv_fun := matrix_equiv_tensor.inv_fun R A n (λ (a b : n), _inst_5 a b), left_inv := _, right_inv := _}
def
matrix_equiv_tensor
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n] :
matrix n n A ≃ₐ[R] tensor_product R A (matrix n n R)
The R-algebra isomorphism matrix n n A ≃ₐ[R] (A ⊗[R] matrix n n R).
Equations
- matrix_equiv_tensor R A n = {to_fun := (matrix_equiv_tensor.to_fun_alg_hom R A n).to_fun, inv_fun := (matrix_equiv_tensor.equiv R A n).inv_fun, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}.symm
@[simp]
theorem
matrix_equiv_tensor_apply
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(M : matrix n n A) :
⇑(matrix_equiv_tensor R A n) M = finset.univ.sum (λ (p : n × n), M p.fst p.snd ⊗ₜ[R] matrix.std_basis_matrix p.fst p.snd 1)
@[simp]
theorem
matrix_equiv_tensor_apply_std_basis
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(i j : n)
(x : A) :
⇑(matrix_equiv_tensor R A n) (matrix.std_basis_matrix i j x) = x ⊗ₜ[R] matrix.std_basis_matrix i j 1
@[simp]
theorem
matrix_equiv_tensor_apply_symm
(R : Type u)
[comm_semiring R]
(A : Type v)
[semiring A]
[algebra R A]
(n : Type w)
[fintype n]
[decidable_eq n]
(a : A)
(M : matrix n n R) :
⇑((matrix_equiv_tensor R A n).symm) (a ⊗ₜ[R] M) = λ (i j : n), a * ⇑(algebra_map R A) (M i j)