class CommGrp_Class {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) extends Grp_Class X, IsCommMon X : Type u_2

• 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.ChosenFiniteProducts.lift inv (CategoryTheory.CategoryStruct.id X)) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit X) Mon_Class.one
• right_inv' : CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.lift (CategoryTheory.CategoryStruct.id X) inv) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenFiniteProducts.toUnit X) Mon_Class.one
• mul_comm' : CategoryTheory.CategoryStruct.comp (β_ X X).hom Mon_Class.mul = Mon_Class.mul

instance instCommGrp_ClassXMk' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) [CommGrp_Class X] : CommGrp_Class (Grp_.mk' X).X

Equations

• instCommGrp_ClassXMk' X = inst✝

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

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

Equations

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

def CommGrp_.mk' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : C) [Grp_Class X] [IsCommMon X] : CommGrp_ C

Equations

• CommGrp_.mk' X = { toGrp_ := Grp_.mk' X, mul_comm := ⋯ }

instance CommGrp_.instCommGrp_ClassX {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : CommGrp_ C) : CommGrp_Class X.X

Equations

• X.instCommGrp_ClassX = { toGrp_Class := X.instGrp_ClassX, toIsCommMon := ⋯ }

def CommGrp_.yonedaCommGrpGrpObj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : CommGrp_ C) : CategoryTheory.Functor (Grp_ C)ᵒᵖ CommGrp

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 CommGrp_.yonedaCommGrpGrpObj_obj_coe {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : CommGrp_ C) (Y : (Grp_ C)ᵒᵖ) : ↑(X.yonedaCommGrpGrpObj.obj Y) = (Opposite.unop Y ⟶ X.toGrp_)

@[simp]

theorem CommGrp_.yonedaCommGrpGrpObj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : CommGrp_ C) {Y Z : (Grp_ C)ᵒᵖ} (f : Y ⟶ Z) : X.yonedaCommGrpGrpObj.map f = CommGrp.ofHom { toFun := fun (x : Opposite.unop Y ⟶ X.toGrp_) => CategoryTheory.CategoryStruct.comp f.unop x, map_one' := ⋯, map_mul' := ⋯ }

def CommGrp_.yonedaCommGrpGrp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] : CategoryTheory.Functor (CommGrp_ C) (CategoryTheory.Functor (Grp_ C)ᵒᵖ CommGrp)

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 CommGrp_.yonedaCommGrpGrp_map_app {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] {X₁ X₂ : CommGrp_ C} (ψ : X₁ ⟶ X₂) (Y : (Grp_ C)ᵒᵖ) : (yonedaCommGrpGrp.map ψ).app Y = CommGrp.ofHom { toFun := fun (x : Opposite.unop Y ⟶ X₁.toGrp_) => CategoryTheory.CategoryStruct.comp x ψ, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem CommGrp_.yonedaCommGrpGrp_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.ChosenFiniteProducts C] (X : CommGrp_ C) : yonedaCommGrpGrp.obj X = X.yonedaCommGrpGrpObj