@[reducible, inline]

abbrev CategoryTheory.AlgebraObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) : Type v

Convenient abbreviation: an algebra structure on an object A : C is a MonObj A.

@[reducible, inline]

abbrev CategoryTheory.LeftModObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] (M : C) : Type v

Convenient abbreviation: a left module structure on M : C over the algebra A is a ModObj A M.

@[reducible, inline]

abbrev CategoryTheory.Definition_2_9_18_MoritaEquivalent {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : C) [MonObj A] [MonObj B] : Prop

Two algebras A and B in C are Morita equivalent if the module categories Mod_C(A) and Mod_C(B) are module equivalent.

def CategoryTheory.IsExactAlgebra {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] [LeftModuleCategory C (RightMod_ A)] : Prop

An algebra A in C is exact when the category RightMod_ A of right A-modules, viewed as a left C-module category, is an exact module category.

@[reducible, inline]

abbrev CategoryTheory.Definition_2_9_21_ExactAlgebra {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A : C) [MonObj A] [LeftModuleCategory C (RightMod_ A)] : Prop

An algebra A in the category C is called exact if the module category Mod_C(A) is exact.

def CategoryTheory.proposition_2_9_10 {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] : LeftModuleCategory C (RightMod_ A)

The category Mod_C(A) of right A-modules, equipped with the natural tensor action of C, the standard associativity, and unit constraints, is a left C-module category.

noncomputable def CategoryTheory.Definition_2_9_22_TensorOverAlgebra {C : Type u} [Category.{v, u} C] [MonoidalCategory C] [Limits.HasCoequalizers C] {A M N : C} (actR : MonoidalCategoryStruct.tensorObj M A ⟶ M) (actL : MonoidalCategoryStruct.tensorObj A N ⟶ N) : C

Tensor product over an algebra A: for a right A-module (M, actR) and a left A-module (N, actL), the object M ⊗_A N is the quotient of M ⊗ N by the image of actR ⊗ id - id ⊗ actL : M ⊗ A ⊗ N → M ⊗ N.

@[reducible, inline]

abbrev CategoryTheory.BimoduleObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : Mon C) : Type (max u v)

Abbreviation for an A-B-bimodule object in C, identified with Mathlib's Bimod A B.

@[reducible, inline]

abbrev CategoryTheory.Definition_2_9_24_Bimodule {C : Type u} [Category.{v, u} C] [MonoidalCategory C] (A B : Mon C) : Type (max u v)

An A-B-bimodule in a monoidal category C is a triple (M, p, q) where M ∈ C, p : A ⊗ M → M makes M a left A-module, q : M ⊗ B → M makes M a right B-module, and the two actions commute.

def CategoryTheory.freeRightModuleObj {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (X : C) : RightModObj A (MonoidalCategoryStruct.tensorObj X A)

Right A-module structure on X ⊗ A obtained by tensoring on the left by X with the right regular A-module.

def CategoryTheory.FreeRightModule {C : Type u} [Category.{v, u} C] [MonoidalCategory C] {A : C} [MonObj A] (X : C) : RightMod_ A

The free right A-module on an object X : C, namely X ⊗ A with the action coming from multiplication on the right factor.

def CategoryTheory.moduleIHomId {C₀ : Type u_1} [Category.{u_3, u_1} C₀] [MonoidalCategory C₀] {M₀ : Type u_2} [Category.{u_4, u_2} M₀] [LeftModuleCategory C₀ M₀] [HasModuleInternalHom C₀ M₀] (m : M₀) : MonoidalCategoryStruct.tensorUnit C₀ ⟶ moduleIHom m m

The identity morphism 𝟙_ C₀ → Hom̲(m, m), obtained from the left unitor actℓ_ m via the defining adjunction of the internal Hom.

@[implicit_reducible]

noncomputable instance CategoryTheory.internalEndMonObj {C₀ : Type u_1} [Category.{u_3, u_1} C₀] [MonoidalCategory C₀] {M₀ : Type u_2} [Category.{u_4, u_2} M₀] [LeftModuleCategory C₀ M₀] [HasModuleInternalHom C₀ M₀] (m : M₀) : MonObj (moduleIHom m m)

The internal endomorphism object Hom̲(m, m) of an object m in a module category M₀ over C₀ carries a canonical algebra (monoid object) structure, with multiplication given by composition and unit by moduleIHomId.