feat(Algebra/Azumaya/Defs): Define Azumaya algebras (#20489)

Co-authored-by: Whysoserioushah <[email protected]>
Co-authored-by: Jujian Zhang <[email protected]>

Mathlib.lean

@@ -35,6 +35,7 @@ import Mathlib.Algebra.Algebra.Tower
 import Mathlib.Algebra.Algebra.Unitization
 import Mathlib.Algebra.Algebra.ZMod
 import Mathlib.Algebra.AlgebraicCard
+import Mathlib.Algebra.Azumaya.Defs
 import Mathlib.Algebra.BigOperators.Associated
 import Mathlib.Algebra.BigOperators.Balance
 import Mathlib.Algebra.BigOperators.Expect

Mathlib/Algebra/Azumaya/Defs.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2025 Yunzhou Xie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yunzhou Xie, Jujian Zhang
+-/
+import Mathlib.Algebra.Module.Projective
+import Mathlib.RingTheory.Finiteness.Defs
+import Mathlib.RingTheory.TensorProduct.Basic
+
+/-!
+# 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
+-/
+
+variable (R A : Type*) [CommSemiring R] [Semiring A] [Algebra R A]
+
+open TensorProduct MulOpposite
+
+/-- `A` as a `A ⊗[R] Aᵐᵒᵖ`-module (or equivalently, an `A`-`A` bimodule). -/
+noncomputable abbrev instModuleTensorProductMop :
+  Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
+
+/-- The canonical map from `A ⊗[R] Aᵐᵒᵖ` to `Module.End R A` where
+  `a ⊗ b` maps to `f : x ↦ a * x * b`. -/
+noncomputable def AlgHom.mulLeftRight : (A ⊗[R] Aᵐᵒᵖ) →ₐ[R] Module.End R A :=
+  letI : Module (A ⊗[R] Aᵐᵒᵖ) A := TensorProduct.Algebra.module
+  letI : IsScalarTower R (A ⊗[R] Aᵐᵒᵖ) A := {
+    smul_assoc := fun r ab a ↦ by
+      change TensorProduct.Algebra.moduleAux _ _ = _ • TensorProduct.Algebra.moduleAux _ _
+      simp }
+  Algebra.lsmul R (A := A ⊗[R] Aᵐᵒᵖ) R A
+
+@[simp]
+lemma AlgHom.mulLeftRight_apply (a : A) (b : Aᵐᵒᵖ) (x : A) :
+    AlgHom.mulLeftRight R A (a ⊗ₜ b) x = a * x * b.unop := by
+  simp only [AlgHom.mulLeftRight, Algebra.lsmul_coe]
+  change TensorProduct.Algebra.moduleAux _ _ = _
+  simp [TensorProduct.Algebra.moduleAux, ← mul_assoc]
+
+/-- 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. -/
+class IsAzumaya extends Module.Projective R A, FaithfulSMul R A, Module.Finite R A : Prop where
+    bij : Function.Bijective <| AlgHom.mulLeftRight R A

docs/references.bib

@@ -276,6 +276,17 @@ @Book{            behrends1979
   zbl           = {0436.46013}
 }
 
+@Book{            bensonfarb1993,
+  author        = {Benson Farb, R. Keith Dennis},
+  series        = {Graduate Texts in Mathematics},
+  title         = {Noncommutative Algebra},
+  year          = {1993},
+  publisher     = {Springer},
+  language      = {English},
+  volume        = {144},
+  url           = {https://link.springer.com/book/10.1007/978-1-4612-0889-1}
+}
+
 @Article{         bergelson1985,
   author        = {Bergelson, Vitaly},
   title         = {Sets of Recurrence of Zm-Actions and Properties of Sets of