structure CategoryTheory.InternalEndAlgebra {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Type (max u₁ v₁)

An algebra in C represented as a structure carrying both the underlying object and the MonObj instance providing its algebra structure.

• carrier : C
• monObj : MonObj self.carrier

noncomputable def CategoryTheory.InternalEndAlgebra.mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : InternalEndAlgebra) : MonoidalCategoryStruct.tensorObj A.carrier A.carrier ⟶ A.carrier

The multiplication morphism of the internal algebra.

noncomputable def CategoryTheory.InternalEndAlgebra.one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : InternalEndAlgebra) : MonoidalCategoryStruct.tensorUnit C ⟶ A.carrier

The unit morphism of the internal algebra.

def CategoryTheory.InternalEndAlgebra.ofMonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] : InternalEndAlgebra

Wrap an object A : C carrying a MonObj instance as an InternalEndAlgebra.

def CategoryTheory.InternalEndAlgebra.ofUnit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : InternalEndAlgebra

The trivial internal algebra given by the monoidal unit 𝟙_ C.

@[implicit_reducible]

instance CategoryTheory.instInhabitedInternalEndAlgebra {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] : Inhabited InternalEndAlgebra

The default internal algebra is the trivial one on 𝟙_ C.

class CategoryTheory.InternalHomData (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] : Type (max (max (max u₁ u₂) v₁) v₂)

The data needed to set up the internal-Hom functor to right modules over an internal algebra: a chosen generator gen ∈ M, the internal end algebra of gen, and a functor F from M to right modules over that algebra.

• gen : M
• endAlgebra : InternalEndAlgebra
• F : Functor M (RightMod_ (endAlgebra M).carrier)

class CategoryTheory.InternalHomBiexact (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] [HasModuleInternalHom C M] : Prop

The biexactness property of the internal Hom bifunctor on an exact module category: it preserves monos and epis on the right, and exchanges monos and epis on the left.

• right_preserves_mono (m₁ : M) {m₂ m₂' : M} (f : m₂ ⟶ m₂') : Mono f → Mono (moduleIHomMapRight m₁ f)
• right_preserves_epi (m₁ : M) {m₂ m₂' : M} (f : m₂ ⟶ m₂') : Epi f → Epi (moduleIHomMapRight m₁ f)
• left_sends_mono_to_epi {m₁ m₁' : M} (f : m₁ ⟶ m₁') (m₂ : M) : Mono f → Epi (moduleIHomMapLeft f m₂)
• left_sends_epi_to_mono {m₁ m₁' : M} (f : m₁ ⟶ m₁') (m₂ : M) : Epi f → Mono (moduleIHomMapLeft f m₂)

instance CategoryTheory.instInternalHomBiexact (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] [HasModuleInternalHom C M] : InternalHomBiexact C M

Internal Hom is biexact in any exact module category equipped with internal Homs.

class CategoryTheory.InternalHomExact (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] : Prop

Exactness of the internal-Hom functor F: it preserves epimorphisms.

• preservesEpi {N₁ N₂ : M} (f : N₁ ⟶ N₂) : Epi f → Epi (InternalHomData.F.map f)

class CategoryTheory.InternalHomGeneration (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] : Prop

The chosen generator gen generates the module category: every N ∈ M admits an epimorphism from X ⊗ gen for some X ∈ C.

• generation (N : M) : ∃ (X : C) (f : LeftModuleCategoryStruct.actObj X (InternalHomData.gen C) ⟶ N), Epi f

class CategoryTheory.InternalHomFaithful (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] : Prop

Faithfulness of the internal-Hom functor F : M ⥤ RightMod (endAlgebra).

• faithful : InternalHomData.F.Faithful

class CategoryTheory.InternalHomFull (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] : Prop

Fullness of the internal-Hom functor F : M ⥤ RightMod (endAlgebra).

• full : InternalHomData.F.Full

class CategoryTheory.InternalHomEssSurj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] : Prop

Essential surjectivity of the internal-Hom functor F : M ⥤ RightMod (endAlgebra).

• essSurj : InternalHomData.F.EssSurj

theorem CategoryTheory.internalHomConditionsImplyFaithful (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] [InternalHomExact C M] [InternalHomGeneration C M] : InternalHomFaithful C M

If the internal-Hom functor F is exact and the chosen generator generates M, then F is faithful.

theorem CategoryTheory.internalHomConditionsImplyFull (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] [InternalHomExact C M] [InternalHomGeneration C M] : InternalHomFull C M

If the internal-Hom functor F is exact and the chosen generator generates M, then F is full.

theorem CategoryTheory.internalHomConditionsImplyEssSurj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] [InternalHomExact C M] [InternalHomGeneration C M] : InternalHomEssSurj C M

If the internal-Hom functor F is exact and the chosen generator generates M, then F is essentially surjective.

noncomputable def CategoryTheory.internalHomEquivalence (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] [InternalHomExact C M] [InternalHomGeneration C M] : M ≌ RightMod_ (InternalHomData.endAlgebra M).carrier

Under exactness and generation, the internal-Hom functor F is an equivalence of categories between M and right modules over the internal end algebra of the generator.

noncomputable def CategoryTheory.internalHomEquivalence_of_steps (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] [hFaith : InternalHomFaithful C M] [hFull : InternalHomFull C M] [hEss : InternalHomEssSurj C M] : M ≌ RightMod_ (InternalHomData.endAlgebra M).carrier

Variant of internalHomEquivalence taking the faithful/full/ess.surj. properties as explicit hypotheses rather than deriving them from exactness and generation.

def CategoryTheory.internalHomEquivalence.algebra {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [LeftModuleCategory C M] [hom : InternalHomData C M] : InternalEndAlgebra

The internal end algebra produced by the InternalHomData package.

class CategoryTheory.ExactModCatInternalHom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] extends CategoryTheory.InternalHomData C M, CategoryTheory.InternalHomExact C M, CategoryTheory.InternalHomGeneration C M : Type (max (max (max u₁ u₂) v₁) v₂)

Combined class collecting all of the data and hypotheses needed to identify an exact module category M with right modules over an internal end algebra.

• gen : M
• endAlgebra : InternalEndAlgebra
• F : Functor M (RightMod_ (endAlgebra M).carrier)
• preservesEpi {N₁ N₂ : M} (f : N₁ ⟶ N₂) : Epi f → Epi (InternalHomData.F.map f)
• generation (N : M) : ∃ (X : C) (f : LeftModuleCategoryStruct.actObj X (InternalHomData.gen C) ⟶ N), Epi f

noncomputable def CategoryTheory.exact_module_cat_equiv (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] [h : ExactModCatInternalHom C M] : M ≌ RightMod_ (InternalHomData.endAlgebra M).carrier

Theorem (EGNO, Section 2.11): An exact module category equipped with an internal end algebra and the relevant exactness/generation conditions is equivalent to right modules over that algebra.

class CategoryTheory.IsIndecomposableModuleCategoryBasic (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [LeftModuleCategory C M] : Prop

A coarse "indecomposable module category" predicate: the category is nonempty and satisfies an opaque indecomposability marker (kept abstract here).

• nonempty : Nonempty M
• indecomposable : True

noncomputable def CategoryTheory.exact_module_cat_equiv_indecomposable (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] [IsIndecomposableModuleCategoryBasic C M] [h : ExactModCatInternalHom C M] : M ≌ RightMod_ (InternalHomData.endAlgebra M).carrier

Specialization of exact_module_cat_equiv to the indecomposable case.

class CategoryTheory.HasProjectiveGenerator (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] extends CategoryTheory.ExactModCatInternalHom C M : Type (max (max (max u₁ u₂) v₁) v₂)

An exact module category equipped with a projective generator (packaged via the ExactModCatInternalHom data and properties).

• gen : M
• endAlgebra : InternalEndAlgebra
• F : Functor M (RightMod_ (endAlgebra M).carrier)
• preservesEpi {N₁ N₂ : M} (f : N₁ ⟶ N₂) : Epi f → Epi (InternalHomData.F.map f)
• generation (N : M) : ∃ (X : C) (f : LeftModuleCategoryStruct.actObj X (InternalHomData.gen C) ⟶ N), Epi f

noncomputable def CategoryTheory.exact_module_cat_equiv_finite (k : Type u_1) [Field k] (C : Type u₁) [Category.{v₁, u₁} C] [FiniteTensorCategory k C] (M : Type u₂) [Category.{v₂, u₂} M] [ExactModuleCategory C M] [h : HasProjectiveGenerator C M] : M ≌ RightMod_ (InternalHomData.endAlgebra M).carrier

Specialization of exact_module_cat_equiv to exact module categories over a finite tensor category that admit a projective generator.

noncomputable def CategoryTheory.algebra_determines_module_cat {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] (A : C) [MonObj A] {M₁ : Type u₂} [Category.{v₂, u₂} M₁] {M₂ : Type u₂} [Category.{v₂, u₂} M₂] (e₁ : M₁ ≌ RightMod_ A) (e₂ : M₂ ≌ RightMod_ A) : M₁ ≌ M₂

Two module categories that are each equivalent to right modules over the same internal algebra A are equivalent to each other.