Documentation

Atlas.TensorCategories.code.FiberFunctor

source
@[reducible, inline]
abbrev TensorCategories.FiberFunctor_1_21 (k : Type u_1) [Field k] (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] :
Type (max (max u_2 u_3) (u_1 + 1))

Definition 1.21 (EGNO): A fiber functor on a category C is a (quasi-)tensor functor C ⥤ ModuleCat k that is exact and faithful.

Instances For
    source
    theorem TensorCategories.FiberFunctor.isFaithful_1_21 {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) :
    FF.F.Faithful

    A fiber functor is faithful on the underlying functor.

    source
    theorem TensorCategories.FiberFunctor.isLeftExact_1_21 {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) :
    FF.F.PreservesMonomorphisms

    A fiber functor preserves monomorphisms (left exactness).

    source
    theorem TensorCategories.FiberFunctor.isRightExact_1_21 {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) :
    FF.F.PreservesEpimorphisms

    A fiber functor preserves epimorphisms (right exactness).

    source
    @[reducible]
    def TensorCategories.FiberFunctor.isMonoidal_1_21 {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) :
    FF.F.Monoidal

    The underlying functor of a fiber functor carries a (lax) monoidal structure.

    Instances For
      source
      def TensorCategories.FiberFunctor.J_1_21 {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) (X Y : C) :
      CategoryTheory.MonoidalCategoryStruct.tensorObj (FF.F.obj X) (FF.F.obj Y) ≅ FF.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

      The tensor structure iso of a fiber functor: J_{X,Y} : F(X) ⊗ F(Y) ≅ F(X ⊗ Y).

      Instances For
        source
        def TensorCategories.FiberFunctor.unitIso_1_21 {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) :
        FF.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k)

        The unit isomorphism of a fiber functor: F(𝟙_ C) ≅ 𝟙_ (ModuleCat k).

        Instances For