Documentation

Mathlib.CategoryTheory.Monoidal.Bimon_

The category of bimonoids in a braided monoidal category. #

We define bimonoids in a braided monoidal category C as comonoid objects in the category of monoid objects in C.

We verify that this is equivalent to the monoid objects in the category of comonoid objects.

TODO #

source
class CategoryTheory.BimonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) extends CategoryTheory.MonObj M, CategoryTheory.ComonObj M :
Type v₁

A bimonoid object in a braided category C is an object that is simultaneously monoid and comonoid objects, and structure morphisms of them satisfy appropriate consistency conditions.

Instances
    source
    @[simp]
    theorem CategoryTheory.BimonObj.one_comul_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {inst✝² : BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorObj M M ⟶ Z) :
    CategoryStruct.comp MonObj.one (CategoryStruct.comp ComonObj.comul h) = CategoryStruct.comp MonObj.one h
    source
    @[simp]
    theorem CategoryTheory.BimonObj.mul_counit_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {inst✝² : BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
    CategoryStruct.comp MonObj.mul (CategoryStruct.comp ComonObj.counit h) = CategoryStruct.comp ComonObj.counit h
    source
    @[simp]
    theorem CategoryTheory.BimonObj.mul_comul_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {inst✝² : BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorObj M M ⟶ Z) :
    CategoryStruct.comp MonObj.mul (CategoryStruct.comp ComonObj.comul h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryStruct.comp (MonoidalCategory.tensorμ M M M M) (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) h))
    source
    @[simp]
    theorem CategoryTheory.BimonObj.one_counit_assoc {C : Type u₁} {inst✝ : Category.{v₁, u₁} C} {inst✝¹ : MonoidalCategory C} {inst✝² : BraidedCategory C} (M : C) [self : BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
    CategoryStruct.comp MonObj.one (CategoryStruct.comp ComonObj.counit h) = h
    source
    class CategoryTheory.IsBimonHom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N : C} [BimonObj M] [BimonObj N] (f : M ⟶ N) extends CategoryTheory.IsMonHom f, CategoryTheory.IsComonHom f :
    Prop

    The property that a morphism between bimonoid objects is a bimonoid morphism.

    Instances
      source
      def CategoryTheory.Bimon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
      Type (max (max u₁ v₁) v₁)

      A bimonoid object in a braided category C is a comonoid object in the (monoidal) category of monoid objects in C.

      Instances For
        source
        @[implicit_reducible]
        instance CategoryTheory.Bimon.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        Category.{v₁, max u₁ v₁} (Bimon C)
        source
        theorem CategoryTheory.Bimon.ext {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y : Bimon C} {f g : X ⟶ Y} (w : f.hom.hom = g.hom.hom) :
        f = g
        source
        theorem CategoryTheory.Bimon.ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X Y : Bimon C} {f g : X ⟶ Y} :
        f = g ↔ f.hom.hom = g.hom.hom
        source
        @[simp]
        theorem CategoryTheory.Bimon.id_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
        (CategoryStruct.id M).hom = CategoryStruct.id M.X
        source
        @[simp]
        theorem CategoryTheory.Bimon.comp_hom' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {M N K : Bimon C} (f : M ⟶ N) (g : N ⟶ K) :
        (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom
        source
        @[reducible, inline]
        abbrev CategoryTheory.Bimon.toMon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
        Functor (Bimon C) (Mon C)

        The forgetful functor from bimonoid objects to monoid objects.

        Instances For
          source
          def CategoryTheory.Bimon.forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
          Functor (Bimon C) C

          The forgetful functor from bimonoid objects to the underlying category.

          Instances For
            source
            @[simp]
            theorem CategoryTheory.Bimon.toMon_forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
            (toMon C).comp (Mon.forget C) = forget C
            source
            def CategoryTheory.Bimon.toComon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
            Functor (Bimon C) (Comon C)

            The forgetful functor from bimonoid objects to comonoid objects.

            Instances For
              source
              @[simp]
              theorem CategoryTheory.Bimon.toComon_obj_comon_comul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Comon (Mon C)) :
              ComonObj.comul = ComonObj.comul.hom
              source
              @[simp]
              theorem CategoryTheory.Bimon.toComon_obj_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Comon (Mon C)) :
              ((toComon C).obj A).X = A.X.X
              source
              @[simp]
              theorem CategoryTheory.Bimon.toComon_obj_comon_counit (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Comon (Mon C)) :
              ComonObj.counit = ComonObj.counit.hom
              source
              @[simp]
              theorem CategoryTheory.Bimon.toComon_map_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : Comon (Mon C)} (f : X✝ ⟶ Y✝) :
              ((toComon C).map f).hom = f.hom.hom
              source
              @[simp]
              theorem CategoryTheory.Bimon.toComon_forget (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
              (toComon C).comp (Comon.forget C) = forget C
              source
              def CategoryTheory.Bimon.toMonComonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
              Mon (Comon C)

              The object level part of the forward direction of Comon (Mon C) ≌ Mon (Comon C)

              Instances For
                source
                @[simp]
                theorem CategoryTheory.Bimon.toMonComonObj_mon_mul_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                MonObj.mul.hom = MonObj.mul
                source
                @[simp]
                theorem CategoryTheory.Bimon.toMonComonObj_mon_one_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                MonObj.one.hom = MonObj.one
                source
                @[simp]
                theorem CategoryTheory.Bimon.toMonComonObj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                M.toMonComonObj.X = (toComon C).obj M
                source
                def CategoryTheory.Bimon.toMonComon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                Functor (Bimon C) (Mon (Comon C))

                The forward direction of Comon (Mon C) ≌ Mon (Comon C)

                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Bimon.toMonComon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                  (toMonComon C).obj M = M.toMonComonObj
                  source
                  @[simp]
                  theorem CategoryTheory.Bimon.toMonComon_map_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : Bimon C} (f : X✝ ⟶ Y✝) :
                  ((toMonComon C).map f).hom = (toComon C).map f
                  source
                  def CategoryTheory.Bimon.ofMonComonObjX {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                  Mon C

                  Auxiliary definition for ofMonComonObj.

                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Bimon.ofMonComonObjX_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                    (ofMonComonObjX M).X = M.X.X
                    source
                    @[simp]
                    theorem CategoryTheory.Bimon.ofMonComonObjX_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                    MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one.hom
                    source
                    @[simp]
                    theorem CategoryTheory.Bimon.ofMonComonObjX_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                    MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj M.X.X M.X.X)) MonObj.mul.hom
                    source
                    def CategoryTheory.Bimon.ofMonComonObj {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                    Bimon C

                    The object level part of the backward direction of Comon (Mon C) ≌ Mon (Comon C)

                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Bimon.ofMonComonObj_comon_comul_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                      ComonObj.comul.hom = ComonObj.comul
                      source
                      @[simp]
                      theorem CategoryTheory.Bimon.ofMonComonObj_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                      (ofMonComonObj M).X = ofMonComonObjX M
                      source
                      @[simp]
                      theorem CategoryTheory.Bimon.ofMonComonObj_comon_counit_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                      ComonObj.counit.hom = ComonObj.counit
                      source
                      def CategoryTheory.Bimon.ofMonComon (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                      Functor (Mon (Comon C)) (Bimon C)

                      The backward direction of Comon (Mon C) ≌ Mon (Comon C)

                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Bimon.ofMonComon_obj (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                        (ofMonComon C).obj M = ofMonComonObj M
                        source
                        @[simp]
                        theorem CategoryTheory.Bimon.ofMonComon_map_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : Mon (Comon C)} (f : X✝ ⟶ Y✝) :
                        ((ofMonComon C).map f).hom = (Comon.forget C).mapMon.map f
                        source
                        @[simp]
                        theorem CategoryTheory.Bimon.toMonComon_ofMonComon_obj_one {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                        MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one
                        source
                        @[simp]
                        theorem CategoryTheory.Bimon.toMonComon_ofMonComon_obj_mul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                        MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj M.X.X M.X.X)) MonObj.mul
                        source
                        def CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                        M.X.X ≅ (((toMonComon C).comp (ofMonComon C)).obj M).X.X

                        Auxiliary definition for equivMonComonUnitIsoApp.

                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                          M.equivMonComonUnitIsoAppXAux.hom = CategoryStruct.id M.X.X
                          source
                          @[simp]
                          theorem CategoryTheory.Bimon.equivMonComonUnitIsoAppXAux_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                          M.equivMonComonUnitIsoAppXAux.inv = CategoryStruct.id M.X.X
                          source
                          instance CategoryTheory.Bimon.instIsMonHomHomEquivMonComonUnitIsoAppXAux {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                          IsMonHom M.equivMonComonUnitIsoAppXAux.hom
                          source
                          def CategoryTheory.Bimon.equivMonComonUnitIsoAppX {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                          M.X ≅ (((toMonComon C).comp (ofMonComon C)).obj M).X

                          Auxiliary definition for equivMonComonUnitIsoApp.

                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.Bimon.equivMonComonUnitIsoAppX_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                            M.equivMonComonUnitIsoAppX.hom.hom = CategoryStruct.id M.X.X
                            source
                            @[simp]
                            theorem CategoryTheory.Bimon.equivMonComonUnitIsoAppX_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                            M.equivMonComonUnitIsoAppX.inv.hom = CategoryStruct.id M.X.X
                            source
                            instance CategoryTheory.Bimon.instIsComonHomMonHomEquivMonComonUnitIsoAppX {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                            IsComonHom M.equivMonComonUnitIsoAppX.hom
                            source
                            def CategoryTheory.Bimon.equivMonComonUnitIsoApp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                            M ≅ ((toMonComon C).comp (ofMonComon C)).obj M

                            The unit for the equivalence Comon (Mon C) ≌ Mon (Comon C).

                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Bimon.equivMonComonUnitIsoApp_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                              M.equivMonComonUnitIsoApp.hom.hom.hom = CategoryStruct.id M.X.X
                              source
                              @[simp]
                              theorem CategoryTheory.Bimon.equivMonComonUnitIsoApp_inv_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                              M.equivMonComonUnitIsoApp.inv.hom.hom = CategoryStruct.id M.X.X
                              source
                              @[simp]
                              theorem CategoryTheory.Bimon.ofMonComon_toMonComon_obj_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                              ComonObj.counit = CategoryStruct.comp ComonObj.counit (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C))
                              source
                              @[simp]
                              theorem CategoryTheory.Bimon.ofMonComon_toMonComon_obj_comul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                              ComonObj.comul = CategoryStruct.comp ComonObj.comul (CategoryStruct.id (MonoidalCategoryStruct.tensorObj M.X.X M.X.X))
                              source
                              def CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                              (((ofMonComon C).comp (toMonComon C)).obj M).X.X ≅ M.X.X

                              Auxiliary definition for equivMonComonCounitIsoApp.

                              Instances For
                                source
                                @[simp]
                                theorem CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                (equivMonComonCounitIsoAppXAux M).hom = CategoryStruct.id M.X.X
                                source
                                @[simp]
                                theorem CategoryTheory.Bimon.equivMonComonCounitIsoAppXAux_inv {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                (equivMonComonCounitIsoAppXAux M).inv = CategoryStruct.id M.X.X
                                source
                                instance CategoryTheory.Bimon.instIsComonHomHomEquivMonComonCounitIsoAppXAux {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                IsComonHom (equivMonComonCounitIsoAppXAux M).hom
                                source
                                def CategoryTheory.Bimon.equivMonComonCounitIsoAppX {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                (((ofMonComon C).comp (toMonComon C)).obj M).X ≅ M.X

                                Auxiliary definition for equivMonComonCounitIsoApp.

                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Bimon.equivMonComonCounitIsoAppX_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                  (equivMonComonCounitIsoAppX M).hom.hom = CategoryStruct.id M.X.X
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Bimon.equivMonComonCounitIsoAppX_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                  (equivMonComonCounitIsoAppX M).inv.hom = CategoryStruct.id M.X.X
                                  source
                                  instance CategoryTheory.Bimon.instIsMonHomComonHomEquivMonComonCounitIsoAppX {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                  IsMonHom (equivMonComonCounitIsoAppX M).hom
                                  source
                                  def CategoryTheory.Bimon.equivMonComonCounitIsoApp {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                  ((ofMonComon C).comp (toMonComon C)).obj M ≅ M

                                  The counit for the equivalence Comon (Mon C) ≌ Mon (Comon C).

                                  Instances For
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Bimon.equivMonComonCounitIsoApp_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                    (equivMonComonCounitIsoApp M).hom.hom.hom = CategoryStruct.id M.X.X
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Bimon.equivMonComonCounitIsoApp_inv_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Mon (Comon C)) :
                                    (equivMonComonCounitIsoApp M).inv.hom.hom = CategoryStruct.id M.X.X
                                    source
                                    def CategoryTheory.Bimon.equivMonComon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                    Bimon C ≌ Mon (Comon C)

                                    The equivalence Comon (Mon C) ≌ Mon (Comon C)

                                    Instances For

                                      The trivial bimonoid #

                                      source
                                      def CategoryTheory.Bimon.trivial (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                      Bimon C

                                      The trivial bimonoid object.

                                      Instances For
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Bimon.trivial_X_X (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                        (trivial C).X.X = MonoidalCategoryStruct.tensorUnit C
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Bimon.trivial_X_mon_mul (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                        MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Bimon.trivial_comon_counit_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                        ComonObj.counit.hom = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Bimon.trivial_X_mon_one (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                        MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Bimon.trivial_comon_comul_hom (C : Type u₁) [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] :
                                        ComonObj.comul.hom = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv
                                        source
                                        def CategoryTheory.Bimon.trivialTo {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Bimon C) :
                                        trivial C ⟶ A

                                        The bimonoid morphism from the trivial bimonoid to any bimonoid.

                                        Instances For
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Bimon.trivialTo_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Bimon C) :
                                          A.trivialTo.hom = default
                                          source
                                          def CategoryTheory.Bimon.toTrivial {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Bimon C) :
                                          A ⟶ trivial C

                                          The bimonoid morphism from any bimonoid to the trivial bimonoid.

                                          Instances For
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Bimon.toTrivial_hom {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (A : Bimon C) :
                                            A.toTrivial.hom = ComonObj.counit

                                            Additional lemmas #

                                            source
                                            theorem CategoryTheory.Bimon.BimonObjAux_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                                            ComonObj.counit = ComonObj.counit.hom
                                            source
                                            theorem CategoryTheory.Bimon.BimonObjAux_comul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                                            ComonObj.comul = ComonObj.comul.hom
                                            source
                                            @[implicit_reducible]
                                            instance CategoryTheory.Bimon.instBimonObjXXMon {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : Bimon C) :
                                            BimonObj M.X.X
                                            source
                                            theorem CategoryTheory.Bimon.one_comul {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] :
                                            CategoryStruct.comp MonObj.one ComonObj.comul = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one)
                                            source
                                            theorem CategoryTheory.Bimon.one_comul_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorObj M M ⟶ Z) :
                                            CategoryStruct.comp MonObj.one (CategoryStruct.comp ComonObj.comul h) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.one MonObj.one) h)
                                            source
                                            theorem CategoryTheory.Bimon.mul_counit {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] :
                                            CategoryStruct.comp MonObj.mul ComonObj.counit = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.counit) (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom
                                            source
                                            theorem CategoryTheory.Bimon.mul_counit_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorUnit C ⟶ Z) :
                                            CategoryStruct.comp MonObj.mul (CategoryStruct.comp ComonObj.counit h) = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.counit ComonObj.counit) (CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom h)
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Bimon.compatibility {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] :
                                            CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryStruct.comp (MonoidalCategoryStruct.associator M M (MonoidalCategoryStruct.tensorObj M M)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M (MonoidalCategoryStruct.associator M M M).inv) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M (MonoidalCategoryStruct.whiskerRight (β_ M M).hom M)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M (MonoidalCategoryStruct.associator M M M).hom) (CategoryStruct.comp (MonoidalCategoryStruct.associator M M (MonoidalCategoryStruct.tensorObj M M)).inv (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul)))))) = CategoryStruct.comp MonObj.mul ComonObj.comul

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

                                            source
                                            @[simp]
                                            theorem CategoryTheory.Bimon.compatibility_assoc {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (M : C) [BimonObj M] {Z : C} (h : MonoidalCategoryStruct.tensorObj M M ⟶ Z) :
                                            CategoryStruct.comp (MonoidalCategoryStruct.tensorHom ComonObj.comul ComonObj.comul) (CategoryStruct.comp (MonoidalCategoryStruct.associator M M (MonoidalCategoryStruct.tensorObj M M)).hom (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M (MonoidalCategoryStruct.associator M M M).inv) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M (MonoidalCategoryStruct.whiskerRight (β_ M M).hom M)) (CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft M (MonoidalCategoryStruct.associator M M M).hom) (CategoryStruct.comp (MonoidalCategoryStruct.associator M M (MonoidalCategoryStruct.tensorObj M M)).inv (CategoryStruct.comp (MonoidalCategoryStruct.tensorHom MonObj.mul MonObj.mul) h)))))) = CategoryStruct.comp MonObj.mul (CategoryStruct.comp ComonObj.comul h)

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

                                            source
                                            def CategoryTheory.Bimon.mk'X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [BimonObj X] :
                                            Mon C

                                            Auxiliary definition for Bimon.mk'.

                                            Instances For
                                              source
                                              @[simp]
                                              theorem CategoryTheory.Bimon.mk'X_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [BimonObj X] :
                                              (mk'X X).X = X
                                              source
                                              def CategoryTheory.Bimon.mk' {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [BimonObj X] :
                                              Bimon C

                                              Construct an object of Bimon C from an object X : C and BimonObj X instance.

                                              Instances For
                                                source
                                                @[simp]
                                                theorem CategoryTheory.Bimon.mk'_X {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] [BraidedCategory C] (X : C) [BimonObj X] :
                                                (mk' X).X = mk'X X