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 (SemiCartesianMonoidalCategory.toUnit X) MonObj.one
• right_inv : CategoryStruct.comp (CartesianMonoidalCategory.lift (CategoryStruct.id X) inv) MonObj.mul = CategoryStruct.comp (SemiCartesianMonoidalCategory.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

def CategoryTheory.yonedaCommGrpGrpObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : CommGrp C) : Functor (Grp C)ᵒᵖ CommGrpCat

The yoneda embedding of CommGrp C into presheaves of groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.yonedaCommGrpGrpObj_map {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : CommGrp C) {H I : (Grp C)ᵒᵖ} (f : H ⟶ I) : (yonedaCommGrpGrpObj G).map f = CommGrpCat.ofHom { toFun := fun (x : Opposite.unop H ⟶ G.toGrp) => CategoryStruct.comp f.unop x, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.yonedaCommGrpGrpObj_obj_coe {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : CommGrp C) (H : (Grp C)ᵒᵖ) : ↑((yonedaCommGrpGrpObj G).obj H) = (Opposite.unop H ⟶ G.toGrp)

def CategoryTheory.yonedaCommGrpGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] : Functor (CommGrp C) (Functor (Grp C)ᵒᵖ CommGrpCat)

The yoneda embedding of CommGrp C into presheaves of groups.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.yonedaCommGrpGrp_map_app {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {X₁ X₂ : CommGrp C} (ψ : X₁ ⟶ X₂) (Y : (Grp C)ᵒᵖ) : (yonedaCommGrpGrp.map ψ).app Y = CommGrpCat.ofHom { toFun := fun (x : Opposite.unop Y ⟶ X₁.toGrp) => CategoryStruct.comp x ψ, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CategoryTheory.yonedaCommGrpGrp_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (G : CommGrp C) : yonedaCommGrpGrp.obj G = yonedaCommGrpGrpObj G