Theorems · Definition · category theory

CategoryTheory.Functor.OplaxMonoidal.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} →
              (η :
                  F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit D) →
                (δ :
                    CategoryTheory.MonoidalCategory.curriedTensorPost F ⟶
                      CategoryTheory.MonoidalCategory.curriedTensorPre F) →
                  CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.firstMap δ =
                      CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.secondMap δ →
                    CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapₗ F =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapₗ F)
                          (CategoryTheory.CategoryStruct.comp
                            (δ.app (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                            (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapₗ η)) →
                      CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.leftMapᵣ F =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.topMapᵣ F)
                            (CategoryTheory.CategoryStruct.comp
                              (((CategoryTheory.flipFunctor C C D).map δ).app
                                (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
                              (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ η)) →
                        F.OplaxMonoidal

F is oplax monoidal given a counit morphism η : F.obj (𝟙_ C) ⟶ 𝟙_ D and a tensorator δ : F (- ⊗ -) ⟶ F - ⊗ F - as a natural transformation 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