Documentation

Mathlib.CategoryTheory.Monoidal.Grp_

The category of groups in a Cartesian monoidal category #

We define group objects in Cartesian monoidal categories.

We show that the associativity diagram of a group object is always Cartesian and deduce that morphisms of group objects commute with taking inverses.

We show that a finite-product-preserving functor takes group objects to group objects.

A group object internal to a cartesian monoidal category. Also see the bundled Grp_.

Instances
    @[deprecated GrpObj (since := "2025-09-13")]

    Alias of GrpObj.


    A group object internal to a cartesian monoidal category. Also see the bundled Grp_.

    Equations
    Instances For

      The inverse in a group object

      Equations
      Instances For

        The inverse in a group object

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

          A group object in a Cartesian monoidal category.

          • X : C

            The underlying object in the ambient monoidal category

          • grp : GrpObj self.X
          Instances For

            A group object is a monoid object.

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

              Alias of Grp_.toMon.


              A group object is a monoid object.

              Equations
              Instances For
                @[deprecated Grp_.mk (since := "2025-06-15")]

                Alias of Grp_.mk.

                Equations
                Instances For
                  @[reducible, inline]

                  Transfer GrpObj along an isomorphism.

                  Equations
                  Instances For

                    The map (· * f).

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

                      The associativity diagram of a group object is Cartesian.

                      In fact, any monoid object whose associativity diagram is Cartesian can be made into a group object (we do not prove this in this file), so we should expect that many properties of group objects follow from this result.

                      @[deprecated GrpObj.toMonObj_injective (since := "2025-09-09")]

                      Alias of GrpObj.toMonObj_injective.

                      theorem GrpObj.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} (h₁ h₂ : GrpObj X) (H : h₁.toMonObj = h₂.toMonObj) :
                      h₁ = h₂
                      @[deprecated Grp_.forget₂Mon (since := "2025-09-15")]

                      Alias of Grp_.forget₂Mon.


                      The forgetful functor from group objects to monoid objects.

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

                        Alias of Grp_.fullyFaithfulForget₂Mon.


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

                        Equations
                        Instances For

                          The forgetful functor from group objects to the ambient category.

                          Equations
                          Instances For
                            @[simp]
                            theorem Grp_.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X✝ Y✝ : Grp_ C} (f : X✝ Y✝) :
                            (forget C).map f = f.hom
                            def Grp_.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {G H : C} (e : G H) [GrpObj G] [GrpObj H] [IsMonHom e.hom] :
                            { X := G, grp := inst✝ } { X := H, grp := inst✝¹ }

                            Construct an isomorphism of 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

                                Grp_ C is cartesian-monoidal #

                                Equations
                                • One or more equations did not get rendered due to their size.
                                @[reducible, inline]

                                The image of a group object under a monoidal functor is a group object.

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem CategoryTheory.Functor.mapGrp_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] {X✝ Y✝ : Grp_ C} (f : X✝ Y✝) :
                                    (F.mapGrp.map f).hom = F.map f.hom

                                    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 composition functor is also the composition on group objects.

                                      Equations
                                      Instances For

                                        Natural transformations between functors lift to group objects.

                                        Equations
                                        Instances For

                                          Natural isomorphisms between functors lift to group objects.

                                          Equations
                                          Instances For

                                            mapGrp is functorial in the left-exact functor.

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[reducible, inline]

                                              Pullback a group object along a fully faithful monoidal functor.

                                              Equations
                                              Instances For
                                                @[deprecated CategoryTheory.Functor.FullyFaithful.grpObj (since := "2025-09-13")]

                                                Alias of CategoryTheory.Functor.FullyFaithful.grpObj.


                                                Pullback a group object along a fully faithful monoidal functor.

                                                Equations
                                                Instances For
                                                  @[simp]

                                                  The essential image of a full and faithful functor between cartesian-monoidal categories is the same on group objects as on objects.

                                                  An adjunction of monoidal functors lifts to an adjunction of their lifts to 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 group objects.

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