ring_theory.matrix_algebra

source

def matrix_equiv_tensor.to_fun_bilinear (R : Type u) [comm_semiring 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

matrix_equiv_tensor.to_fun_bilinear R A n = (algebra.lsmul R (matrix n n A)).to_linear_map.compl₂ (algebra.linear_map R A).map_matrix

source

@[simp]

theorem matrix_equiv_tensor.to_fun_bilinear_apply (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] (n : Type w) (a : A) (m : matrix n n R) :

⇑(⇑(matrix_equiv_tensor.to_fun_bilinear R A n) a) m = a • m.map ⇑(algebra_map R A)

source

def matrix_equiv_tensor.to_fun_linear (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] (n : Type w) :

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

matrix_equiv_tensor.to_fun_linear R A n = tensor_product.lift (matrix_equiv_tensor.to_fun_bilinear R A n)

source

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) [decidable_eq n] [fintype 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.

Equations

matrix_equiv_tensor.to_fun_alg_hom R A n = algebra.tensor_product.alg_hom_of_linear_map_tensor_product (matrix_equiv_tensor.to_fun_linear R A n) _ _

source

@[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) [decidable_eq n] [fintype n] (a : A) (m : matrix n n R) :

⇑(matrix_equiv_tensor.to_fun_alg_hom R A n) (a ⊗ₜ[R] m) = a • m.map ⇑(algebra_map R A)

source

def matrix_equiv_tensor.inv_fun (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] (n : Type w) [decidable_eq n] [fintype n] (M : 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)

source

@[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) [decidable_eq n] [fintype n] :

matrix_equiv_tensor.inv_fun R A n 0 = 0

source

@[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) [decidable_eq n] [fintype 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

source

@[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) [decidable_eq n] [fintype n] (a : A) (M : matrix n n A) :

matrix_equiv_tensor.inv_fun R A n (a • M) = a ⊗ₜ[R] 1 * matrix_equiv_tensor.inv_fun R A n M

source

@[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) [decidable_eq n] [fintype n] (M : matrix n n R) :

matrix_equiv_tensor.inv_fun R A n (M.map ⇑(algebra_map R A)) = 1 ⊗ₜ[R] M

source

theorem matrix_equiv_tensor.right_inv (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] (n : Type w) [decidable_eq n] [fintype 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

source

theorem matrix_equiv_tensor.left_inv (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] (n : Type w) [decidable_eq n] [fintype 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

source

def matrix_equiv_tensor.equiv (R : Type u) [comm_semiring R] (A : Type v) [semiring A] [algebra R A] (n : Type w) [decidable_eq n] [fintype 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 _inst_5, left_inv := _, right_inv := _}

source

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

source

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

source

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

source

@[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) = M.map (λ (x : R), a * ⇑(algebra_map R A) x)