Yoneda embedding of CommGrp C

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

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

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

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

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

Alias of CategoryTheory.CommGrpObj.

---

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

Equations

• @CategoryTheory.CommGrp_Class = @CategoryTheory.CommGrpObj

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

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

Equations

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

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

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

Alias of CategoryTheory.CommGrpObj.ofRepresentableBy.

---

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

Equations

• @CategoryTheory.CommGrp_Class.ofRepresentableBy = @CategoryTheory.CommGrpObj.ofRepresentableBy