Yoneda embedding of CommGrp_ C

class CommGrpObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) extends GrpObj X, IsCommMonObj X : Type v

Abbreviation for an unbundled commutative group object. It is a group object that is a commutative monoid object.

• one : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ X
• mul : CategoryTheory.MonoidalCategoryStruct.tensorObj X X ⟶ X
• one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight one X) mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom
• mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X one) mul = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
• mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight mul X) mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X X X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X mul) mul)
• inv : X ⟶ X
• left_inv : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X)) MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) MonObj.one
• right_inv : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv) MonObj.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) MonObj.one
• mul_comm : CategoryTheory.CategoryStruct.comp (β_ X X).hom MonObj.mul = MonObj.mul

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

def CommGrp_Class {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : Type v

Alias of CommGrpObj.

---

Abbreviation for an unbundled commutative group object. It is a group object that is a commutative monoid object.

Equations

• @CommGrp_Class = @CommGrpObj

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

If X represents a presheaf of commutative groups, then X is a commutative group object.

Equations

• CommGrpObj.ofRepresentableBy X F α = { toGrpObj := GrpObj.ofRepresentableBy X (F.comp (CategoryTheory.forget₂ CommGrp Grp)) α, toIsCommMonObj := ⋯ }

@[deprecated CommGrpObj.ofRepresentableBy (since := "2025-09-13")]

def CommGrp_Class.ofRepresentableBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (F : CategoryTheory.Functor Cᵒᵖ CommGrp) (α : (F.comp (CategoryTheory.forget CommGrp)).RepresentableBy X) : CommGrpObj X

Alias of CommGrpObj.ofRepresentableBy.

---

If X represents a presheaf of commutative groups, then X is a commutative group object.

Equations

• @CommGrp_Class.ofRepresentableBy = @CommGrpObj.ofRepresentableBy