English
A nontrivial matrix ring over R is Azumaya; the Azumaya structure is established via explicit inverses and isomorphisms between tensor and End structures.
Русский
Непрерывное матричное кольцо над R является Azumaya; структура Azumaya устанавливается через явные обратные и изоморфизмы между тензорным и End-структурами.
LaTeX
$$$\text{IsAzumaya}_R(\mathrm{Matrix}_{n}(R))$ with explicit bijections as above$$
Lean4
/-- A nontrivial matrix ring over `R` is an Azumaya algebra over `R`. -/
theorem matrix [Nonempty n] : IsAzumaya R (Matrix n n R)
where
eq_of_smul_eq_smul := by nontriviality R; exact eq_of_smul_eq_smul
bij :=
Function.bijective_iff_has_inverse.mpr
⟨AlgHom.mulLeftRightMatrix_inv R n, DFunLike.congr_fun (AlgHom.mulLeftRightMatrix.inv_comp R n),
DFunLike.congr_fun (AlgHom.mulLeftRightMatrix.comp_inv R n)⟩
