Alias for ModuleFunctor matching the textbook numbering of Definition 2.1.2 (the
notion of a module functor between left C-module categories) in EGNO.
Instances For
A morphism of module functors between two left C-module categories: a natural
transformation F.toFunctor ⟶ G.toFunctor whose components are compatible with the module
structure isomorphisms of F and G.
- compat (X : C) (A : M) : CategoryStruct.comp (self.natTrans.app (LeftModuleCategoryStruct.actObj X A)) (G.strIso X A).hom = CategoryStruct.comp (F.strIso X A).hom (LeftModuleCategoryStruct.actWhiskerLeft X (self.natTrans.app A))
Instances For
Two module functor homs are equal whenever their underlying natural transformations are equal.
The identity module functor hom on F, given by the identity natural transformation.
Instances For
Composition of module functor homs: the underlying natural transformations are composed and the compatibility square is verified.
Instances For
The category structure on ModuleFunctor C M N with module functor homs as morphisms,
identity and composition as defined by ModuleFunctorHom.id and ModuleFunctorHom.comp.
A module functor is exact if its underlying functor preserves both monomorphisms and epimorphisms.
Instances
In an exact module category, whiskering a monomorphism f by a projective object P
yields a split monomorphism, witnessed by an explicit retraction.
A morphism g in a module category is a monomorphism if whiskering by every projective
object of C (in particular the projective unit) yields a monomorphism.
A morphism g in a module category is an epimorphism if whiskering by every projective
object of C (in particular the projective unit) yields an epimorphism.
Alias of moduleAction_reflects_mono: the action of C reflects monomorphisms when
the unit is projective.
An epimorphism e : A ⟶ B with projective target B splits, i.e. admits a section
s : B ⟶ A with s ≫ e = 𝟙 B.
Alias of moduleAction_reflects_epi: the action of C reflects epimorphisms when
the unit is projective.
In an exact module category with biexact action, left whiskering by any object P : C
preserves epimorphisms.
Any module functor F whose source is an exact module category (with biexact action and
projective unit) is automatically exact, i.e. preserves monomorphisms and epimorphisms.
Baseline assumption for a finite multitensor category: the monoidal unit 𝟙_ C is
projective.
- unit_projective : Projective (MonoidalCategoryStruct.tensorUnit C)
Instances
Bundle of the standard exactness infrastructure on a module category M: abelianness,
right-exactness of the action, and biexactness of the action bifunctor.
- abelian : Abelian M
- actionRightExact : ExactModuleCategory.ActionRightExact C M
- biexact : ExactModuleCategory.BiexactAction C M
Instances
Proposition 2.7.8 (EGNO): Any module functor from an exact module category over a finite multitensor category to another module category is exact.
Post-composition leg of the biexactness of the composition bifunctor: post-composing a
module natural transformation η : F₁ ⟶ F₂ with an exact module functor G preserves both
monomorphism and epimorphism components.
Pre-composition leg of the biexactness of the composition bifunctor: pre-composing a
module natural transformation η : G₁ ⟶ G₂ with a module functor F : M₁ ⥤ M₂ transports
the mono/epi component conditions appropriately.
Every module functor between exact module categories admits a left adjoint at the level of underlying functors.
Every module functor between exact module categories admits a right adjoint at the level of underlying functors.
The right adjoint to a module functor between exact module categories preserves epimorphisms.
A module functor between exact module categories has both a left and a right adjoint, and the right adjoint preserves epimorphisms.
The underlying functor of a module functor between exact module categories is both a left and a right adjoint.
A module functor between exact module categories preserves projective objects, derived from the existence of an epi-preserving right adjoint.
Corollary 2.13.4 (EGNO): A module functor between exact module categories preserves projective objects.