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
    @[deprecated BimonObj (since := "2025-09-09")]

    Alias of BimonObj.


    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.

    Equations
    Instances For
      @[deprecated IsBimonHom (since := "2025-09-15")]

      Alias of IsBimonHom.


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

      Equations
      Instances For

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

        Equations
        Instances For
          @[deprecated Bimon (since := "2025-09-15")]

          Alias of Bimon.


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

          Equations
          Instances For
            @[reducible, inline]

            The forgetful functor from bimonoid objects to monoid objects.

            Equations
            Instances For
              @[deprecated Bimon.toMon (since := "2025-09-15")]

              Alias of Bimon.toMon.


              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
                    @[deprecated Bimon.toComon (since := "2025-09-15")]

                    Alias of Bimon.toComon.


                    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
                        @[deprecated Bimon.toMonComonObj (since := "2025-09-15")]

                        Alias of Bimon.toMonComonObj.


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

                        Equations
                        Instances For

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

                          Equations
                          Instances For
                            @[deprecated Bimon.toMonComon (since := "2025-09-15")]

                            Alias of Bimon.toMonComon.


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

                            Equations
                            Instances For
                              @[deprecated Bimon.ofMonComonObjX (since := "2025-09-15")]

                              Alias of Bimon.ofMonComonObjX.


                              Auxiliary definition for ofMonComonObj.

                              Equations
                              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
                                  @[deprecated Bimon.ofMonComonObj (since := "2025-09-15")]

                                  Alias of Bimon.ofMonComonObj.


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

                                  Equations
                                  Instances For

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

                                    Equations
                                    Instances For
                                      @[deprecated Bimon.ofMonComon (since := "2025-09-15")]

                                      Alias of Bimon.ofMonComon.


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

                                      Equations
                                      Instances For
                                        @[deprecated Bimon.equivMonComonUnitIsoAppX (since := "2025-09-15")]

                                        Alias of Bimon.equivMonComonUnitIsoAppX.


                                        Auxiliary definition for equivMonComonUnitIsoApp.

                                        Equations
                                        Instances For
                                          @[deprecated Bimon.equivMonComonUnitIsoApp (since := "2025-09-15")]

                                          Alias of Bimon.equivMonComonUnitIsoApp.


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

                                          Equations
                                          Instances For
                                            @[deprecated Bimon.equivMonComonCounitIsoApp (since := "2025-09-15")]

                                            Alias of Bimon.equivMonComonCounitIsoApp.


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

                                            Equations
                                            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
                                                @[deprecated Bimon.equivMonComon (since := "2025-09-15")]

                                                Alias of Bimon.equivMonComon.


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

                                                Equations
                                                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 #

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

                                                      Auxiliary definition for Bimon.mk'.

                                                      Equations
                                                      Instances For

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

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