Documentation

Mathlib.CategoryTheory.Monoidal.CommGrp_

The category of commutative groups in a Cartesian monoidal category #

source
structure CategoryTheory.CommGrp (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
Type (max u₁ v₁)

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
    source
    @[deprecated CategoryTheory.CommGrp (since := "2025-10-13")]
    def CategoryTheory.CommGrp_ (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
    Type (max u₁ v₁)

    Alias of CategoryTheory.CommGrp.

    A commutative group object internal to a Cartesian monoidal category.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev CategoryTheory.CommGrp.toGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
      Grp C

      A commutative group object is a group object.

      Equations
      Instances For
        source
        theorem CategoryTheory.CommGrp.toGrp_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
        A.toGrp.X = A.X
        source
        @[deprecated CategoryTheory.CommGrp.toGrp (since := "2025-10-13")]
        def CategoryTheory.CommGrp.toGrp_ {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
        Grp C

        Alias of CategoryTheory.CommGrp.toGrp.

        A commutative group object is a group object.

        Equations
        Instances For
          source
          def CategoryTheory.CommGrp.toCommMon {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
          CommMon C

          A commutative group object is a commutative monoid object.

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.CommGrp.toCommMon_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
            A.toCommMon.X = A.X
            source
            @[reducible, inline]
            abbrev CategoryTheory.CommGrp.toMon {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
            Mon C

            A commutative group object is a monoid object.

            Equations
            Instances For
              source
              def CategoryTheory.CommGrp.trivial (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
              CommGrp C

              The trivial commutative group object.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.CommGrp.trivial_grp_mul (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                MonObj.mul = (MonoidalCategoryStruct.leftUnitor (MonoidalCategoryStruct.tensorUnit C)).hom
                source
                @[simp]
                theorem CategoryTheory.CommGrp.trivial_X (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                (trivial C).X = MonoidalCategoryStruct.tensorUnit C
                source
                @[simp]
                theorem CategoryTheory.CommGrp.trivial_grp_one (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                MonObj.one = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                source
                @[simp]
                theorem CategoryTheory.CommGrp.trivial_grp_inv (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                GrpObj.inv = CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)
                source
                @[implicit_reducible]
                instance CategoryTheory.CommGrp.instInhabited {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                Inhabited (CommGrp C)
                Equations
                source
                @[implicit_reducible]
                instance CategoryTheory.CommGrp.instCategory {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                Category.{v₁, max u₁ v₁} (CommGrp C)
                Equations
                • One or more equations did not get rendered due to their size.
                source
                @[simp]
                theorem CategoryTheory.CommGrp.id_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                (CategoryStruct.id A).hom = CategoryStruct.id A.toGrp
                source
                @[simp]
                theorem CategoryTheory.CommGrp.comp_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R S T : CommGrp C} (f : R ⟶ S) (g : S ⟶ T) :
                (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom
                source
                theorem CategoryTheory.CommGrp.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f g : A ⟶ B) (h : f.hom.hom.hom = g.hom.hom.hom) :
                f = g
                source
                theorem CategoryTheory.CommGrp.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} {f g : A ⟶ B} :
                f = g ↔ f.hom.hom.hom = g.hom.hom.hom
                source
                @[deprecated CategoryTheory.CommGrp.id_hom (since := "2025-12-18")]
                theorem CategoryTheory.CommGrp.id' {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                (CategoryStruct.id A).hom = CategoryStruct.id A.toGrp

                Alias of CategoryTheory.CommGrp.id_hom.

                source
                @[deprecated CategoryTheory.CommGrp.comp_hom (since := "2025-12-18")]
                theorem CategoryTheory.CommGrp.comp' {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {R S T : CommGrp C} (f : R ⟶ S) (g : S ⟶ T) :
                (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

                Alias of CategoryTheory.CommGrp.comp_hom.

                source
                def CategoryTheory.CommGrp.forget₂Grp (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                Functor (CommGrp C) (Grp C)

                The forgetful functor from commutative group objects to group objects.

                Equations
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.CommGrp.forget₂Grp_obj_X (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                  ((forget₂Grp C).obj A).X = A.X
                  source
                  @[deprecated CategoryTheory.CommGrp.forget₂Grp (since := "2025-10-13")]
                  def CategoryTheory.CommGrp.forget₂Grp_ (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                  Functor (CommGrp C) (Grp C)

                  Alias of CategoryTheory.CommGrp.forget₂Grp.

                  The forgetful functor from commutative group objects to group objects.

                  Equations
                  Instances For
                    source
                    def CategoryTheory.CommGrp.fullyFaithfulForget₂Grp (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                    (forget₂Grp C).FullyFaithful

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

                    Equations
                    Instances For
                      source
                      @[deprecated CategoryTheory.CommGrp.fullyFaithfulForget₂Grp (since := "2025-10-13")]
                      def CategoryTheory.CommGrp.fullyFaithfulForget₂Grp_ (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                      (forget₂Grp C).FullyFaithful

                      Alias of CategoryTheory.CommGrp.fullyFaithfulForget₂Grp.

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

                      Equations
                      Instances For
                        source
                        instance CategoryTheory.CommGrp.instFullGrpForget₂Grp (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                        (forget₂Grp C).Full
                        source
                        instance CategoryTheory.CommGrp.instFaithfulGrpForget₂Grp (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                        (forget₂Grp C).Faithful
                        source
                        @[simp]
                        theorem CategoryTheory.CommGrp.forget₂Grp_obj_one (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                        MonObj.one = MonObj.one
                        source
                        @[simp]
                        theorem CategoryTheory.CommGrp.forget₂Grp_obj_mul (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                        MonObj.mul = MonObj.mul
                        source
                        @[simp]
                        theorem CategoryTheory.CommGrp.forget₂Grp_map_hom (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f : A ⟶ B) :
                        ((forget₂Grp C).map f).hom = f.hom.hom
                        source
                        def CategoryTheory.CommGrp.forget₂CommMon (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                        Functor (CommGrp C) (CommMon C)

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

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          def CategoryTheory.CommGrp.fullyFaithfulForget₂CommMon (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                          (forget₂CommMon C).FullyFaithful

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

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            source
                            instance CategoryTheory.CommGrp.instFullCommMonForget₂CommMon (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                            (forget₂CommMon C).Full
                            source
                            instance CategoryTheory.CommGrp.instFaithfulCommMonForget₂CommMon (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                            (forget₂CommMon C).Faithful
                            source
                            @[simp]
                            theorem CategoryTheory.CommGrp.forget₂CommMon_obj_one (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                            MonObj.one = MonObj.one
                            source
                            @[simp]
                            theorem CategoryTheory.CommGrp.forget₂CommMon_obj_mul (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                            MonObj.mul = MonObj.mul
                            source
                            @[simp]
                            theorem CategoryTheory.CommGrp.forget₂CommMon_map_hom (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {A B : CommGrp C} (f : A ⟶ B) :
                            ((forget₂CommMon C).map f).hom = f.hom.hom
                            source
                            def CategoryTheory.CommGrp.forget (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                            Functor (CommGrp C) C

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

                            Equations
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.CommGrp.forget_obj (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) :
                              (forget C).obj X = X.X
                              source
                              @[simp]
                              theorem CategoryTheory.CommGrp.forget_map (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X✝ Y✝ : CommGrp C} (f : X✝ ⟶ Y✝) :
                              (forget C).map f = f.hom.hom.hom
                              source
                              instance CategoryTheory.CommGrp.instFaithfulForget (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                              (forget C).Faithful
                              source
                              @[simp]
                              theorem CategoryTheory.CommGrp.forget₂Grp_comp_forget (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                              (forget₂Grp C).comp (Grp.forget C) = forget C
                              source
                              @[simp]
                              theorem CategoryTheory.CommGrp.forget₂CommMon_comp_forget (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                              (forget₂CommMon C).comp (CommMon.forget C) = forget C
                              source
                              instance CategoryTheory.CommGrp.instIsIsoGrpHom (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : CommGrp C} {f : G ⟶ H} [IsIso f] :
                              IsIso f.hom
                              source
                              instance CategoryTheory.CommGrp.instIsIsoMonHomGrp (C : Type u₁) [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : CommGrp C} {f : G ⟶ H} [IsIso f] :
                              IsIso f.hom.hom
                              source
                              def CategoryTheory.CommGrp.mkIso' {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [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
                                source
                                @[simp]
                                theorem CategoryTheory.CommGrp.mkIso'_inv_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [IsCommMonObj G] [GrpObj H] [IsCommMonObj H] [IsMonHom e.hom] :
                                (mkIso' e).inv.hom.hom.hom = e.inv
                                source
                                @[simp]
                                theorem CategoryTheory.CommGrp.mkIso'_hom_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [IsCommMonObj G] [GrpObj H] [IsCommMonObj H] [IsMonHom e.hom] :
                                (mkIso' e).hom.hom.hom.hom = e.hom
                                source
                                @[reducible, inline]
                                abbrev CategoryTheory.CommGrp.mkIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : CommGrp C} (e : G.X ≅ H.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                                G ≅ H

                                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
                                  source
                                  @[simp]
                                  theorem CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : CommGrp C} (e : G.X ≅ H.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                                  (mkIso e one_f mul_f).hom.hom.hom.hom = e.hom
                                  source
                                  @[simp]
                                  theorem CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : CommGrp C} (e : G.X ≅ H.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                                  (mkIso e one_f mul_f).inv.hom.hom.hom = e.inv
                                  source
                                  @[deprecated CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom (since := "2025-12-18")]
                                  theorem CategoryTheory.CommGrp.mkIso_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : CommGrp C} (e : G.X ≅ H.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                                  (mkIso e one_f mul_f).hom.hom.hom.hom = e.hom

                                  Alias of CategoryTheory.CommGrp.mkIso_hom_hom_hom_hom.

                                  source
                                  @[deprecated CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom (since := "2025-12-18")]
                                  theorem CategoryTheory.CommGrp.mkIso_inv_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : CommGrp C} (e : G.X ≅ H.X) (one_f : CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryStruct.comp MonObj.mul e.hom = CategoryStruct.comp (MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) :
                                  (mkIso e one_f mul_f).inv.hom.hom.hom = e.inv

                                  Alias of CategoryTheory.CommGrp.mkIso_inv_hom_hom_hom.

                                  source
                                  @[implicit_reducible]
                                  instance CategoryTheory.CommGrp.uniqueHomFromTrivial {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                                  Unique (trivial C ⟶ A)
                                  Equations
                                  source
                                  instance CategoryTheory.CommGrp.instHasInitial {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                                  Limits.HasInitial (CommGrp C)
                                  source
                                  def CategoryTheory.Functor.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] :
                                  Functor (CommGrp C) (CommGrp D)

                                  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
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Functor.mapCommGrp_obj_grp_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) :
                                    MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map MonObj.mul)
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Functor.mapCommGrp_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) :
                                    (F.mapCommGrp.obj A).X = F.obj A.X
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] {X✝ Y✝ : CommGrp C} (f : X✝ ⟶ Y✝) :
                                    (F.mapCommGrp.map f).hom.hom.hom = F.map f.hom.hom.hom
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Functor.mapCommGrp_obj_grp_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) :
                                    GrpObj.inv = F.map GrpObj.inv
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Functor.mapCommGrp_obj_grp_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) :
                                    MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)
                                    source
                                    instance CategoryTheory.Functor.Faithful.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] [F.Faithful] :
                                    F.mapCommGrp.Faithful
                                    source
                                    def CategoryTheory.Functor.FullyFaithful.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) :
                                    F.mapCommGrp.FullyFaithful

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

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) {X✝ Y✝ : CommGrp C} (f : F.mapCommGrp.obj X✝ ⟶ F.mapCommGrp.obj Y✝) :
                                      hF.mapCommGrp.preimage f = InducedCategory.homMk (Grp.homMk' (hF.mapMon.preimage f.hom.hom))
                                      source
                                      instance CategoryTheory.Functor.Full.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] [F.Full] [F.Faithful] :
                                      F.mapCommGrp.Full
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.mapCommGrp_id_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                                      MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.mapCommpGrp_id_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) :
                                      MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) MonObj.mul
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.comp_mapCommGrp_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (A : CommGrp C) :
                                      MonObj.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map MonObj.one)
                                      source
                                      @[simp]
                                      theorem CategoryTheory.Functor.comp_mapCommGrp_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (A : CommGrp C) :
                                      MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map MonObj.mul)
                                      source
                                      def CategoryTheory.Functor.mapCommGrpIdIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] :
                                      (Functor.id C).mapCommGrp ≅ Functor.id (CommGrp C)

                                      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
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) :
                                        (mapCommGrpIdIso.inv.app X).hom.hom.hom = CategoryStruct.id X.X
                                        source
                                        @[simp]
                                        theorem CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) :
                                        (mapCommGrpIdIso.hom.app X).hom.hom.hom = CategoryStruct.id X.X
                                        source
                                        def CategoryTheory.Functor.mapCommGrpCompIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] :
                                        (F.comp G).mapCommGrp ≅ F.mapCommGrp.comp G.mapCommGrp

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

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (X : CommGrp C) :
                                          (mapCommGrpCompIso.inv.app X).hom.hom.hom = CategoryStruct.id (G.obj (F.obj X.X))
                                          source
                                          @[simp]
                                          theorem CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (X : CommGrp C) :
                                          (mapCommGrpCompIso.hom.app X).hom.hom.hom = CategoryStruct.id (G.obj (F.obj X.X))
                                          source
                                          def CategoryTheory.Functor.mapCommGrpNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (f : F ⟶ F') :
                                          F.mapCommGrp ⟶ F'.mapCommGrp

                                          Natural transformations between functors lift to commutative group objects.

                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            source
                                            @[simp]
                                            theorem CategoryTheory.Functor.mapCommGrpNatTrans_app_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (f : F ⟶ F') (X : CommGrp C) :
                                            ((mapCommGrpNatTrans f).app X).hom.hom.hom = f.app X.X
                                            source
                                            def CategoryTheory.Functor.mapCommGrpNatIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') :
                                            F.mapCommGrp ≅ F'.mapCommGrp

                                            Natural isomorphisms between functors lift to commutative group objects.

                                            Equations
                                            Instances For
                                              source
                                              @[simp]
                                              theorem CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') (X : CommGrp C) :
                                              ((mapCommGrpNatIso e).hom.app X).hom.hom.hom = e.hom.app X.X
                                              source
                                              @[simp]
                                              theorem CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom_hom_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') (X : CommGrp C) :
                                              ((mapCommGrpNatIso e).inv.app X).hom.hom.hom = e.inv.app X.X
                                              source
                                              noncomputable def CategoryTheory.Functor.mapCommGrpFunctor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] :
                                              Functor (C ⥤ₗ D) (Functor (CommGrp C) (CommGrp D))

                                              mapCommGrp is functorial in the left-exact functor.

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                source
                                                @[simp]
                                                theorem CategoryTheory.Functor.mapCommGrpFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : C ⥤ₗ D) :
                                                mapCommGrpFunctor.obj F = F.obj.mapCommGrp
                                                source
                                                @[simp]
                                                theorem CategoryTheory.Functor.mapCommGrpFunctor_map {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {X✝ Y✝ : C ⥤ₗ D} (α : X✝ ⟶ Y✝) :
                                                mapCommGrpFunctor.map α = mapCommGrpNatTrans α.hom
                                                source
                                                noncomputable def CategoryTheory.Adjunction.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] :
                                                F.mapCommGrp ⊣ G.mapCommGrp

                                                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
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Adjunction.mapCommGrp_counit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] :
                                                  a.mapCommGrp.counit = CategoryStruct.comp Functor.mapCommGrpCompIso.inv (CategoryStruct.comp (Functor.mapCommGrpNatTrans a.counit) Functor.mapCommGrpIdIso.hom)
                                                  source
                                                  @[simp]
                                                  theorem CategoryTheory.Adjunction.mapCommGrp_unit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] :
                                                  a.mapCommGrp.unit = CategoryStruct.comp Functor.mapCommGrpIdIso.inv (CategoryStruct.comp (Functor.mapCommGrpNatTrans a.unit) Functor.mapCommGrpCompIso.hom)
                                                  source
                                                  noncomputable def CategoryTheory.Equivalence.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :
                                                  CommGrp C ≌ CommGrp D

                                                  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
                                                    source
                                                    @[simp]
                                                    theorem CategoryTheory.Equivalence.mapCommGrp_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :
                                                    e.mapCommGrp.counitIso = Functor.mapCommGrpCompIso.symm ≪≫ Functor.mapCommGrpNatIso e.counitIso ≪≫ Functor.mapCommGrpIdIso
                                                    source
                                                    @[simp]
                                                    theorem CategoryTheory.Equivalence.mapCommGrp_functor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :
                                                    e.mapCommGrp.functor = e.functor.mapCommGrp
                                                    source
                                                    @[simp]
                                                    theorem CategoryTheory.Equivalence.mapCommGrp_inverse {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :
                                                    e.mapCommGrp.inverse = e.inverse.mapCommGrp
                                                    source
                                                    @[simp]
                                                    theorem CategoryTheory.Equivalence.mapCommGrp_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] :
                                                    e.mapCommGrp.unitIso = Functor.mapCommGrpIdIso.symm ≪≫ Functor.mapCommGrpNatIso e.unitIso ≪≫ Functor.mapCommGrpCompIso