Constructive Remarks on Azumaya Algebra


Preprint, (2023). On arXiv ArXiv 2306.17679 .
with Thierry Coquand and Stefan Neuwirth. (2023).

Abstract
The notion of central simple algebra over a field has been generalised to the notion of Azumaya algebra over an arbitrary commutative ring R. The definition is the following characterisation: an algebra A which is projective of finite type over R and such that the canonical map A ⊗F A op to End R(A) is an isomorphism. One main goal of this note is to show in a constructive setting that this definition is equivalent to a suitable generalisation of another characterisation: an algebra A which becomes a matrix algebra by an algebraic (resp. separable) extension of F.