Morita equivalence

Two R-algebras A and B are Morita equivalent if the categories of modules over A and B are R-linearly equivalent. In this file, we prove that Morita equivalence is an equivalence relation and that isomorphic algebras are Morita equivalent.

Main definitions

• MoritaEquivalence R A B: a structure containing an R-linear equivalence of categories between the module categories of A and B.
• IsMoritaEquivalent R A B: a predicate asserting that R-algebras A and B are Morita equivalent.

TODO

• For any ring R, R and Matₙ(R) are Morita equivalent.
• Morita equivalence in terms of projective generators.
• Morita equivalence in terms of full idempotents.
• Morita equivalence in terms of existence of an invertible bimodule.
• If R ≈ S, then R is simple iff S is simple.

References

• [Nathan Jacobson, Basic Algebra II][jacobson1989]

Tags

Morita Equivalence, Category Theory, Noncommutative Ring, Module Theory

structure MoritaEquivalence (R : Type u₀) [CommSemiring R] (A : Type u₁) [Ring A] [Algebra R A] (B : Type u₂) [Ring B] [Algebra R B] : Type (max (u₁ + 1) (u₂ + 1))

Let A and B be R-algebras. A Morita equivalence between A and B is an R-linear equivalence between the categories of A-modules and B-modules.

• eqv : ModuleCat A ≌ ModuleCat B

  The underlying equivalence of categories

• linear : CategoryTheory.Functor.Linear R self.eqv.functor

instance MoritaEquivalence.instAdditiveModuleCatFunctorEqv (R : Type u₀) [CommSemiring R] {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B] (e : MoritaEquivalence R A B) : e.eqv.functor.Additive

def MoritaEquivalence.refl (R : Type u₀) [CommSemiring R] (A : Type u₁) [Ring A] [Algebra R A] : MoritaEquivalence R A A

For any R-algebra A, A is Morita equivalent to itself.

Equations

• MoritaEquivalence.refl R A = { eqv := CategoryTheory.Equivalence.refl, linear := ⋯ }

def MoritaEquivalence.symm (R : Type u₀) [CommSemiring R] {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B] (e : MoritaEquivalence R A B) : MoritaEquivalence R B A

For any R-algebras A and B, if A is Morita equivalent to B, then B is Morita equivalent to A.

Equations

• MoritaEquivalence.symm R e = { eqv := e.eqv.symm, linear := ⋯ }

def MoritaEquivalence.trans (R : Type u₀) [CommSemiring R] {A B C : Type u₁} [Ring A] [Algebra R A] [Ring B] [Algebra R B] [Ring C] [Algebra R C] (e : MoritaEquivalence R A B) (e' : MoritaEquivalence R B C) : MoritaEquivalence R A C

For any R-algebras A, B, and C, if A is Morita equivalent to B and B is Morita equivalent to C, then A is Morita equivalent to C.

Equations

• MoritaEquivalence.trans R e e' = { eqv := e.eqv.trans e'.eqv, linear := ⋯ }

noncomputable def MoritaEquivalence.ofAlgEquiv {R : Type u₀} [CommSemiring R] {A : Type u₁} {B : Type u₂} [Ring A] [Algebra R A] [Ring B] [Algebra R B] (f : A ≃ₐ[R] B) : MoritaEquivalence R A B

Isomorphic R-algebras are Morita equivalent.

Equations

• MoritaEquivalence.ofAlgEquiv f = { eqv := ModuleCat.restrictScalarsEquivalenceOfRingEquiv f.symm.toRingEquiv, linear := ⋯ }

structure IsMoritaEquivalent (R : Type u₀) [CommSemiring R] (A : Type u₁) [Ring A] [Algebra R A] (B : Type u₂) [Ring B] [Algebra R B] : Prop

Let A and B be R-algebras. We say that A and B are Morita equivalent if the categories of A-modules and B-modules are equivalent as R-linear categories.

• cond : Nonempty (MoritaEquivalence R A B)

theorem IsMoritaEquivalent.refl (R : Type u₀) [CommSemiring R] (A : Type u₁) [Ring A] [Algebra R A] : IsMoritaEquivalent R A A

theorem IsMoritaEquivalent.symm (R : Type u₀) [CommSemiring R] {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B] (h : IsMoritaEquivalent R A B) : IsMoritaEquivalent R B A

theorem IsMoritaEquivalent.trans (R : Type u₀) [CommSemiring R] {A B C : Type u₁} [Ring A] [Ring B] [Ring C] [Algebra R A] [Algebra R B] [Algebra R C] (h : IsMoritaEquivalent R A B) (h' : IsMoritaEquivalent R B C) : IsMoritaEquivalent R A C

theorem IsMoritaEquivalent.of_algEquiv (R : Type u₀) [CommSemiring R] {A : Type u₁} [Ring A] [Algebra R A] {B : Type u₂} [Ring B] [Algebra R B] (f : A ≃ₐ[R] B) : IsMoritaEquivalent R A B