From 3ab599b4a76696ec3680f9ef91f75945900fa95e Mon Sep 17 00:00:00 2001 From: Whysoserioushah Date: Mon, 6 Jan 2025 11:25:40 +0800 Subject: [PATCH] docBlame --- Mathlib/Algebra/Azumaya/Defs.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Mathlib/Algebra/Azumaya/Defs.lean b/Mathlib/Algebra/Azumaya/Defs.lean index 658c2eead561a..f66d1593c8fc4 100644 --- a/Mathlib/Algebra/Azumaya/Defs.lean +++ b/Mathlib/Algebra/Azumaya/Defs.lean @@ -11,9 +11,8 @@ import Mathlib.RingTheory.Finiteness.Defs # 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 endomorphism ring of A `End R A` -via the map `f : a ⊗ b ↦ (x ↦ a * x * b.unop)`. +and faithful R-algebra where the tensor product `A ⊗[R] Aᵐᵒᵖ` is isomorphic to the +endomorphism ring of A `End R A` via the map `f : a ⊗ b ↦ (x ↦ a * x * b.unop)`. TODO : Add the rest three definitions and prove they are equivalent: · There exist an `R`-algebra `B` such that `B ⊗[R] A` is Morita equivalent to `R`, · `Aᵐᵒᵖ ⊗[R] A` is Morita equivalent to `R`, @@ -56,6 +55,8 @@ noncomputable abbrev TensorProduct.Algebra.moduleAux' : (A ⊗[R] Aᵐᵒᵖ) Algebra.TensorProduct.one_def] } +/-- An azumaya algebra is a finitely generated, projective and faithful R-algebra where + `TensorProduct.Algebra.moduleAux` is an isomorphism. -/ class IsAzumaya extends Module.Projective R A, FaithfulSMul R A : Prop where fg : Module.Finite R A bij : Function.Bijective <| TensorProduct.Algebra.moduleAux' R A