Documentation

Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_

Yoneda embedding of Grp C #

We show that group objects are exactly those whose yoneda presheaf is a presheaf of groups, by constructing the yoneda embedding Grp C ⥤ Cᵒᵖ ⥤ GrpCat.{v} and showing that it is fully faithful and its (essential) image is the representable functors.

source
def CategoryTheory.GrpObj.ofRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) :
GrpObj X

If X represents a presheaf of monoids, then X is a monoid object.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[deprecated CategoryTheory.GrpObj.ofRepresentableBy (since := "2025-09-13")]
    def CategoryTheory.Grp_Class.ofRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) :
    GrpObj X

    Alias of CategoryTheory.GrpObj.ofRepresentableBy.

    If X represents a presheaf of monoids, then X is a monoid object.

    Equations
    Instances For
      source
      @[reducible, inline]
      abbrev CategoryTheory.Hom.group {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] :
      Group (X ⟶ G)

      If G is a group object, then Hom(X, G) has a group structure.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem CategoryTheory.Hom.inv_def {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] (f : X ⟶ G) :
        f⁻¹ = CategoryStruct.comp f GrpObj.inv
        source
        def CategoryTheory.yonedaGrpObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] :
        Functor Cᵒᵖ GrpCat

        If G is a group object, then Hom(-, G) is a presheaf of groups.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.yonedaGrpObj_map {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] {X✝ Y✝ : Cᵒᵖ} (φ : X✝ ⟶ Y✝) :
          (yonedaGrpObj G).map φ = GrpCat.ofHom (MonCat.Hom.hom ((yonedaMonObj G).map φ))
          source
          @[simp]
          theorem CategoryTheory.yonedaGrpObj_obj_coe {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] (X : Cᵒᵖ) :
          ↑((yonedaGrpObj G).obj X) = (Opposite.unop X ⟶ G)
          source
          def CategoryTheory.yonedaGrpObjRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] :
          ((yonedaGrpObj G).comp (forget GrpCat)).RepresentableBy G

          If G is a monoid object, then Hom(-, G) as a presheaf of monoids is represented by G.

          Equations
          Instances For
            source
            theorem CategoryTheory.GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] :
            ofRepresentableBy G (yonedaGrpObj G) (yonedaGrpObjRepresentableBy G) = inst✝
            source
            @[deprecated CategoryTheory.GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy (since := "2025-09-13")]
            theorem CategoryTheory.Grp_Class.ofRepresentableBy_yonedaGrpObjRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] :
            GrpObj.ofRepresentableBy G (yonedaGrpObj G) (yonedaGrpObjRepresentableBy G) = inst✝

            Alias of CategoryTheory.GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy.

            source
            def CategoryTheory.yonedaGrpObjIsoOfRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) :
            yonedaGrpObj X ≅ F

            If X represents a presheaf of groups F, then Hom(-, X) is isomorphic to F as a presheaf of groups.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) :
              (yonedaGrpObjIsoOfRepresentableBy X F α).inv = { app := fun (X_1 : Cᵒᵖ) => GrpCat.ofHom ↑{ toEquiv := α.homEquiv.symm, map_mul' := ⋯ }, naturality := ⋯ }
              source
              @[simp]
              theorem CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) :
              (yonedaGrpObjIsoOfRepresentableBy X F α).hom = { app := fun (X_1 : Cᵒᵖ) => GrpCat.ofHom ↑{ toEquiv := α.homEquiv, map_mul' := ⋯ }, naturality := ⋯ }
              source
              def CategoryTheory.yonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
              Functor (Grp C) (Functor Cᵒᵖ GrpCat)

              The yoneda embedding of Grp_C into presheaves of groups.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                @[simp]
                theorem CategoryTheory.yonedaGrp_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : Grp C) :
                yonedaGrp.obj G = yonedaGrpObj G.X
                source
                @[simp]
                theorem CategoryTheory.yonedaGrp_map_app {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H : Grp C} (ψ : G ⟶ H) (Y : Cᵒᵖ) :
                (yonedaGrp.map ψ).app Y = GrpCat.ofHom (MonCat.Hom.hom ((yonedaMon.map ψ.hom).app Y))
                source
                theorem CategoryTheory.yonedaGrp_naturality {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X Y : C} [GrpObj G] [GrpObj H] (α : yonedaGrpObj G ⟶ yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) :
                (ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryStruct.comp f g) = CategoryStruct.comp f ((ConcreteCategory.hom (α.app (Opposite.op Y))) g)
                source
                theorem CategoryTheory.yonedaGrp_naturality_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X Y : C} [GrpObj G] [GrpObj H] (α : yonedaGrpObj G ⟶ yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : H ⟶ Z) :
                CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryStruct.comp f g)) h = CategoryStruct.comp f (CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)
                source
                def CategoryTheory.yonedaGrpFullyFaithful {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
                yonedaGrp.FullyFaithful

                The yoneda embedding for Grp_C is fully faithful.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  instance CategoryTheory.instFullGrpFunctorOppositeGrpCatYonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
                  yonedaGrp.Full
                  source
                  instance CategoryTheory.instFaithfulGrpFunctorOppositeGrpCatYonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
                  yonedaGrp.Faithful
                  source
                  theorem CategoryTheory.essImage_yonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] :
                  yonedaGrp.essImage = (fun (x : Functor Cᵒᵖ GrpCat) => x.comp (forget GrpCat)) ⁻¹' setOf Functor.IsRepresentable
                  source
                  theorem CategoryTheory.GrpObj.inv_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (g : G ⟶ H) [IsMonHom g] :
                  CategoryStruct.comp f⁻¹ g = (CategoryStruct.comp f g)⁻¹
                  source
                  theorem CategoryTheory.GrpObj.inv_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (g : G ⟶ H) [IsMonHom g] {Z : C} (h : H ⟶ Z) :
                  CategoryStruct.comp f⁻¹ (CategoryStruct.comp g h) = CategoryStruct.comp (CategoryStruct.comp f g)⁻¹ h
                  source
                  @[deprecated CategoryTheory.GrpObj.inv_comp (since := "2025-09-13")]
                  theorem CategoryTheory.Grp_Class.inv_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (g : G ⟶ H) [IsMonHom g] :
                  CategoryStruct.comp f⁻¹ g = (CategoryStruct.comp f g)⁻¹

                  Alias of CategoryTheory.GrpObj.inv_comp.

                  source
                  theorem CategoryTheory.GrpObj.div_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f g : X ⟶ G) (h : G ⟶ H) [IsMonHom h] :
                  CategoryStruct.comp (f / g) h = CategoryStruct.comp f h / CategoryStruct.comp g h
                  source
                  theorem CategoryTheory.GrpObj.div_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f g : X ⟶ G) (h : G ⟶ H) [IsMonHom h] {Z : C} (h✝ : H ⟶ Z) :
                  CategoryStruct.comp (f / g) (CategoryStruct.comp h h✝) = CategoryStruct.comp (CategoryStruct.comp f h / CategoryStruct.comp g h) h✝
                  source
                  @[deprecated CategoryTheory.GrpObj.div_comp (since := "2025-09-13")]
                  theorem CategoryTheory.Grp_Class.div_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f g : X ⟶ G) (h : G ⟶ H) [IsMonHom h] :
                  CategoryStruct.comp (f / g) h = CategoryStruct.comp f h / CategoryStruct.comp g h

                  Alias of CategoryTheory.GrpObj.div_comp.

                  source
                  theorem CategoryTheory.GrpObj.zpow_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsMonHom g] :
                  CategoryStruct.comp (f ^ n) g = CategoryStruct.comp f g ^ n
                  source
                  theorem CategoryTheory.GrpObj.zpow_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsMonHom g] {Z : C} (h : H ⟶ Z) :
                  CategoryStruct.comp (f ^ n) (CategoryStruct.comp g h) = CategoryStruct.comp (CategoryStruct.comp f g ^ n) h
                  source
                  @[deprecated CategoryTheory.GrpObj.zpow_comp (since := "2025-09-13")]
                  theorem CategoryTheory.Grp_Class.zpow_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsMonHom g] :
                  CategoryStruct.comp (f ^ n) g = CategoryStruct.comp f g ^ n

                  Alias of CategoryTheory.GrpObj.zpow_comp.

                  source
                  theorem CategoryTheory.GrpObj.comp_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) :
                  CategoryStruct.comp f g⁻¹ = (CategoryStruct.comp f g)⁻¹
                  source
                  theorem CategoryTheory.GrpObj.comp_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : G ⟶ Z) :
                  CategoryStruct.comp f (CategoryStruct.comp g⁻¹ h) = CategoryStruct.comp (CategoryStruct.comp f g)⁻¹ h
                  source
                  @[deprecated CategoryTheory.GrpObj.comp_inv (since := "2025-09-13")]
                  theorem CategoryTheory.Grp_Class.comp_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) :
                  CategoryStruct.comp f g⁻¹ = (CategoryStruct.comp f g)⁻¹

                  Alias of CategoryTheory.GrpObj.comp_inv.

                  source
                  theorem CategoryTheory.GrpObj.comp_div {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) :
                  CategoryStruct.comp f (g / h) = CategoryStruct.comp f g / CategoryStruct.comp f h
                  source
                  theorem CategoryTheory.GrpObj.comp_div_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) {Z : C} (h✝ : G ⟶ Z) :
                  CategoryStruct.comp f (CategoryStruct.comp (g / h) h✝) = CategoryStruct.comp (CategoryStruct.comp f g / CategoryStruct.comp f h) h✝
                  source
                  @[deprecated CategoryTheory.GrpObj.comp_div (since := "2025-09-13")]
                  theorem CategoryTheory.Grp_Class.comp_div {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) :
                  CategoryStruct.comp f (g / h) = CategoryStruct.comp f g / CategoryStruct.comp f h

                  Alias of CategoryTheory.GrpObj.comp_div.

                  source
                  theorem CategoryTheory.GrpObj.comp_zpow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) :
                  CategoryStruct.comp f (g ^ n) = CategoryStruct.comp f g ^ n
                  source
                  theorem CategoryTheory.GrpObj.comp_zpow_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) {Z : C} (h : G ⟶ Z) :
                  CategoryStruct.comp f (CategoryStruct.comp (g ^ n) h) = CategoryStruct.comp (CategoryStruct.comp f g ^ n) h
                  source
                  @[deprecated CategoryTheory.GrpObj.comp_zpow (since := "2025-09-13")]
                  theorem CategoryTheory.Grp_Class.comp_zpow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) :
                  CategoryStruct.comp f (g ^ n) = CategoryStruct.comp f g ^ n

                  Alias of CategoryTheory.GrpObj.comp_zpow.

                  source
                  theorem CategoryTheory.GrpObj.inv_eq_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] :
                  inv = (CategoryStruct.id G)⁻¹
                  source
                  @[simp]
                  theorem CategoryTheory.GrpObj.one_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] :
                  CategoryStruct.comp MonObj.one inv = MonObj.one
                  source
                  @[simp]
                  theorem CategoryTheory.GrpObj.one_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] {Z : C} (h : G ⟶ Z) :
                  CategoryStruct.comp MonObj.one (CategoryStruct.comp inv h) = CategoryStruct.comp MonObj.one h
                  source
                  @[deprecated CategoryTheory.GrpObj.inv_eq_inv (since := "2025-09-13")]
                  theorem CategoryTheory.Grp_Class.inv_eq_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] :
                  GrpObj.inv = (CategoryStruct.id G)⁻¹

                  Alias of CategoryTheory.GrpObj.inv_eq_inv.

                  source
                  instance CategoryTheory.instIsMonHomInvOfIsCommMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] [BraidedCategory C] [IsCommMonObj G] :
                  IsMonHom GrpObj.inv
                  source
                  instance CategoryTheory.instIsMonHomInvHomOfIsCommMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M G : C} [MonObj M] [GrpObj G] [BraidedCategory C] [IsCommMonObj G] {f : M ⟶ G} [IsMonHom f] :
                  IsMonHom f⁻¹
                  source
                  instance CategoryTheory.Grp.instMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : Grp C} [IsCommMonObj H.X] :
                  MonObj H
                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.hom_one {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (H : Grp C) [IsCommMonObj H.X] :
                  MonObj.one.hom.hom = MonObj.one
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.hom_mul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (H : Grp C) [IsCommMonObj H.X] :
                  MonObj.mul.hom.hom = MonObj.mul
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.Hom.hom_one {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] :
                  InducedCategory.Hom.hom 1 = 1
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.Hom.hom_mul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f g : G ⟶ H) :
                  (f * g).hom = f.hom * g.hom
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.Hom.hom_pow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) (n : ℕ) :
                  (f ^ n).hom = f.hom ^ n
                  source
                  instance CategoryTheory.Grp.instGrpObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : Grp C} [IsCommMonObj H.X] :
                  GrpObj H

                  A commutative group object is a group object in the category of group objects.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.Hom.hom_hom_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) :
                  f⁻¹.hom.hom = f.hom.hom⁻¹
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.Hom.hom_hom_div {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f g : G ⟶ H) :
                  (f / g).hom.hom = f.hom.hom / g.hom.hom
                  source
                  @[simp]
                  theorem CategoryTheory.Grp.Hom.hom_hom_zpow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) (n : ℤ) :
                  (f ^ n).hom.hom = f.hom.hom ^ n
                  source
                  @[deprecated CategoryTheory.Grp.Hom.hom_hom_inv (since := "2025-12-18")]
                  theorem CategoryTheory.Grp.Hom.hom_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) :
                  f⁻¹.hom.hom = f.hom.hom⁻¹

                  Alias of CategoryTheory.Grp.Hom.hom_hom_inv.

                  source
                  @[deprecated CategoryTheory.Grp.Hom.hom_hom_div (since := "2025-12-18")]
                  theorem CategoryTheory.Grp.Hom.hom_div {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f g : G ⟶ H) :
                  (f / g).hom.hom = f.hom.hom / g.hom.hom

                  Alias of CategoryTheory.Grp.Hom.hom_hom_div.

                  source
                  @[deprecated CategoryTheory.Grp.Hom.hom_hom_zpow (since := "2025-12-18")]
                  theorem CategoryTheory.Grp.Hom.hom_zpow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) (n : ℤ) :
                  (f ^ n).hom.hom = f.hom.hom ^ n

                  Alias of CategoryTheory.Grp.Hom.hom_hom_zpow.

                  source
                  instance CategoryTheory.Grp.instIsCommMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : Grp C} [IsCommMonObj H.X] :
                  IsCommMonObj H

                  A commutative group object is a commutative group object in the category of group objects.

                  source
                  instance CategoryTheory.Grp.instIsMonHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] [IsCommMonObj G.X] (f : G ⟶ H) :
                  IsMonHom f
                  source
                  @[reducible, inline]
                  abbrev CategoryTheory.Hom.commGroup {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] [BraidedCategory C] [IsCommMonObj G] :
                  CommGroup (X ⟶ G)

                  If G is a commutative group object, then Hom(X, G) has a commutative group structure.

                  Equations
                  Instances For