Documentation

Mathlib.CategoryTheory.Monoidal.CommGrp_

The category of commutative groups in a Cartesian monoidal category #

A commutative group object internal to a Cartesian monoidal category.

  • X : C

    The underlying object in the ambient monoidal category

  • grp : GrpObj self.X
  • comm : IsCommMonObj self.X
Instances For
    @[deprecated CommGrp (since := "2025-10-13")]

    Alias of CommGrp.


    A commutative group object internal to a Cartesian monoidal category.

    Equations
    Instances For

      A commutative group object is a group object.

      Equations
      Instances For
        @[deprecated CommGrp.toGrp (since := "2025-10-13")]

        Alias of CommGrp.toGrp.


        A commutative group object is a group object.

        Equations
        Instances For

          A commutative group object is a commutative monoid object.

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

            Alias of CommGrp.toCommMon.


            A commutative group object is a commutative monoid object.

            Equations
            Instances For
              @[reducible, inline]

              A commutative group object is a monoid object.

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

                Alias of CommGrp.toMon.


                A commutative group object is a monoid object.

                Equations
                Instances For
                  @[deprecated CommGrp.forget₂Grp (since := "2025-10-13")]

                  Alias of CommGrp.forget₂Grp.


                  The forgetful functor from commutative group objects to group objects.

                  Equations
                  Instances For
                    @[deprecated CommGrp.fullyFaithfulForget₂Grp (since := "2025-10-13")]

                    Alias of CommGrp.fullyFaithfulForget₂Grp.


                    The forgetful functor from commutative group objects to group objects is fully faithful.

                    Equations
                    Instances For
                      @[deprecated CommGrp.forget₂CommMon (since := "2025-09-15")]

                      Alias of CommGrp.forget₂CommMon.


                      The forgetful functor from commutative group objects to commutative monoid objects.

                      Equations
                      Instances For
                        @[deprecated CommGrp.fullyFaithfulForget₂CommMon (since := "2025-09-15")]

                        Alias of CommGrp.fullyFaithfulForget₂CommMon.


                        The forgetful functor from commutative group objects to commutative monoid objects is fully faithful.

                        Equations
                        Instances For

                          The forgetful functor from commutative group objects to the ambient category.

                          Equations
                          Instances For
                            def CommGrp.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : C} (e : G H) [GrpObj G] [IsCommMonObj G] [GrpObj H] [IsCommMonObj H] [IsMonHom e.hom] :
                            { X := G, grp := inst✝, comm := inst✝¹ } { X := H, grp := inst✝², comm := inst✝³ }

                            Construct an isomorphism of commutative group objects by giving a monoid isomorphism between the underlying objects.

                            Equations
                            Instances For
                              @[reducible, inline]

                              Construct an isomorphism of group objects by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

                              Equations
                              Instances For

                                A finite-product-preserving functor takes commutative group objects to commutative group objects.

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

                                  If F : C ⥤ D is a fully faithful monoidal functor, then CommGrpCat(F) : CommGrpCat C ⥤ CommGrpCat D is fully faithful too.

                                  Equations
                                  Instances For

                                    The identity functor is also the identity on commutative group objects.

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

                                      Natural transformations between functors lift to commutative group objects.

                                      Equations
                                      Instances For

                                        Natural isomorphisms between functors lift to commutative group objects.

                                        Equations
                                        Instances For

                                          mapCommGrp is functorial in the left-exact functor.

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

                                            An adjunction of braided functors lifts to an adjunction of their lifts to commutative group objects.

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

                                              An equivalence of categories lifts to an equivalence of their commutative group objects.

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