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

    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 : Grp_Class self.X
        Instances For

          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 Grp_Class along an isomorphism.

              Equations
              • One or more equations did not get rendered due to their size.
              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.

                  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) [Grp_Class G] [Grp_Class H] [IsMon_Hom 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

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        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

                                    Pullback a group object along a fully faithful monoidal functor.

                                    Equations
                                    Instances For

                                      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