structure TensorCategories.QuasiTensorFunctor (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u₁) [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u u₁) v) v₁)

Definition 1.14.1 (Etingof–Gelaki–Nikshych–Ostrik): A quasi-tensor functor between abelian monoidal categories C and D over a field k. It consists of an exact (mono- and epi-preserving) faithful functor F equipped with natural isomorphisms J X Y : F X ⊗ F Y ≅ F (X ⊗ Y) and a unit isomorphism F (𝟙_ C) ≅ 𝟙_ D.

• F : CategoryTheory.Functor C D
• faithful : self.F.Faithful
• preservesMono : self.F.PreservesMonomorphisms
• preservesEpi : self.F.PreservesEpimorphisms
• J (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (self.F.obj X) (self.F.obj Y) ≅ self.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
• J_natural_left {X X' : C} (f : X ⟶ X') (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.F.map f) (self.F.obj Y)) (self.J X' Y).hom = CategoryTheory.CategoryStruct.comp (self.J X Y).hom (self.F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
• J_natural_right (X : C) {Y Y' : C} (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.F.obj X) (self.F.map g)) (self.J X Y').hom = CategoryTheory.CategoryStruct.comp (self.J X Y).hom (self.F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
• unitIso : self.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

structure TensorCategories.TensorFunctor (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u₁) [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u u₁) v) v₁)

Definition 1.14.1 (Etingof–Gelaki–Nikshych–Ostrik): A tensor functor between abelian monoidal categories C and D over a field k is an exact faithful functor F equipped with a monoidal structure (coherent associativity and unit isomorphisms).

• F : CategoryTheory.Functor C D
• faithful : self.F.Faithful
• preservesMono : self.F.PreservesMonomorphisms
• preservesEpi : self.F.PreservesEpimorphisms
• monoidal : self.F.Monoidal

def TensorCategories.TensorFunctor.toQuasiTensorFunctor {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (TF : TensorFunctor k C D) : QuasiTensorFunctor k C D

Every tensor functor is in particular a quasi-tensor functor: the monoidal structure provides the natural isomorphisms J and the unit isomorphism.

@[reducible, inline]

abbrev TensorCategories.Definition_1_14_1_QuasiTensorFunctor (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u₁) [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u u₁) v) v₁)

Reference abbreviation for Definition 1.14.1: a quasi-tensor functor.

@[reducible, inline]

abbrev TensorCategories.Definition_1_14_1_TensorFunctor (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u₁) [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u u₁) v) v₁)

Reference abbreviation for Definition 1.14.1: a tensor functor.

theorem TensorCategories.QuasiTensorFunctor.isLeftExact {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (QTF : QuasiTensorFunctor k C D) : QTF.F.PreservesMonomorphisms

A quasi-tensor functor is left exact: its underlying functor preserves monomorphisms.

theorem TensorCategories.QuasiTensorFunctor.isRightExact {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (QTF : QuasiTensorFunctor k C D) : QTF.F.PreservesEpimorphisms

A quasi-tensor functor is right exact: its underlying functor preserves epimorphisms.

theorem TensorCategories.QuasiTensorFunctor.isFaithful {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (QTF : QuasiTensorFunctor k C D) : QTF.F.Faithful

A quasi-tensor functor is faithful.

def TensorCategories.QuasiTensorFunctor.preservesUnit {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (QTF : QuasiTensorFunctor k C D) : QTF.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

A quasi-tensor functor preserves the unit object, as recorded by its unit isomorphism.

theorem TensorCategories.TensorFunctor.isLeftExact {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (TF : TensorFunctor k C D) : TF.F.PreservesMonomorphisms

A tensor functor is left exact: its underlying functor preserves monomorphisms.

theorem TensorCategories.TensorFunctor.isRightExact {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (TF : TensorFunctor k C D) : TF.F.PreservesEpimorphisms

A tensor functor is right exact: its underlying functor preserves epimorphisms.

theorem TensorCategories.TensorFunctor.isFaithful {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (TF : TensorFunctor k C D) : TF.F.Faithful

A tensor functor is faithful.

def TensorCategories.TensorFunctor.preservesUnit {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (TF : TensorFunctor k C D) : TF.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit D

The unit isomorphism of a tensor functor, derived from its monoidal structure.

def TensorCategories.QuasiTensorFunctor.toTensorFunctor_of_monoidal {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] (QTF : QuasiTensorFunctor k C D) (hmon : QTF.F.Monoidal) : TensorFunctor k C D

A quasi-tensor functor whose underlying functor carries a monoidal structure upgrades to a tensor functor.

structure TensorCategories.QuasiFiberFunctor (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] extends TensorCategories.QuasiTensorFunctor k C (ModuleCat k) : Type (max (max u v) (w + 1))

Definition 1.19.1 (Etingof–Gelaki–Nikshych–Ostrik): A quasi-fiber functor on an abelian monoidal category C over a field k is a quasi-tensor functor from C to the category of k-modules.

• F : CategoryTheory.Functor C (ModuleCat k)
• faithful : self.F.Faithful
• preservesMono : self.F.PreservesMonomorphisms
• preservesEpi : self.F.PreservesEpimorphisms
• J (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (self.F.obj X) (self.F.obj Y) ≅ self.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
• J_natural_left {X X' : C} (f : X ⟶ X') (Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (self.F.map f) (self.F.obj Y)) (self.J X' Y).hom = CategoryTheory.CategoryStruct.comp (self.J X Y).hom (self.F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Y))
• J_natural_right (X : C) {Y Y' : C} (g : Y ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (self.F.obj X) (self.F.map g)) (self.J X Y').hom = CategoryTheory.CategoryStruct.comp (self.J X Y).hom (self.F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X g))
• unitIso : self.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ CategoryTheory.MonoidalCategoryStruct.tensorUnit (ModuleCat k)

structure TensorCategories.FiberFunctor (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] : Type (max (max u v) (w + 1))

Definition 1.19.1 (Etingof–Gelaki–Nikshych–Ostrik): A fiber functor on an abelian monoidal category C over a field k is a tensor functor from C to the category of k-modules.

• F : CategoryTheory.Functor C (ModuleCat k)
• faithful : self.F.Faithful
• preservesMono : self.F.PreservesMonomorphisms
• preservesEpi : self.F.PreservesEpimorphisms
• monoidal : self.F.Monoidal

@[reducible, inline]

abbrev TensorCategories.Definition_1_19_1_QuasiFiberFunctor (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))

Reference abbreviation for Definition 1.19.1: a quasi-fiber functor.

@[reducible, inline]

abbrev TensorCategories.Definition_1_19_1_FiberFunctor (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))

Reference abbreviation for Definition 1.19.1: a fiber functor.

def TensorCategories.FiberFunctor.toTensorFunctor {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) : TensorFunctor k C (ModuleCat k)

A fiber functor on C is in particular a tensor functor from C to the category of k-modules.

def TensorCategories.FiberFunctor.toQuasiFiberFunctor {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (FF : FiberFunctor k C) : QuasiFiberFunctor k C

A fiber functor is in particular a quasi-fiber functor, via its monoidal structure.

def TensorCategories.FiberFunctor.ofTensorFunctorToVec {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (TF : TensorFunctor k C (ModuleCat k)) : FiberFunctor k C

A tensor functor from C to the category of k-modules is a fiber functor on C.

def TensorCategories.QuasiFiberFunctor.toQuasiTensorFunctorToVec {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (QFF : QuasiFiberFunctor k C) : QuasiTensorFunctor k C (ModuleCat k)

Exhibit a quasi-fiber functor as a quasi-tensor functor into the category of k-modules.

def TensorCategories.QuasiFiberFunctor.IsNormalized {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (QFF : QuasiFiberFunctor k C) : Prop

Definition 1.34.1 (Etingof–Gelaki–Nikshych–Ostrik): A quasi-fiber functor QFF is normalized when the natural isomorphisms J are compatible with the left and right unit constraints via the unit isomorphism.

@[reducible, inline]

abbrev TensorCategories.Definition_1_34_1_IsNormalized {k : Type u_1} [Field k] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (QFF : QuasiFiberFunctor k C) : Prop

Reference abbreviation for Definition 1.34.1: a normalized quasi-fiber functor.

@[reducible, inline]

abbrev TensorCategories.Definition_1_34_1 {k : Type u_1} [Field k] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (QFF : QuasiFiberFunctor k C) : Prop

Reference abbreviation for Definition 1.34.1.

def TensorCategories.QuasiFiberFunctor.TwistEquivalent {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (QFF₁ QFF₂ : QuasiFiberFunctor k C) : Prop

Definition 1.34.2 (Etingof–Gelaki–Nikshych–Ostrik): Two quasi-fiber functors on C are twist-equivalent if they share the same underlying functor.

noncomputable def TensorCategories.QuasiFiberFunctor.twist {k : Type w} [Field k] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (QFF₁ QFF₂ : QuasiFiberFunctor k C) (h : QFF₁.TwistEquivalent QFF₂) (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (QFF₁.F.obj X) (QFF₁.F.obj Y) ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj (QFF₁.F.obj X) (QFF₁.F.obj Y)

The twist isomorphism on QFF₁.F X ⊗ QFF₁.F Y obtained from a twist-equivalence h : QFF₁.TwistEquivalent QFF₂, comparing the two natural isomorphisms J on the same underlying functor.

@[reducible, inline]

abbrev TensorCategories.Definition_1_34_2 {k : Type u_1} [Field k] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (QFF₁ QFF₂ : QuasiFiberFunctor k C) : Prop

Reference abbreviation for Definition 1.34.2: twist-equivalence of quasi-fiber functors.

structure TensorCategories.IsProjectiveGenerator {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (P : C) : Prop

An object P of an abelian category C is a projective generator if it is projective and detects zero objects (any X admitting only the zero map from P must itself be zero).

• proj : CategoryTheory.Projective P
• generates (X : C) : (∀ (f : P ⟶ X), f = 0) → CategoryTheory.Limits.IsZero X

theorem TensorCategories.projective_generator_exists (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughProjectives C] (hHomFiniteDim : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) : ∃ (P : C), IsProjectiveGenerator P

Every finite abelian k-linear category with enough projectives admits a projective generator.

theorem TensorCategories.projGen_fiberFunctor (k : Type w) [Field k] [IsAlgClosed k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.RigidCategory C] [CategoryTheory.EnoughProjectives C] (hHomFiniteDim : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (hEnd : Nonempty (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≃ₐ[k] k)) (P : C) (hP : IsProjectiveGenerator P) : Nonempty (FiberFunctor k C)

A finite rigid k-linear monoidal category over an algebraically closed field with End(𝟙) ≃ₐ[k] k and a projective generator P admits a fiber functor.

theorem TensorCategories.endFiberFunctor_isHopfAlgebra (k : Type w) [Field k] [IsAlgClosed k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.RigidCategory C] [CategoryTheory.EnoughProjectives C] (hHomFiniteDim : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (hEnd : Nonempty (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≃ₐ[k] k)) (FF : FiberFunctor k C) : Nonempty (HopfAlgebra k (CategoryTheory.End FF.F))

The endomorphism algebra of a fiber functor on a finite rigid k-linear monoidal category over an algebraically closed field carries a Hopf algebra structure.

theorem TensorCategories.endFiberFunctor_finiteDimensional (k : Type w) [Field k] [IsAlgClosed k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] [CategoryTheory.RigidCategory C] [CategoryTheory.EnoughProjectives C] (hHomFiniteDim : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (hEnd : Nonempty (CategoryTheory.End (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≃ₐ[k] k)) (FF : FiberFunctor k C) : Module.Finite k (CategoryTheory.End FF.F)

The endomorphism algebra of a fiber functor on a finite rigid k-linear monoidal category over an algebraically closed field is finite-dimensional.

theorem TensorCategories.repHopf_finiteTensorWithFiberFunctor (k : Type w) [Field k] [IsAlgClosed k] (H : Type v) [Ring H] [Algebra k H] [HopfAlgebra k H] [FiniteDimensional k H] : ∃ (C : Type (max u v w)) (x : CategoryTheory.Category.{v, max (max u v) w} C) (x_1 : CategoryTheory.Preadditive C) (x_2 : CategoryTheory.Linear k C) (x_3 : CategoryTheory.Abelian C) (x_4 : CategoryTheory.MonoidalCategory C) (x_5 : CategoryTheory.RigidCategory C), Nonempty (FiberFunctor k C)

Every finite-dimensional Hopf algebra H over an algebraically closed field arises as the endomorphisms of a fiber functor on some finite rigid k-linear monoidal category.

theorem TensorCategories.exact_faithful_functor_unique_on_finite_abelian_monoidal (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] (hHomFiniteDim : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (F₁ F₂ : CategoryTheory.Functor C (ModuleCat k)) [F₁.Faithful] [F₁.PreservesMonomorphisms] [F₁.PreservesEpimorphisms] [F₂.Faithful] [F₂.PreservesMonomorphisms] [F₂.PreservesEpimorphisms] : Nonempty (F₁ ≅ F₂)

Any two exact faithful k-linear functors from a finite abelian monoidal category to the category of k-modules are naturally isomorphic.

theorem TensorCategories.prop_1_34_7 (k : Type w) [Field k] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Preadditive C] [CategoryTheory.Linear k C] [CategoryTheory.Abelian C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalPreadditive C] [CategoryTheory.MonoidalLinear k C] (hHomFiniteDim : ∀ (X Y : C), FiniteDimensional k (X ⟶ Y)) (F₁ F₂ : QuasiFiberFunctor k C) : Nonempty (F₁.F ≅ F₂.F)

Proposition 1.34.7 (Etingof–Gelaki–Nikshych–Ostrik): On a finite abelian k-linear monoidal category, any two quasi-fiber functors are naturally isomorphic on the underlying functors; equivalently, a quasi-fiber functor is unique up to twisting.

@[reducible, inline]

abbrev Definition_1_14_1_QuasiTensorFunctor (k : Type u_1) [Field k] (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u_4) [CategoryTheory.Category.{u_5, u_4} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u_2 u_4) u_3) u_5)

Reference abbreviation for Definition 1.14.1: a quasi-tensor functor.

@[reducible, inline]

abbrev Definition_1_14_1_TensorFunctor (k : Type u_1) [Field k] (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u_4) [CategoryTheory.Category.{u_5, u_4} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u_2 u_4) u_3) u_5)

Reference abbreviation for Definition 1.14.1: a tensor functor.

@[reducible, inline]

abbrev Definition_1_14_1 (k : Type u_1) [Field k] (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.Abelian C] (D : Type u_4) [CategoryTheory.Category.{u_5, u_4} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.Abelian D] : Type (max (max (max u_2 u_4) u_3) u_5)

Reference abbreviation for Definition 1.14.1.

@[reducible, inline]

abbrev Definition_1_19_1_QuasiFiberFunctor (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))

Reference abbreviation for Definition 1.19.1: a quasi-fiber functor.

@[reducible, inline]

abbrev Definition_1_19_1_FiberFunctor (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))

Reference abbreviation for Definition 1.19.1: a fiber functor.

@[reducible, inline]

abbrev Definition_1_19_1 (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))

Reference abbreviation for Definition 1.19.1.