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 #

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

Instances
    theorem Bimon_Class.mul_counit'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {M : C} [self : Bimon_Class M] {Z : C} (h : 𝟙_ C Z) :
    theorem Bimon_Class.one_counit'_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {M : C} [self : Bimon_Class M] {Z : C} (h : 𝟙_ C Z) :

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

    Instances

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

      Equations
      Instances For
        theorem Bimon_.ext (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : Bimon_ C} {f g : X Y} (w : f.hom.hom = g.hom.hom) :
        f = g
        @[reducible, inline]

        The forgetful functor from bimonoid objects to monoid objects.

        Equations
        Instances For

          The forgetful functor from bimonoid objects to the underlying category.

          Equations
          Instances For

            The forgetful functor from bimonoid objects to comonoid objects.

            Equations
            Instances For
              @[simp]

              The object level part of the forward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                The forward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For

                  The object level part of the backward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For

                    The backward direction of Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      The equivalence Comon_ (Mon_ C) ≌ Mon_ (Comon_ C)

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        The trivial bimonoid #

                        The bimonoid morphism from the trivial bimonoid to any bimonoid.

                        Equations
                        Instances For
                          @[deprecated Bimon_.trivialTo]

                          Alias of Bimon_.trivialTo.


                          The bimonoid morphism from the trivial bimonoid to any bimonoid.

                          Equations
                          Instances For

                            The bimonoid morphism from any bimonoid to the trivial bimonoid.

                            Equations
                            Instances For
                              @[deprecated Bimon_.toTrivial]

                              Alias of Bimon_.toTrivial.


                              The bimonoid morphism from any bimonoid to the trivial bimonoid.

                              Equations
                              Instances For

                                Additional lemmas #