Azumaya Algebras

An Azumaya algebra over a commutative ring R is a finitely generated, projective and faithful R-algebra where the tensor product A ⊗[R] Aᵐᵒᵖ is isomorphic to the R-endomorphisms of A via the map f : a ⊗ b ↦ (x ↦ a * x * b.unop). TODO : Add the three more definitions and prove they are equivalent: · There exists an R-algebra B such that B ⊗[R] A is Morita equivalent to R; · Aᵐᵒᵖ ⊗[R] A is Morita equivalent to R; · The center of A is R and A is a separable algebra.

Reference

• [Benson Farb , R. Keith Dennis, Noncommutative Algebra][bensonfarb1993]

Tags

Azumaya algebra, central simple algebra, noncommutative algebra

@[reducible, inline]

noncomputable abbrev instModuleTensorProductMop (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : Module (TensorProduct R A Aᵐᵒᵖ) A

A as a A ⊗[R] Aᵐᵒᵖ-module (or equivalently, an A-A bimodule).

Equations

• instModuleTensorProductMop R A = TensorProduct.Algebra.module

noncomputable def AlgHom.mulLeftRight (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] : TensorProduct R A Aᵐᵒᵖ →ₐ[R] Module.End R A

The canonical map from A ⊗[R] Aᵐᵒᵖ to Module.End R A where a ⊗ b maps to f : x ↦ a * x * b.

Equations

• AlgHom.mulLeftRight R A = Algebra.lsmul R R A

@[simp]

theorem AlgHom.mulLeftRight_apply (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (b : Aᵐᵒᵖ) (x : A) : ((mulLeftRight R A) (a ⊗ₜ[R] b)) x = a * x * MulOpposite.unop b

class IsAzumaya (R : Type u_1) (A : Type u_2) [CommSemiring R] [Semiring A] [Algebra R A] extends Module.Projective R A, FaithfulSMul R A, Module.Finite R A : Prop

An Azumaya algebra is a finitely generated, projective and faithful R-algebra where AlgHom.mulLeftRight R A : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A is an isomorphism.

• out : ∃ (s : A →ₗ[R] A →₀ R), Function.LeftInverse ⇑(Finsupp.linearCombination R id) ⇑s
• eq_of_smul_eq_smul {m₁ m₂ : R} : (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
• fg_top : ⊤.FG
• bij : Function.Bijective ⇑(AlgHom.mulLeftRight R A)