Matrix algebra is an Azumaya algebra over R

In this file we prove that finite-dimensional matrix algebra Matrix n n R over R is an Azumaya algebra where R is a commutative ring.

Main Results

• IsAzumaya.Matrix: Finite-dimensional matrix algebra over R is Azumaya.

@[reducible, inline]

abbrev AlgHom.mulLeftRightMatrix_inv (R : Type u_1) (n : Type u_2) [CommSemiring R] [Fintype n] [DecidableEq n] : Module.End R (Matrix n n R) →ₗ[R] TensorProduct R (Matrix n n R) (Matrix n n R)ᵐᵒᵖ

AlgHom.mulLeftRight for matrix algebra sends basis Eᵢⱼ⊗Eₖₗ to the map f : Eₛₜ ↦ Eᵢⱼ * Eₛₜ * Eₖₗ = δⱼₛδₜₖEᵢₗ, therefore we construct the inverse by sending f to ∑ᵢₗₛₜ f(Eₛₜ)ᵢₗ • Eᵢₛ⊗Eₜₗ.

theorem AlgHom.mulLeftRightMatrix.inv_comp (R : Type u_1) (n : Type u_2) [CommSemiring R] [Fintype n] [DecidableEq n] : mulLeftRightMatrix_inv R n ∘ₗ (mulLeftRight R (Matrix n n R)).toLinearMap = LinearMap.id

theorem AlgHom.mulLeftRightMatrix.comp_inv (R : Type u_1) (n : Type u_2) [CommSemiring R] [Fintype n] [DecidableEq n] : (mulLeftRight R (Matrix n n R)).toLinearMap ∘ₗ mulLeftRightMatrix_inv R n = LinearMap.id

theorem IsAzumaya.matrix (R : Type u_1) (n : Type u_2) [CommSemiring R] [Fintype n] [DecidableEq n] [Nonempty n] : IsAzumaya R (Matrix n n R)

A nontrivial matrix ring over R is an Azumaya algebra over R.