noncomputable def
moduleFunctorCategoryIsAbelian
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M₁ : Type u₂)
[CategoryTheory.Category.{v₂, u₂} M₁]
[CategoryTheory.LeftModuleCategory C M₁]
(M₂ : Type u₃)
[CategoryTheory.Category.{v₃, u₃} M₂]
[CategoryTheory.LeftModuleCategory C M₂]
:
The category of module functors between two left C-module categories carries a
canonical abelian structure.
Instances For
noncomputable def
moduleFunctorCategoryIsLinear
(k : Type w)
[Field k]
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.MonoidalCategory C]
(M₁ : Type u₂)
[CategoryTheory.Category.{v₂, u₂} M₁]
[CategoryTheory.LeftModuleCategory C M₁]
(M₂ : Type u₃)
[CategoryTheory.Category.{v₃, u₃} M₂]
[CategoryTheory.LeftModuleCategory C M₂]
:
CategoryTheory.Linear k (CategoryTheory.ModuleFunctor C M₁ M₂)
The category of module functors between two left C-module categories carries a
canonical k-linear structure compatible with the abelian structure.
Instances For
theorem
moduleFunctorCategory_isFinite
(k : Type w)
[Field k]
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.FiniteTensorCategory k C]
(M₁ : Type u₂)
[CategoryTheory.Category.{v₂, u₂} M₁]
[CategoryTheory.ExactModuleCategory C M₁]
(M₂ : Type u₃)
[CategoryTheory.Category.{v₃, u₃} M₂]
[CategoryTheory.ExactModuleCategory C M₂]
:
For a finite tensor category C and exact left C-module categories M₁, M₂, the
category of module functors between them is a finite abelian category.
theorem
proposition_2_13_5
(k : Type w)
[Field k]
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.FiniteTensorCategory k C]
(M₁ : Type u₂)
[CategoryTheory.Category.{v₂, u₂} M₁]
[CategoryTheory.ExactModuleCategory C M₁]
(M₂ : Type u₃)
[CategoryTheory.Category.{v₃, u₃} M₂]
[CategoryTheory.ExactModuleCategory C M₂]
:
Proposition 2.13.5 (EGNO): The category of module functors between two exact module categories over a finite tensor category is itself a finite abelian category.