English
If A ≃_R B is an algebra isomorphism and A is Azumaya over R, then B is Azumaya over R.
Русский
Если A и B изоморфны как алгебры над R и A является Azumaya над R, то B тоже Azumaya над R.
LaTeX
$$$\text{IsAzumaya}(R, A) \Rightarrow \text{IsAzumaya}(R, B) \\text{whenever } A \cong_R B$$$
Lean4
theorem of_AlgEquiv (e : A ≃ₐ[R] B) [IsAzumaya R A] : IsAzumaya R B :=
let _ : Module.Projective R B := .of_equiv e.toLinearEquiv
let _ : FaithfulSMul R B := .of_injective e e.injective
let _ : Module.Finite R B := .equiv e.toLinearEquiv
⟨Function.Bijective.of_comp_iff (AlgHom.mulLeftRight R B) (Algebra.TensorProduct.congr e e.op).bijective |>.1 <|
by
rw [← AlgEquiv.coe_algHom, ← AlgHom.coe_comp, mulLeftRight_comp_congr]
simp [AlgHom.mulLeftRight_bij]⟩
