Theorems · Definition · category theory

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

F is monoidal given a co/unit morphisms ε/η : 𝟙_ D ↔ F.obj (𝟙_ C) and tensorators μ / δ : F - ⊗ F - ↔ F (- ⊗ -) as natural transformations between bifunctors, satisfying the relevant compatibilities.

Defined in

Mathlib.CategoryTheory.Monoidal.Multifunctor

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.MonoidalCategory