Theorems · Definition · category theory

CategoryTheory.Functor.CoreMonoidal.ofBifunctor

{C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            {F : CategoryTheory.Functor C D} →
              (ε :
                  CategoryTheory.MonoidalCategoryStruct.tensorUnit D ≅
                    F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) →
                (μ :
                    CategoryTheory.MonoidalCategory.curriedTensorPre F ≅
                      CategoryTheory.MonoidalCategory.curriedTensorPost F) →
                  CategoryTheory.Functor.LaxMonoidal.ofBifunctor.firstMap μ.hom =
                      CategoryTheory.Functor.LaxMonoidal.ofBifunctor.secondMap μ.hom →
                    CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapₗ F =
                        CategoryTheory.CategoryStruct.comp
                          (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapₗ ε.hom)
                          (CategoryTheory.CategoryStruct.comp
                            (μ.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                            (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapₗ F)) →
                      CategoryTheory.Functor.LaxMonoidal.ofBifunctor.leftMapᵣ F =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.topMapᵣ ε.hom)
                            (CategoryTheory.CategoryStruct.comp
                              (((CategoryTheory.flipFunctor C C D).map μ.hom).app
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                              (CategoryTheory.Functor.LaxMonoidal.ofBifunctor.bottomMapᵣ F)) →
                        F.CoreMonoidal

F is monoidal given a unit isomorphism ε : 𝟙_ D ≅ F.obj (𝟙_ C) and a tensorator isomorphism μ : F - ⊗ F - ≅ F (- ⊗ -) as a natural isomorphism between bifunctors, satisfying the relevant compatibilities.

Defined in

Mathlib.CategoryTheory.Monoidal.Multifunctor

Cited by

0 results in Mathlib

Foundations

Depth 49 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory