morita equivalence

Stream: Is there code for X?

[Edison Xie]

currently is there morita equivalence defined in mathlib4? If not I'm going to define one in order to give a definition for azumaya algebra following the discussion about quaternion algebra.

[Edison Xie]

Btw should I define azumaya over commutative local ring like the how it's originally made or over just commrings?

[Junyan Xu]

Not sure what you're trying to say, but since the definitions work for any commutative rings, why restrict to local rings?
You might want to consult GTM 144, Noncommutative Algebra by Farb and Dennis, which has a chapter on Azumaya algebras. However it uses the 4th definition on Wikipedia and doesn't mention Morita equivalence.

[Edison Xie]

I thought it would be nice to both define and offer the four equivalence definitions

[Edison Xie]

thanks for the ref :))

[Jz Pan]

Another reference you may want to check is Jacobson's Basic Algebra.

[Edison Xie]

Jz Pan said:

Another reference you may want to check is Jacobson's Basic Algebra.

thanks! which chapter to be exact?

[Junyan Xu]

Apparently Section 3.12 and 3.15 of Basic Algebra II (2nd edition) is about Morita theory.