@[reducible, inline]

abbrev TensorCategories.MonoidalFunctorProps.Definition_1_4_1_MonoidalFunctor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.MonoidalCategory C] (D : Type u_2) [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.Functor C D) : Type (max u_1 u_4)

EGNO Definition 1.4.1: a monoidal functor F : C ⥤ D, expressed as the existence of a Functor.Monoidal structure on F.

@[reducible, inline]

abbrev TensorCategories.MonoidalFunctorProps.def_1_4_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.4.1 (natural transformations): a monoidal natural transformation between lax monoidal functors.

theorem TensorCategories.MonoidalFunctorProps.Prop_1_4_3_left {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) [F.LaxMonoidal] (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) (F.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X) (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))

EGNO Proposition 1.4.3 (left unitality): for a lax monoidal functor F, the left unitor of F X factors through ε ▷ F X and μ (𝟙_ C) X followed by F (λ_ X).hom.

@[reducible, inline]

abbrev TensorCategories.MonoidalFunctorProps.def_1_4_5_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.4.5: a monoidal natural transformation between lax monoidal functors.

@[implicit_reducible]

noncomputable instance TensorCategories.MonoidalFunctorProps.monoidalFunctor_exactPairing {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) [F.Monoidal] (X Y : C) [CategoryTheory.ExactPairing X Y] : CategoryTheory.ExactPairing (F.obj X) (F.obj Y)

A monoidal functor preserves exact pairings: if (X, Y) is an exact pairing in C, then (F X, F Y) is an exact pairing in D, with evaluation and coevaluation conjugated by the monoidal structure isomorphisms.

instance TensorCategories.MonoidalFunctorProps.monoidalNatTrans_isIso_unit {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.Monoidal] [G.Monoidal] (α : F ⟶ G) [CategoryTheory.NatTrans.IsMonoidal α] : CategoryTheory.IsIso (α.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))

Part of EGNO Exercise 1.10.15: a monoidal natural transformation between strong monoidal functors has invertible component at the unit object.

instance TensorCategories.MonoidalFunctorProps.monoidalNatTrans_isIso_tensor {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.Monoidal] [G.Monoidal] (α : F ⟶ G) [CategoryTheory.NatTrans.IsMonoidal α] (X Y : C) [CategoryTheory.IsIso (α.app X)] [CategoryTheory.IsIso (α.app Y)] : CategoryTheory.IsIso (α.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))

Part of EGNO Exercise 1.10.15: a monoidal natural transformation between strong monoidal functors has invertible component at a tensor product whenever it has invertible components at the factors.

noncomputable def TensorCategories.MonoidalFunctorProps.monoidalNatTrans_inv {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.Monoidal] [G.Monoidal] (α : F ⟶ G) [CategoryTheory.NatTrans.IsMonoidal α] (X : C) [CategoryTheory.HasRightDual X] : G.obj X ⟶ F.obj X

Candidate inverse of α.app X at a right-dualizable object X, built from the evaluation/coevaluation of the right dual together with the inverse component α.app Xᘁ.

theorem TensorCategories.MonoidalFunctorProps.monoidalNatTrans_tensorHom_comp_eval {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.Monoidal] [G.Monoidal] (α : F ⟶ G) [CategoryTheory.NatTrans.IsMonoidal α] (X Y : C) [CategoryTheory.ExactPairing X Y] : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app Y) (α.app X)) (ε_ (G.obj X) (G.obj Y)) = ε_ (F.obj X) (F.obj Y)

Compatibility of a monoidal natural transformation with the evaluation of an exact pairing transported through F and G.

theorem TensorCategories.MonoidalFunctorProps.monoidalNatTrans_coev_comp_tensorHom {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.Monoidal] [G.Monoidal] (α : F ⟶ G) [CategoryTheory.NatTrans.IsMonoidal α] (X Y : C) [CategoryTheory.ExactPairing X Y] : CategoryTheory.CategoryStruct.comp (η_ (F.obj X) (F.obj Y)) (CategoryTheory.MonoidalCategoryStruct.tensorHom (α.app X) (α.app Y)) = η_ (G.obj X) (G.obj Y)

Compatibility of a monoidal natural transformation with the coevaluation of an exact pairing transported through F and G.

instance TensorCategories.MonoidalFunctorProps.monoidalNatTrans_isIso_of_hasRightDual {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.Monoidal] [G.Monoidal] (α : F ⟶ G) [CategoryTheory.NatTrans.IsMonoidal α] (X : C) [CategoryTheory.HasRightDual X] : CategoryTheory.IsIso (α.app X)

Part of EGNO Exercise 1.10.15: a monoidal natural transformation between strong monoidal functors has invertible component at any right-dualizable object.

instance TensorCategories.MonoidalFunctorProps.monoidalNatTrans_isIso_of_rigid {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.RightRigidCategory C] [CategoryTheory.RightRigidCategory D] (F G : CategoryTheory.Functor C D) [F.Monoidal] [G.Monoidal] (α : F ⟶ G) [CategoryTheory.NatTrans.IsMonoidal α] (X : C) : CategoryTheory.IsIso (α.app X)

EGNO Exercise 1.10.15 (rigid case): when both C and D are right-rigid, every monoidal natural transformation between strong monoidal functors is a natural isomorphism.