English
A nontrivial matrix ring M_n(R) is Azumaya over R; there exists a bijective mulLeftRight matrix-based isomorphism and a classical Azumaya structure.
Русский
Непротиворечивое матричное кольцо M_n(R) является Azumaya над R; существует биективный изоморфизм mulLeftRight и азумайя-структура.
LaTeX
$$$\text{IsAzumaya}_R(\mathrm{Matrix}_{n}(R))$$$
Lean4
/-- `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ₜₗ`. -/
abbrev mulLeftRightMatrix_inv : Module.End R (Matrix n n R) →ₗ[R] Matrix n n R ⊗[R] (Matrix n n R)ᵐᵒᵖ
where
toFun f := ∑ ⟨⟨i, j⟩, k, l⟩ : (n × n) × n × n, f (single j k 1) i l • (single i j 1) ⊗ₜ[R] op (single k l 1)
map_add' f1 f2 := by simp [add_smul, Finset.sum_add_distrib]
map_smul' r f := by simp [MulAction.mul_smul, Finset.smul_sum]
