Basic properties of Azumaya algebras

In this file we prove basic facts about Azumaya algebras such as R is an Azumaya algebra over itself where R is a commutative ring.

Main Results

• IsAzumaya.id: R is an Azumaya algebra over itself.

• IsAzumaya.ofAlgEquiv: If A is an Azumaya algebra over R and A is isomorphic to B as an R-algebra, then B is an Azumaya algebra over R.

Tags

Noncommutative algebra, Azumaya algebra, Brauer Group

theorem IsAzumaya.AlgHom.mulLeftRight_bij (R : Type u_1) (A : Type u_2) [CommSemiring R] [Ring A] [Algebra R A] [h : IsAzumaya R A] : Function.Bijective ⇑(AlgHom.mulLeftRight R A)

@[reducible, inline]

abbrev IsAzumaya.tensorEquivEnd (R : Type u_1) [CommSemiring R] : TensorProduct R R Rᵐᵒᵖ ≃ₐ[R] Module.End R R

The "canonical" isomorphism between R ⊗ Rᵒᵖ and End R R which is equal to AlgHom.mulLeftRight R R.

theorem IsAzumaya.coe_tensorEquivEnd (R : Type u_1) [CommSemiring R] : ↑(tensorEquivEnd R) = AlgHom.mulLeftRight R R

instance IsAzumaya.id (R : Type u_1) [CommSemiring R] : IsAzumaya R R

theorem IsAzumaya.mulLeftRight_comp_congr (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) : (AlgHom.mulLeftRight R B).comp ↑(Algebra.TensorProduct.congr e (AlgEquiv.op e)) = (↑(LinearEquiv.algConj R e.toLinearEquiv)).comp (AlgHom.mulLeftRight R A)

The following diagram commutes:

          e ⊗ eᵒᵖ
A ⊗ Aᵐᵒᵖ  ------------> B ⊗ Bᵐᵒᵖ
  |                        |
  |                        |
  | mulLeftRight R A       | mulLeftRight R B
  |                        |
  V                        V
End R A   ------------> End R B
          e.conj

theorem IsAzumaya.of_AlgEquiv (R : Type u_1) (A : Type u_2) (B : Type u_3) [CommSemiring R] [Ring A] [Ring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) [IsAzumaya R A] : IsAzumaya R B