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

    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₂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 Grp(F) : Grp C ⥤ Grp 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