LeanPool.BrauerGroupNew.MatrixEquivTensor #

Imported Lean Pool material for LeanPool.BrauerGroupNew.MatrixEquivTensor.

def toTensorMartrixToFunBilinear (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] :

K →ₗ[F] Matrix n n A →ₗ[F] Matrix n n (TensorProduct F K A)

Bilinear map sending a scalar and a matrix to the matrix obtained by tensoring entries.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem toTensorMartrixToFunBilinear_apply (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (k : K) (M : Matrix n n A) :

((toTensorMartrixToFunBilinear K F A n) k) M = k • Algebra.TensorProduct.includeRight.mapMatrix M

source

@[reducible, inline]

abbrev toTensorMatrixToFunFlinear (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] :

TensorProduct F K (Matrix n n A) →ₗ[F] Matrix n n (TensorProduct F K A)

The F-linear map induced from toTensorMartrixToFunBilinear.

Equations

toTensorMatrixToFunFlinear K F A n = TensorProduct.lift (toTensorMartrixToFunBilinear K F A n)

Instances For

source

@[reducible, inline]

abbrev toTensorMatrixToFunKlinear (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] :

TensorProduct F K (Matrix n n A) →ₗ[K] Matrix n n (TensorProduct F K A)

The K-linear map from a tensor of matrices to matrices over a tensor product.

Equations

toTensorMatrixToFunKlinear K F A n = { toAddHom := (toTensorMatrixToFunFlinear K F A n).toAddHom, map_smul' := ⋯ }

Instances For

source

@[reducible, inline]

abbrev toTensorMatrix (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] :

TensorProduct F K (Matrix n n A) →ₐ[K] Matrix n n (TensorProduct F K A)

Algebra homomorphism from a tensor of matrices to matrices over the tensor product.

Equations

toTensorMatrix K F A n = AlgHom.ofLinearMap (toTensorMatrixToFunKlinear K F A n) ⋯ ⋯

Instances For

source

def invFunToFunBilinear (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] (i j : n) :

K →ₗ[F] A →ₗ[F] TensorProduct F K (Matrix n n A)

Bilinear map placing a tensor entry into the (i,j) matrix coefficient.

Equations

invFunToFunBilinear K F A n i j = { toFun := fun (k : K) => { toFun := fun (a : A) => k ⊗ₜ[F] Matrix.single i j a, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

@[simp]

theorem invFunToFunBilinear_apply (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] (i j : n) (k : K) (a : A) :

((invFunToFunBilinear K F A n i j) k) a = k ⊗ₜ[F] Matrix.single i j a

source

@[reducible, inline]

abbrev invFunToFun (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] (i j : n) :

TensorProduct F K A →ₗ[F] TensorProduct F K (Matrix n n A)

The F-linear map induced by invFunToFunBilinear.

Equations

invFunToFun K F A n i j = TensorProduct.lift (invFunToFunBilinear K F A n i j)

Instances For

source

@[reducible, inline]

abbrev invFunKlinear (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] (i j : n) :

TensorProduct F K A →ₗ[K] TensorProduct F K (Matrix n n A)

The K-linear map placing a tensor entry into the (i,j) matrix coefficient.

Equations

invFunKlinear K F A n i j = { toAddHom := (invFunToFun K F A n i j).toAddHom, map_smul' := ⋯ }

Instances For

source

@[reducible, inline]

abbrev invFunLinearMap (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] :

Matrix n n (TensorProduct F K A) →ₗ[K] TensorProduct F K (Matrix n n A)

Linear inverse map from matrices over the tensor product to a tensor of matrices.

Equations

invFunLinearMap K F A n = { toFun := fun (M : Matrix n n (TensorProduct F K A)) => ∑ p : n × n, (invFunKlinear K F A n p.1 p.2) (M p.1 p.2), map_add' := ⋯, map_smul' := ⋯ }

Instances For

source

theorem matrixTensor_left_inv (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (M : TensorProduct F K (Matrix n n A)) :

(invFunLinearMap K F A n) ((toTensorMatrix K F A n) M) = M

source

theorem matrixTensor_right_inv (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (M : Matrix n n (TensorProduct F K A)) :

(toTensorMatrix K F A n) ((invFunLinearMap K F A n) M) = M

source

def equivTensor' (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] :

TensorProduct F K (Matrix n n A) ≃ Matrix n n (TensorProduct F K A)

Equivalence underlying the tensor-matrix algebra equivalence.

Equations

equivTensor' K F A n = { toFun := ⇑(toTensorMatrix K F A n), invFun := ⇑(invFunLinearMap K F A n), left_inv := ⋯, right_inv := ⋯ }

Instances For

source

def matrixTensorEquivTensor (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] :

TensorProduct F K (Matrix n n A) ≃ₐ[K] Matrix n n (TensorProduct F K A)

Algebra equivalence between tensoring a matrix algebra and matrices over a tensor product.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem matrixTensorEquivTensor_apply (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (M : TensorProduct F K (Matrix n n A)) :

(matrixTensorEquivTensor K F A n) M = (toTensorMatrix K F A n) M

source

@[simp]

theorem matrixTensorEquivTensor_symm_apply (K : Type u_1) (F : Type u_2) [CommSemiring K] [CommSemiring F] [Algebra F K] (A : Type u_3) (n : Type u_4) [Ring A] [Algebra F A] [DecidableEq n] [Fintype n] (M : Matrix n n (TensorProduct F K A)) :

(matrixTensorEquivTensor K F A n).symm M = (invFunLinearMap K F A n) M