def
CategoryTheory.IsMoritaEquivalent
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(ModA : Type u₂)
[Category.{v₂, u₂} ModA]
[LeftModuleCategory' C ModA]
(ModB : Type u₃)
[Category.{v₃, u₃} ModB]
[LeftModuleCategory' C ModB]
:
Two left module categories ModA and ModB over C are Morita equivalent if there
exists an equivalence of module categories between them.
Instances For
noncomputable def
CategoryTheory.Proposition_2_9_10
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(A : C)
[MonObj A]
:
LeftModuleCategory' C (Mod_ C A)
EGNO Proposition 2.9.10: for any algebra A in C, the category Mod_ C A of
left A-modules in C is a left module category over C.
Instances For
@[implicit_reducible]
noncomputable instance
CategoryTheory.instLeftModuleCategory'_Mod_
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(A : C)
[MonObj A]
:
LeftModuleCategory' C (Mod_ C A)
The left C-module category structure on Mod_ C A coming from Proposition 2.9.10,
registered as an instance.
def
CategoryTheory.IsMoritaEquivalent_Algebras
(C : Type u₁)
[Category.{v₁, u₁} C]
[MonoidalCategory C]
(A B : C)
[MonObj A]
[MonObj B]
:
Two algebras A and B in C are Morita equivalent if their categories of left
modules in C are Morita equivalent as C-module categories.
Instances For
def
CategoryTheory.Definition_2_9_18
(C : Type u_1)
[Category.{u_2, u_1} C]
[MonoidalCategory C]
(A B : C)
[MonObj A]
[MonObj B]
:
EGNO Definition 2.9.18: Morita equivalence of algebras in a monoidal category.