Yoneda embedding of CommGrp_ C

class CommGrp_Class {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) extends Grp_Class X, IsCommMon 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)) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) Mon_Class.one
• right_inv : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) Mon_Class.one
• mul_comm : CategoryTheory.CategoryStruct.comp (β_ X X).hom Mon_Class.mul = Mon_Class.mul

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) : CommGrp_Class X

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

Equations

• CommGrp_Class.ofRepresentableBy X F α = { toGrp_Class := Grp_Class.ofRepresentableBy X (F.comp (CategoryTheory.forget₂ CommGrp Grp)) α, toIsCommMon := ⋯ }