Yoneda embedding of Grp C

We show that group objects are exactly those whose yoneda presheaf is a presheaf of groups, by constructing the yoneda embedding Grp C ⥤ Cᵒᵖ ⥤ GrpCat.{v} and showing that it is fully faithful and its (essential) image is the representable functors.

@[implicit_reducible]

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

If X represents a presheaf of monoids, then X is a monoid object.

Equations

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

@[implicit_reducible]

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

If X represents a presheaf of additive monoids, then X is an additive monoid object.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Hom.group {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] : Group (X ⟶ G)

If G is a group object, then Hom(X, G) has a group structure.

Equations

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

@[reducible, inline]

abbrev CategoryTheory.Hom.addGroup {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [AddGrpObj G] : AddGroup (X ⟶ G)

If G is an additive group object, then Hom(X, G) has an additive group structure.

Equations

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

theorem CategoryTheory.Hom.inv_def {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] (f : X ⟶ G) : f⁻¹ = CategoryStruct.comp f GrpObj.inv

theorem CategoryTheory.Hom.neg_def {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [AddGrpObj G] (f : X ⟶ G) : -f = CategoryStruct.comp f AddGrpObj.neg

def CategoryTheory.yonedaGrpObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] : Functor Cᵒᵖ GrpCat

If G is a group object, then Hom(-, G) is a presheaf of groups.

Equations

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

def CategoryTheory.yonedaAddGrpObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [AddGrpObj G] : Functor Cᵒᵖ AddGrpCat

If G is an additive group object, then Hom(-, G) is a presheaf of additive groups.

Equations

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

@[simp]

theorem CategoryTheory.yonedaAddGrpObj_obj_coe {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [AddGrpObj G] (X : Cᵒᵖ) : ↑((yonedaAddGrpObj G).obj X) = (Opposite.unop X ⟶ G)

@[simp]

theorem CategoryTheory.yonedaGrpObj_obj_coe {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] (X : Cᵒᵖ) : ↑((yonedaGrpObj G).obj X) = (Opposite.unop X ⟶ G)

@[simp]

theorem CategoryTheory.yonedaGrpObj_map {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] {X✝ Y✝ : Cᵒᵖ} (φ : X✝ ⟶ Y✝) : (yonedaGrpObj G).map φ = GrpCat.ofHom (MonCat.Hom.hom ((yonedaMonObj G).map φ))

@[simp]

theorem CategoryTheory.yonedaAddGrpObj_map {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [AddGrpObj G] {X✝ Y✝ : Cᵒᵖ} (φ : X✝ ⟶ Y✝) : (yonedaAddGrpObj G).map φ = AddGrpCat.ofHom (AddMonCat.Hom.hom ((yonedaAddMonObj G).map φ))

def CategoryTheory.yonedaGrpObjRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] : ((yonedaGrpObj G).comp (forget GrpCat)).RepresentableBy G

If G is a monoid object, then Hom(-, G) as a presheaf of monoids is represented by G.

Equations

• CategoryTheory.yonedaGrpObjRepresentableBy G = CategoryTheory.Functor.representableByEquiv.symm (CategoryTheory.Iso.refl (CategoryTheory.yoneda.obj G))

def CategoryTheory.yonedaAddGrpObjRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [AddGrpObj G] : ((yonedaAddGrpObj G).comp (forget AddGrpCat)).RepresentableBy G

If G is an additive monoid object, then Hom(-, G) as a presheaf of additive monoids is represented by G.

Equations

• CategoryTheory.yonedaAddGrpObjRepresentableBy G = CategoryTheory.Functor.representableByEquiv.symm (CategoryTheory.Iso.refl (CategoryTheory.yoneda.obj G))

theorem CategoryTheory.GrpObj.ofRepresentableBy_yonedaGrpObjRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] : ofRepresentableBy G (yonedaGrpObj G) (yonedaGrpObjRepresentableBy G) = inst✝

theorem CategoryTheory.AddGrpObj.ofRepresentableBy_yonedaAddGrpObjRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [AddGrpObj G] : ofRepresentableBy G (yonedaAddGrpObj G) (yonedaAddGrpObjRepresentableBy G) = inst✝

def CategoryTheory.yonedaGrpObjIsoOfRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) : yonedaGrpObj X ≅ F

If X represents a presheaf of groups F, then Hom(-, X) is isomorphic to F as a presheaf of groups.

Equations

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

def CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ AddGrpCat) (α : (F.comp (forget AddGrpCat)).RepresentableBy X) : yonedaAddGrpObj X ≅ F

If X represents a presheaf of additive groups F, then Hom(-, X) is isomorphic to F as a presheaf of additive groups.

Equations

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

@[simp]

theorem CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) : (yonedaGrpObjIsoOfRepresentableBy X F α).inv = { app := fun (X_1 : Cᵒᵖ) => GrpCat.ofHom ↑{ toEquiv := α.homEquiv.symm, map_mul' := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.yonedaGrpObjIsoOfRepresentableBy_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ GrpCat) (α : (F.comp (forget GrpCat)).RepresentableBy X) : (yonedaGrpObjIsoOfRepresentableBy X F α).hom = { app := fun (X_1 : Cᵒᵖ) => GrpCat.ofHom ↑{ toEquiv := α.homEquiv, map_mul' := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy_hom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ AddGrpCat) (α : (F.comp (forget AddGrpCat)).RepresentableBy X) : (yonedaAddGrpObjIsoOfRepresentableBy X F α).hom = { app := fun (X_1 : Cᵒᵖ) => AddGrpCat.ofHom ↑{ toEquiv := α.homEquiv, map_add' := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (X : C) (F : Functor Cᵒᵖ AddGrpCat) (α : (F.comp (forget AddGrpCat)).RepresentableBy X) : (yonedaAddGrpObjIsoOfRepresentableBy X F α).inv = { app := fun (X_1 : Cᵒᵖ) => AddGrpCat.ofHom ↑{ toEquiv := α.homEquiv.symm, map_add' := ⋯ }, naturality := ⋯ }

def CategoryTheory.yonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : Functor (Grp C) (Functor Cᵒᵖ GrpCat)

The yoneda embedding of Grp C into presheaves of groups.

Equations

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

def CategoryTheory.yonedaAddGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : Functor (AddGrp C) (Functor Cᵒᵖ AddGrpCat)

The yoneda embedding of AddGrp_C into presheaves of additive groups.

Equations

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

@[simp]

theorem CategoryTheory.yonedaGrp_map_app {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H : Grp C} (ψ : G ⟶ H) (Y : Cᵒᵖ) : (yonedaGrp.map ψ).app Y = GrpCat.ofHom (MonCat.Hom.hom ((yonedaMon.map ψ.hom).app Y))

@[simp]

theorem CategoryTheory.yonedaAddGrp_map_app {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H : AddGrp C} (ψ : G ⟶ H) (Y : Cᵒᵖ) : (yonedaAddGrp.map ψ).app Y = AddGrpCat.ofHom (AddMonCat.Hom.hom ((yonedaAddMon.map ψ.hom).app Y))

@[simp]

theorem CategoryTheory.yonedaGrp_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : Grp C) : yonedaGrp.obj G = yonedaGrpObj G.X

@[simp]

theorem CategoryTheory.yonedaAddGrp_obj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : AddGrp C) : yonedaAddGrp.obj G = yonedaAddGrpObj G.X

theorem CategoryTheory.yonedaGrp_naturality {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X Y : C} [GrpObj G] [GrpObj H] (α : yonedaGrpObj G ⟶ yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) : (ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryStruct.comp f g) = CategoryStruct.comp f ((ConcreteCategory.hom (α.app (Opposite.op Y))) g)

theorem CategoryTheory.yonedaAddGrp_naturality {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X Y : C} [AddGrpObj G] [AddGrpObj H] (α : yonedaAddGrpObj G ⟶ yonedaAddGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) : (ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryStruct.comp f g) = CategoryStruct.comp f ((ConcreteCategory.hom (α.app (Opposite.op Y))) g)

theorem CategoryTheory.yonedaGrp_naturality_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X Y : C} [GrpObj G] [GrpObj H] (α : yonedaGrpObj G ⟶ yonedaGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : H ⟶ Z) : CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryStruct.comp f g)) h = CategoryStruct.comp f (CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)

theorem CategoryTheory.yonedaAddGrp_naturality_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X Y : C} [AddGrpObj G] [AddGrpObj H] (α : yonedaAddGrpObj G ⟶ yonedaAddGrpObj H) (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : H ⟶ Z) : CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op X))) (CategoryStruct.comp f g)) h = CategoryStruct.comp f (CategoryStruct.comp ((ConcreteCategory.hom (α.app (Opposite.op Y))) g) h)

def CategoryTheory.yonedaGrpFullyFaithful {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaGrp.FullyFaithful

The yoneda embedding for Grp C is fully faithful.

Equations

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

def CategoryTheory.yonedaAddGrpFullyFaithful {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaAddGrp.FullyFaithful

The yoneda embedding for AddGrp C is fully faithful.

Equations

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

instance CategoryTheory.instFullGrpFunctorOppositeGrpCatYonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaGrp.Full

instance CategoryTheory.instFullAddGrpFunctorOppositeAddGrpCatYonedaAddGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaAddGrp.Full

instance CategoryTheory.instFaithfulGrpFunctorOppositeGrpCatYonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaGrp.Faithful

instance CategoryTheory.instFaithfulAddGrpFunctorOppositeAddGrpCatYonedaAddGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaAddGrp.Faithful

theorem CategoryTheory.essImage_yonedaGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaGrp.essImage = fun (F : Functor Cᵒᵖ GrpCat) => (F.comp (forget GrpCat)).IsRepresentable

theorem CategoryTheory.essImage_yonedaAddGrp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] : yonedaAddGrp.essImage = fun (F : Functor Cᵒᵖ AddGrpCat) => (F.comp (forget AddGrpCat)).IsRepresentable

theorem CategoryTheory.GrpObj.inv_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (g : G ⟶ H) [IsMonHom g] : CategoryStruct.comp f⁻¹ g = (CategoryStruct.comp f g)⁻¹

theorem CategoryTheory.AddGrpObj.neg_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [AddGrpObj G] [AddGrpObj H] (f : X ⟶ G) (g : G ⟶ H) [IsAddMonHom g] : CategoryStruct.comp (-f) g = -CategoryStruct.comp f g

theorem CategoryTheory.AddGrpObj.neg_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [AddGrpObj G] [AddGrpObj H] (f : X ⟶ G) (g : G ⟶ H) [IsAddMonHom g] {Z : C} (h : H ⟶ Z) : CategoryStruct.comp (-f) (CategoryStruct.comp g h) = CategoryStruct.comp (-CategoryStruct.comp f g) h

theorem CategoryTheory.GrpObj.inv_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (g : G ⟶ H) [IsMonHom g] {Z : C} (h : H ⟶ Z) : CategoryStruct.comp f⁻¹ (CategoryStruct.comp g h) = CategoryStruct.comp (CategoryStruct.comp f g)⁻¹ h

theorem CategoryTheory.GrpObj.div_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f g : X ⟶ G) (h : G ⟶ H) [IsMonHom h] : CategoryStruct.comp (f / g) h = CategoryStruct.comp f h / CategoryStruct.comp g h

theorem CategoryTheory.AddGrpObj.sub_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [AddGrpObj G] [AddGrpObj H] (f g : X ⟶ G) (h : G ⟶ H) [IsAddMonHom h] : CategoryStruct.comp (f - g) h = CategoryStruct.comp f h - CategoryStruct.comp g h

theorem CategoryTheory.GrpObj.div_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f g : X ⟶ G) (h : G ⟶ H) [IsMonHom h] {Z : C} (h✝ : H ⟶ Z) : CategoryStruct.comp (f / g) (CategoryStruct.comp h h✝) = CategoryStruct.comp (CategoryStruct.comp f h / CategoryStruct.comp g h) h✝

theorem CategoryTheory.AddGrpObj.sub_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [AddGrpObj G] [AddGrpObj H] (f g : X ⟶ G) (h : G ⟶ H) [IsAddMonHom h] {Z : C} (h✝ : H ⟶ Z) : CategoryStruct.comp (f - g) (CategoryStruct.comp h h✝) = CategoryStruct.comp (CategoryStruct.comp f h - CategoryStruct.comp g h) h✝

theorem CategoryTheory.GrpObj.zpow_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsMonHom g] : CategoryStruct.comp (f ^ n) g = CategoryStruct.comp f g ^ n

theorem CategoryTheory.AddGrpObj.zsmul_comp {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [AddGrpObj G] [AddGrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsAddMonHom g] : CategoryStruct.comp (n • f) g = n • CategoryStruct.comp f g

theorem CategoryTheory.AddGrpObj.zsmul_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [AddGrpObj G] [AddGrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsAddMonHom g] {Z : C} (h : H ⟶ Z) : CategoryStruct.comp (n • f) (CategoryStruct.comp g h) = CategoryStruct.comp (n • CategoryStruct.comp f g) h

theorem CategoryTheory.GrpObj.zpow_comp_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G H X : C} [GrpObj G] [GrpObj H] (f : X ⟶ G) (n : ℤ) (g : G ⟶ H) [IsMonHom g] {Z : C} (h : H ⟶ Z) : CategoryStruct.comp (f ^ n) (CategoryStruct.comp g h) = CategoryStruct.comp (CategoryStruct.comp f g ^ n) h

theorem CategoryTheory.GrpObj.comp_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) : CategoryStruct.comp f g⁻¹ = (CategoryStruct.comp f g)⁻¹

theorem CategoryTheory.AddGrpObj.comp_neg {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) : CategoryStruct.comp f (-g) = -CategoryStruct.comp f g

theorem CategoryTheory.AddGrpObj.comp_neg_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (-g) h) = CategoryStruct.comp (-CategoryStruct.comp f g) h

theorem CategoryTheory.GrpObj.comp_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp g⁻¹ h) = CategoryStruct.comp (CategoryStruct.comp f g)⁻¹ h

theorem CategoryTheory.GrpObj.comp_div {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) : CategoryStruct.comp f (g / h) = CategoryStruct.comp f g / CategoryStruct.comp f h

theorem CategoryTheory.AddGrpObj.comp_sub {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [AddGrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) : CategoryStruct.comp f (g - h) = CategoryStruct.comp f g - CategoryStruct.comp f h

theorem CategoryTheory.GrpObj.comp_div_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) {Z : C} (h✝ : G ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (g / h) h✝) = CategoryStruct.comp (CategoryStruct.comp f g / CategoryStruct.comp f h) h✝

theorem CategoryTheory.AddGrpObj.comp_sub_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [AddGrpObj G] (f : X ⟶ Y) (g h : Y ⟶ G) {Z : C} (h✝ : G ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (g - h) h✝) = CategoryStruct.comp (CategoryStruct.comp f g - CategoryStruct.comp f h) h✝

theorem CategoryTheory.GrpObj.comp_zpow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) : CategoryStruct.comp f (g ^ n) = CategoryStruct.comp f g ^ n

theorem CategoryTheory.AddGrpObj.comp_zsmul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) : CategoryStruct.comp f (n • g) = n • CategoryStruct.comp f g

theorem CategoryTheory.GrpObj.comp_zpow_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [GrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (g ^ n) h) = CategoryStruct.comp (CategoryStruct.comp f g ^ n) h

theorem CategoryTheory.AddGrpObj.comp_zsmul_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X Y : C} [AddGrpObj G] (f : X ⟶ Y) (g : Y ⟶ G) (n : ℤ) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp f (CategoryStruct.comp (n • g) h) = CategoryStruct.comp (n • CategoryStruct.comp f g) h

theorem CategoryTheory.GrpObj.inv_eq_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] : inv = (CategoryStruct.id G)⁻¹

theorem CategoryTheory.AddGrpObj.neg_eq_neg {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] : neg = -CategoryStruct.id G

@[simp]

theorem CategoryTheory.GrpObj.one_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] : CategoryStruct.comp MonObj.one inv = MonObj.one

@[simp]

theorem CategoryTheory.AddGrpObj.zero_neg {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] : CategoryStruct.comp AddMonObj.zero neg = AddMonObj.zero

@[simp]

theorem CategoryTheory.AddGrpObj.zero_neg_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] {Z : C} (h : G ⟶ Z) : CategoryStruct.comp AddMonObj.zero (CategoryStruct.comp neg h) = CategoryStruct.comp AddMonObj.zero h

@[simp]

theorem CategoryTheory.GrpObj.one_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] {Z : C} (h : G ⟶ Z) : CategoryStruct.comp MonObj.one (CategoryStruct.comp inv h) = CategoryStruct.comp MonObj.one h

@[simp]

theorem CategoryTheory.Functor.map_inv' {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u_1} [Category.{v_1, u_1} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] {X G : C} (f : X ⟶ G) [GrpObj G] : F.map f⁻¹ = (F.map f)⁻¹

If G is a group object and F is monoidal, then Hom(X, G) → Hom(F X, F G) preserves inverses.

@[simp]

theorem CategoryTheory.Functor.map_neg' {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {D : Type u_1} [Category.{v_1, u_1} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] {X G : C} (f : X ⟶ G) [AddGrpObj G] : F.map (-f) = -F.map f

def CategoryTheory.GrpObj.conj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] : MonoidalCategoryStruct.tensorObj G G ⟶ G

Conjugation in G as a morphism. This is the map (x, y) ↦ x * y * x⁻¹, see CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv.

Equations

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

def CategoryTheory.AddGrpObj.addConj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [AddGrpObj G] : MonoidalCategoryStruct.tensorObj G G ⟶ G

Conjugation in G as a morphism. This is the map (x, y) ↦ x + y + (-x), see CategoryTheory.AddGrpObj.lift_conj_eq_add_add_neg.

Equations

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

@[simp]

theorem CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [GrpObj G] (f₁ f₂ : X ⟶ G) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (conj G) = f₁ * f₂ * f₁⁻¹

@[simp]

theorem CategoryTheory.AddGrpObj.lift_addConj_eq_add_add_neg {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [AddGrpObj G] (f₁ f₂ : X ⟶ G) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (addConj G) = f₁ + f₂ + -f₁

@[simp]

theorem CategoryTheory.AddGrpObj.lift_addConj_eq_add_add_neg_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [AddGrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (CategoryStruct.comp (addConj G) h) = CategoryStruct.comp (f₁ + f₂ + -f₁) h

@[simp]

theorem CategoryTheory.GrpObj.lift_conj_eq_mul_mul_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [GrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (CategoryStruct.comp (conj G) h) = CategoryStruct.comp (f₁ * f₂ * f₁⁻¹) h

def CategoryTheory.GrpObj.commutator {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [GrpObj G] : MonoidalCategoryStruct.tensorObj G G ⟶ G

The commutator of G as a morphism. This is the map (x, y) ↦ x * y * x⁻¹ * y⁻¹, see CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv. This morphism is constant with value 1 if and only if G is commutative (see CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η).

Equations

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

def CategoryTheory.AddGrpObj.addCommutator {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] (G : C) [AddGrpObj G] : MonoidalCategoryStruct.tensorObj G G ⟶ G

The commutator of G as a morphism. This is the map (x, y) ↦ x + y + (-x) + (-y), see CategoryTheory.AddGrpObj.lift_commutator_eq_add_add_neg_neg. This morphism is constant with value 0 if and only if G is commutative (see CategoryTheory.isCommAddMonObj_iff_commutator_eq_toAddUnit_η).

Equations

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

@[simp]

theorem CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [GrpObj G] (f₁ f₂ : X ⟶ G) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (commutator G) = f₁ * f₂ * f₁⁻¹ * f₂⁻¹

@[simp]

theorem CategoryTheory.AddGrpObj.lift_addCommutator_eq_add_add_neg_neg {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [AddGrpObj G] (f₁ f₂ : X ⟶ G) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (addCommutator G) = f₁ + f₂ + -f₁ + -f₂

@[simp]

theorem CategoryTheory.GrpObj.lift_commutator_eq_mul_mul_inv_inv_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [GrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (CategoryStruct.comp (commutator G) h) = CategoryStruct.comp (f₁ * f₂ * f₁⁻¹ * f₂⁻¹) h

@[simp]

theorem CategoryTheory.AddGrpObj.lift_addCommutator_eq_add_add_neg_neg_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {X G : C} [AddGrpObj G] (f₁ f₂ : X ⟶ G) {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (CartesianMonoidalCategory.lift f₁ f₂) (CategoryStruct.comp (addCommutator G) h) = CategoryStruct.comp (f₁ + f₂ + -f₁ + -f₂) h

@[simp]

theorem CategoryTheory.GrpObj.η_whiskerRight_commutator {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.one G) (commutator G) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) G)) MonObj.one

@[simp]

theorem CategoryTheory.AddGrpObj.η_whiskerRight_addCommutator {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.zero G) (addCommutator G) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) G)) AddMonObj.zero

@[simp]

theorem CategoryTheory.GrpObj.η_whiskerRight_commutator_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight MonObj.one G) (CategoryStruct.comp (commutator G) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) G)) (CategoryStruct.comp MonObj.one h)

@[simp]

theorem CategoryTheory.AddGrpObj.η_whiskerRight_addCommutator_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerRight AddMonObj.zero G) (CategoryStruct.comp (addCommutator G) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj (MonoidalCategoryStruct.tensorUnit C) G)) (CategoryStruct.comp AddMonObj.zero h)

@[simp]

theorem CategoryTheory.GrpObj.whiskerLeft_η_commutator {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G MonObj.one) (commutator G) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj G (MonoidalCategoryStruct.tensorUnit C))) MonObj.one

@[simp]

theorem CategoryTheory.AddGrpObj.whiskerLeft_η_addCommutator {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G AddMonObj.zero) (addCommutator G) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj G (MonoidalCategoryStruct.tensorUnit C))) AddMonObj.zero

@[simp]

theorem CategoryTheory.AddGrpObj.whiskerLeft_η_addCommutator_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G AddMonObj.zero) (CategoryStruct.comp (addCommutator G) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj G (MonoidalCategoryStruct.tensorUnit C))) (CategoryStruct.comp AddMonObj.zero h)

@[simp]

theorem CategoryTheory.GrpObj.whiskerLeft_η_commutator_assoc {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] {Z : C} (h : G ⟶ Z) : CategoryStruct.comp (MonoidalCategoryStruct.whiskerLeft G MonObj.one) (CategoryStruct.comp (commutator G) h) = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj G (MonoidalCategoryStruct.tensorUnit C))) (CategoryStruct.comp MonObj.one h)

instance CategoryTheory.instIsMonHomInvOfIsCommMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] [BraidedCategory C] [IsCommMonObj G] : IsMonHom GrpObj.inv

instance CategoryTheory.instIsAddMonHomNegOfIsCommAddMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] [BraidedCategory C] [IsCommAddMonObj G] : IsAddMonHom AddGrpObj.neg

instance CategoryTheory.instIsMonHomInvHomOfIsCommMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M G : C} [MonObj M] [GrpObj G] [BraidedCategory C] [IsCommMonObj G] {f : M ⟶ G} [IsMonHom f] : IsMonHom f⁻¹

instance CategoryTheory.instIsAddMonHomNegHomOfIsCommAddMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {M G : C} [AddMonObj M] [AddGrpObj G] [BraidedCategory C] [IsCommAddMonObj G] {f : M ⟶ G} [IsAddMonHom f] : IsAddMonHom (-f)

@[implicit_reducible]

instance CategoryTheory.Grp.instMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : Grp C} [IsCommMonObj H.X] : MonObj H

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddGrp.instAddMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : AddGrp C} [IsCommAddMonObj H.X] : AddMonObj H

Equations

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

@[simp]

theorem CategoryTheory.Grp.hom_one {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (H : Grp C) [IsCommMonObj H.X] : MonObj.one.hom.hom = MonObj.one

@[simp]

theorem CategoryTheory.AddGrp.hom_zero {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (H : AddGrp C) [IsCommAddMonObj H.X] : AddMonObj.zero.hom.hom = AddMonObj.zero

@[simp]

theorem CategoryTheory.Grp.hom_mul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (H : Grp C) [IsCommMonObj H.X] : MonObj.mul.hom.hom = MonObj.mul

@[simp]

theorem CategoryTheory.AddGrp.hom_add {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] (H : AddGrp C) [IsCommAddMonObj H.X] : AddMonObj.add.hom.hom = AddMonObj.add

@[simp]

theorem CategoryTheory.Grp.Hom.hom_one {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] : InducedCategory.Hom.hom 1 = 1

@[simp]

theorem CategoryTheory.AddGrp.Hom.hom_zero {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} [IsCommAddMonObj H.X] : InducedCategory.Hom.hom 0 = 0

@[simp]

theorem CategoryTheory.Grp.Hom.hom_mul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f g : G ⟶ H) : (f * g).hom = f.hom * g.hom

@[simp]

theorem CategoryTheory.AddGrp.Hom.hom_add {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} [IsCommAddMonObj H.X] (f g : G ⟶ H) : (f + g).hom = f.hom + g.hom

@[simp]

theorem CategoryTheory.Grp.Hom.hom_pow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) (n : ℕ) : (f ^ n).hom = f.hom ^ n

@[simp]

theorem CategoryTheory.AddGrp.Hom.hom_nsmul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} [IsCommAddMonObj H.X] (f : G ⟶ H) (n : ℕ) : (n • f).hom = n • f.hom

@[implicit_reducible]

instance CategoryTheory.Grp.instGrpObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : Grp C} [IsCommMonObj H.X] : GrpObj H

A commutative group object is a group object in the category of group objects.

Equations

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

@[implicit_reducible]

instance CategoryTheory.AddGrp.instAddGrpObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : AddGrp C} [IsCommAddMonObj H.X] : AddGrpObj H

Equations

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

@[simp]

theorem CategoryTheory.Grp.Hom.hom_hom_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) : f⁻¹.hom.hom = f.hom.hom⁻¹

@[simp]

theorem CategoryTheory.AddGrp.Hom.hom_hom_neg {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} [IsCommAddMonObj H.X] (f : G ⟶ H) : (-f).hom.hom = -f.hom.hom

@[simp]

theorem CategoryTheory.Grp.Hom.hom_hom_div {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f g : G ⟶ H) : (f / g).hom.hom = f.hom.hom / g.hom.hom

@[simp]

theorem CategoryTheory.AddGrp.Hom.hom_hom_sub {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} [IsCommAddMonObj H.X] (f g : G ⟶ H) : (f - g).hom.hom = f.hom.hom - g.hom.hom

@[simp]

theorem CategoryTheory.Grp.Hom.hom_hom_zpow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) (n : ℤ) : (f ^ n).hom.hom = f.hom.hom ^ n

@[simp]

theorem CategoryTheory.AddGrp.Hom.hom_hom_zsmul {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} [IsCommAddMonObj H.X] (f : G ⟶ H) (n : ℤ) : (n • f).hom.hom = n • f.hom.hom

@[deprecated CategoryTheory.Grp.Hom.hom_hom_inv (since := "2025-12-18")]

theorem CategoryTheory.Grp.Hom.hom_inv {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) : f⁻¹.hom.hom = f.hom.hom⁻¹

Alias of CategoryTheory.Grp.Hom.hom_hom_inv.

@[deprecated CategoryTheory.Grp.Hom.hom_hom_div (since := "2025-12-18")]

theorem CategoryTheory.Grp.Hom.hom_div {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f g : G ⟶ H) : (f / g).hom.hom = f.hom.hom / g.hom.hom

Alias of CategoryTheory.Grp.Hom.hom_hom_div.

@[deprecated CategoryTheory.Grp.Hom.hom_hom_zpow (since := "2025-12-18")]

theorem CategoryTheory.Grp.Hom.hom_zpow {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] (f : G ⟶ H) (n : ℤ) : (f ^ n).hom.hom = f.hom.hom ^ n

Alias of CategoryTheory.Grp.Hom.hom_hom_zpow.

instance CategoryTheory.Grp.instIsCommMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : Grp C} [IsCommMonObj H.X] : IsCommMonObj H

A commutative group object is a commutative group object in the category of group objects.

instance CategoryTheory.AddGrp.instIsCommAddMonObj {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {H : AddGrp C} [IsCommAddMonObj H.X] : IsCommAddMonObj H

instance CategoryTheory.Grp.instIsMonHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : Grp C} [IsCommMonObj H.X] [IsCommMonObj G.X] (f : G ⟶ H) : IsMonHom f

instance CategoryTheory.AddGrp.instIsAddMonHom {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] [BraidedCategory C] {G H : AddGrp C} [IsCommAddMonObj H.X] [IsCommAddMonObj G.X] (f : G ⟶ H) : IsAddMonHom f

@[reducible, inline]

abbrev CategoryTheory.Hom.commGroup {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [GrpObj G] [BraidedCategory C] [IsCommMonObj G] : CommGroup (X ⟶ G)

If G is a commutative group object, then Hom(X, G) has a commutative group structure.

Equations

• CategoryTheory.Hom.commGroup = { toGroup := CategoryTheory.Hom.group, mul_comm := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.Hom.addCommGroup {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G X : C} [AddGrpObj G] [BraidedCategory C] [IsCommAddMonObj G] : AddCommGroup (X ⟶ G)

If G is a commutative additive group object, then Hom(X, G) has a commutative additive group structure.

Equations

• CategoryTheory.Hom.addCommGroup = { toAddGroup := CategoryTheory.Hom.addGroup, add_comm := ⋯ }

theorem CategoryTheory.isCommMonObj_iff_commutator_eq_toUnit_η {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [GrpObj G] [BraidedCategory C] : IsCommMonObj G ↔ GrpObj.commutator G = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj G G)) MonObj.one

G is a commutative group object if and only if the commutator map (x, y) ↦ x * y * x⁻¹ * y⁻¹ is constant.

theorem CategoryTheory.isCommAddMonObj_iff_addCommutator_eq_toAddUnit_η {C : Type u} [Category.{v, u} C] [CartesianMonoidalCategory C] {G : C} [AddGrpObj G] [BraidedCategory C] : IsCommAddMonObj G ↔ AddGrpObj.addCommutator G = CategoryStruct.comp (SemiCartesianMonoidalCategory.toUnit (MonoidalCategoryStruct.tensorObj G G)) AddMonObj.zero