Theorems · Theorem · category theory

CategoryTheory.Bimon.compatibility

∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M : C) [inst_3 : CategoryTheory.BimonObj M],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator M M (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
            (CategoryTheory.MonoidalCategoryStruct.associator M M M).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ M M).hom M))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M
                (CategoryTheory.MonoidalCategoryStruct.associator M M M).hom)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.associator M M
                    (CategoryTheory.MonoidalCategoryStruct.tensorObj M M)).inv
                (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul
                  CategoryTheory.MonObj.mul)))))) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.ComonObj.comul

Compatibility of the monoid and comonoid structures, in terms of morphisms in C.

Defined in

Mathlib.CategoryTheory.Monoidal.Bimon_

Cited by

2 results in Mathlib

Foundations

Depth 6 from the axioms · uses propext

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.BraidedCategoryCategoryTheory.BimonObj