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 comonoid object in the (monoidal) category of monoid objects in C.

Equations
Instances For
    theorem Bimon_.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : Bimon_ C} {Y : Bimon_ C} {f : X Y} {g : X Y} :
    f = g f.hom.hom = g.hom.hom
    theorem Bimon_.ext (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : Bimon_ C} {Y : Bimon_ C} {f : X Y} {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

          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

                      The bimonoid morphism from any bimonoid to the trivial bimonoid.

                      Equations
                      Instances For

                        Additional lemmas #