structure TensorCategories.def_1_1_2_MonoidalSubcategory (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] : Type (max (max (max u₁ (u₂ + 1)) v₁) (v₂ + 1))

EGNO Definition 1.1.2: a monoidal subcategory of C is a category D with a faithful monoidal functor ι : D ⥤ C.

• D : Type u₂
• instCat : CategoryTheory.Category.{v₂, u₂} self.D
• instMonoidal : CategoryTheory.MonoidalCategory self.D
• ι : CategoryTheory.Functor self.D C
• instFaithful : self.ι.Faithful
• instMonoidalFunctor : self.ι.Monoidal

def TensorCategories.def_1_1_2_MonoidalSubcategory.ofFullSubcategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (P : CategoryTheory.ObjectProperty C) [P.IsMonoidal] : def_1_1_2_MonoidalSubcategory C

Construct a monoidal subcategory in the sense of EGNO Definition 1.1.2 from any monoidal ObjectProperty on C, using the inclusion of the corresponding full subcategory.

structure TensorCategories.def_1_4_1_MonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] : Type (max (max (max u₁ u₂) v₁) v₂)

EGNO Definition 1.4.1: a monoidal functor C ⥤ D is a functor F together with the data of a monoidal structure on F.

• F : CategoryTheory.Functor C D
• instMonoidal : self.F.Monoidal

def TensorCategories.def_1_4_1_MonoidalFunctor.J {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (MF : def_1_4_1_MonoidalFunctor C D) (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (MF.F.obj X) (MF.F.obj Y) ≅ MF.F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

The monoidal structure morphism J : F X ⊗ F Y ≅ F (X ⊗ Y) of EGNO Definition 1.4.1, extracted from the underlying Functor.Monoidal instance.

@[reducible, inline]

abbrev TensorCategories.def_1_4_5_MonoidalFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) : Type (max u₁ v₂)

EGNO Definition 1.4.5: a monoidal functor on F, expressed as the existence of a Functor.Monoidal structure.

@[reducible, inline]

abbrev TensorCategories.def_1_5_1_MonoidalNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] {F G : CategoryTheory.Functor C D} [F.LaxMonoidal] [G.LaxMonoidal] (η : F ⟶ G) : Prop

EGNO Definition 1.5.1: a monoidal natural transformation between lax monoidal functors, expressed via NatTrans.IsMonoidal.

@[reducible, inline]

abbrev TensorCategories.def_1_5_1_MonoidalFunctorIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] (F G : CategoryTheory.LaxMonoidalFunctor C D) : Type (max u₁ v₂)

EGNO Definition 1.5.1 (isomorphism version): an isomorphism of lax monoidal functors.