The category of commutative groups in a Cartesian monoidal category

structure CommGrp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : Type (max u₁ v₁)

A commutative group object internal to a Cartesian monoidal category.

• X : C

  The underlying object in the ambient monoidal category

• grp : GrpObj self.X
• comm : IsCommMonObj self.X

@[deprecated CommGrp (since := "2025-10-13")]

def CommGrp_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : Type (max u₁ v₁)

Alias of CommGrp.

---

A commutative group object internal to a Cartesian monoidal category.

Equations

• CommGrp_ = CommGrp

def CommGrp.toGrp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : Grp C

A commutative group object is a group object.

Equations

• A.toGrp = { X := A.X, grp := A.grp }

@[simp]

theorem CommGrp.toGrp_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : A.toGrp.X = A.X

@[deprecated CommGrp.toGrp (since := "2025-10-13")]

def CommGrp.toGrp_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : Grp C

Alias of CommGrp.toGrp.

---

A commutative group object is a group object.

Equations

• @CommGrp.toGrp_ = @CommGrp.toGrp

def CommGrp.toCommMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : CommMon C

A commutative group object is a commutative monoid object.

Equations

• A.toCommMon = { X := A.X, mon := A.grp.toMonObj, comm := ⋯ }

@[simp]

theorem CommGrp.toCommMon_X {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : A.toCommMon.X = A.X

@[deprecated CommGrp.toCommMon (since := "2025-09-15")]

def CommGrp.toCommMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : CommMon C

Alias of CommGrp.toCommMon.

---

A commutative group object is a commutative monoid object.

Equations

• @CommGrp.toCommMon_ = @CommGrp.toCommMon

@[reducible, inline]

abbrev CommGrp.toMon {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : Mon C

A commutative group object is a monoid object.

Equations

• A.toMon = A.toCommMon.toMon

@[deprecated CommGrp.toMon (since := "2025-09-15")]

def CommGrp.toMon_ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : Mon C

Alias of CommGrp.toMon.

---

A commutative group object is a monoid object.

Equations

• @CommGrp.toMon_ = @CommGrp.toMon

def CommGrp.trivial (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CommGrp C

The trivial commutative group object.

Equations

• CommGrp.trivial C = { X := CategoryTheory.MonoidalCategoryStruct.tensorUnit C, grp := GrpObj.instTensorUnit, comm := ⋯ }

@[simp]

theorem CommGrp.trivial_grp_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : MonObj.one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem CommGrp.trivial_grp_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : MonObj.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom

@[simp]

theorem CommGrp.trivial_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C

@[simp]

theorem CommGrp.trivial_grp_inv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : GrpObj.inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

instance CommGrp.instInhabited {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : Inhabited (CommGrp C)

Equations

• CommGrp.instInhabited = { default := CommGrp.trivial C }

instance CommGrp.instCategory {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Category.{v₁, max u₁ v₁} (CommGrp C)

Equations

• CommGrp.instCategory = CategoryTheory.InducedCategory.category CommGrp.toGrp

@[simp]

theorem CommGrp.id_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp C) : (CategoryTheory.CategoryStruct.id A).hom = CategoryTheory.CategoryStruct.id A.X

@[simp]

theorem CommGrp.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {R S T : CommGrp C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

theorem CommGrp.hom_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommGrp C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g

theorem CommGrp.hom_ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommGrp C} {f g : A ⟶ B} : f = g ↔ f.hom = g.hom

@[simp]

theorem CommGrp.id' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : CategoryTheory.CategoryStruct.id A = CategoryTheory.CategoryStruct.id A.toMon

@[simp]

theorem CommGrp.comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A₁ A₂ A₃ : CommGrp C} (f : A₁ ⟶ A₂) (g : A₂ ⟶ A₃) : CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp f g

def CommGrp.forget₂Grp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (CommGrp C) (Grp C)

The forgetful functor from commutative group objects to group objects.

Equations

• CommGrp.forget₂Grp C = CategoryTheory.inducedFunctor CommGrp.toGrp

@[simp]

theorem CommGrp.forget₂Grp_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : ((forget₂Grp C).obj A).X = A.X

@[deprecated CommGrp.forget₂Grp (since := "2025-10-13")]

def CommGrp.forget₂Grp_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (CommGrp C) (Grp C)

Alias of CommGrp.forget₂Grp.

---

The forgetful functor from commutative group objects to group objects.

Equations

• CommGrp.forget₂Grp_ = CommGrp.forget₂Grp

def CommGrp.fullyFaithfulForget₂Grp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂Grp C).FullyFaithful

The forgetful functor from commutative group objects to group objects is fully faithful.

Equations

• CommGrp.fullyFaithfulForget₂Grp C = CategoryTheory.fullyFaithfulInducedFunctor CommGrp.toGrp

@[deprecated CommGrp.fullyFaithfulForget₂Grp (since := "2025-10-13")]

def CommGrp.fullyFaithfulForget₂Grp_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂Grp C).FullyFaithful

Alias of CommGrp.fullyFaithfulForget₂Grp.

---

The forgetful functor from commutative group objects to group objects is fully faithful.

Equations

• CommGrp.fullyFaithfulForget₂Grp_ = CommGrp.fullyFaithfulForget₂Grp

instance CommGrp.instFullGrpForget₂Grp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂Grp C).Full

instance CommGrp.instFaithfulGrpForget₂Grp (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂Grp C).Faithful

@[simp]

theorem CommGrp.forget₂Grp_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : MonObj.one = MonObj.one

@[simp]

theorem CommGrp.forget₂Grp_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : MonObj.mul = MonObj.mul

@[simp]

theorem CommGrp.forget₂Grp_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommGrp C} (f : A ⟶ B) : ((forget₂Grp C).map f).hom = f.hom

def CommGrp.forget₂CommMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (CommGrp C) (CommMon C)

The forgetful functor from commutative group objects to commutative monoid objects.

Equations

• CommGrp.forget₂CommMon C = CategoryTheory.inducedFunctor CommGrp.toCommMon

@[simp]

theorem CommGrp.forget₂CommMon_obj_X (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : ((forget₂CommMon C).obj A).X = A.X

@[deprecated CommGrp.forget₂CommMon (since := "2025-09-15")]

def CommGrp.forget₂CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (CommGrp C) (CommMon C)

Alias of CommGrp.forget₂CommMon.

---

The forgetful functor from commutative group objects to commutative monoid objects.

Equations

• CommGrp.forget₂CommMon_ = CommGrp.forget₂CommMon

def CommGrp.fullyFaithfulForget₂CommMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂CommMon C).FullyFaithful

The forgetful functor from commutative group objects to commutative monoid objects is fully faithful.

Equations

• CommGrp.fullyFaithfulForget₂CommMon C = CategoryTheory.fullyFaithfulInducedFunctor CommGrp.toCommMon

@[deprecated CommGrp.fullyFaithfulForget₂CommMon (since := "2025-09-15")]

def CommGrp.fullyFaithfulForget₂CommMon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂CommMon C).FullyFaithful

Alias of CommGrp.fullyFaithfulForget₂CommMon.

---

The forgetful functor from commutative group objects to commutative monoid objects is fully faithful.

Equations

• CommGrp.fullyFaithfulForget₂CommMon_ = CommGrp.fullyFaithfulForget₂CommMon

instance CommGrp.instFullCommMonForget₂CommMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂CommMon C).Full

instance CommGrp.instFaithfulCommMonForget₂CommMon (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂CommMon C).Faithful

@[simp]

theorem CommGrp.forget₂CommMon_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : MonObj.one = MonObj.one

@[simp]

theorem CommGrp.forget₂CommMon_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : MonObj.mul = MonObj.mul

@[simp]

theorem CommGrp.forget₂CommMon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {A B : CommGrp C} (f : A ⟶ B) : ((forget₂CommMon C).map f).hom = f.hom

def CommGrp.forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor (CommGrp C) C

The forgetful functor from commutative group objects to the ambient category.

Equations

• CommGrp.forget C = (CommGrp.forget₂Grp C).comp (Grp.forget C)

@[simp]

theorem CommGrp.forget_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {X✝ Y✝ : CommGrp C} (f : X✝ ⟶ Y✝) : (forget C).map f = f.hom

@[simp]

theorem CommGrp.forget_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : CommGrp C) : (forget C).obj X = X.X

instance CommGrp.instFaithfulForget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget C).Faithful

@[simp]

theorem CommGrp.forget₂Grp_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂Grp C).comp (Grp.forget C) = forget C

@[simp]

theorem CommGrp.forget₂CommMon_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : (forget₂CommMon C).comp (CommMon.forget C) = forget C

instance CommGrp.instIsIsoHom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CommGrp C} {f : G ⟶ H} [CategoryTheory.IsIso f] : CategoryTheory.IsIso f.hom

def CommGrp.mkIso' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [IsCommMonObj G] [GrpObj H] [IsCommMonObj H] [IsMonHom e.hom] : { X := G, grp := inst✝, comm := inst✝¹ } ≅ { X := H, grp := inst✝², comm := inst✝³ }

Construct an isomorphism of commutative group objects by giving a monoid isomorphism between the underlying objects.

Equations

• CommGrp.mkIso' e = (CommGrp.fullyFaithfulForget₂Grp C).preimageIso (Grp.mkIso' e)

@[simp]

theorem CommGrp.mkIso'_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [IsCommMonObj G] [GrpObj H] [IsCommMonObj H] [IsMonHom e.hom] : (mkIso' e).hom.hom = e.hom

@[simp]

theorem CommGrp.mkIso'_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : C} (e : G ≅ H) [GrpObj G] [IsCommMonObj G] [GrpObj H] [IsCommMonObj H] [IsMonHom e.hom] : (mkIso' e).inv.hom = e.inv

@[reducible, inline]

abbrev CommGrp.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CommGrp C} (e : G.X ≅ H.X) (one_f : CategoryTheory.CategoryStruct.comp MonObj.one e.hom = MonObj.one := by cat_disch) (mul_f : CategoryTheory.CategoryStruct.comp MonObj.mul e.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom) MonObj.mul := by cat_disch) : G ≅ H

Construct an isomorphism of group objects by giving an isomorphism between the underlying objects and checking compatibility with unit and multiplication only in the forward direction.

Equations

• CommGrp.mkIso e one_f mul_f = CommGrp.mkIso' e

instance CommGrp.uniqueHomFromTrivial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : CommGrp C) : Unique (trivial C ⟶ A)

Equations

• A.uniqueHomFromTrivial = A.toMon.uniqueHomFromTrivial

instance CommGrp.instHasInitial {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Limits.HasInitial (CommGrp C)

def CategoryTheory.Functor.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] : Functor (CommGrp C) (CommGrp D)

A finite-product-preserving functor takes commutative group objects to commutative group objects.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_grp_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) : MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map MonObj.mul)

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] {X✝ Y✝ : CommGrp C} (f : X✝ ⟶ Y✝) : (F.mapCommGrp.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) : (F.mapCommGrp.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_grp_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) : MonObj.one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map MonObj.one)

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_obj_grp_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : Functor C D) [F.Braided] (A : CommGrp C) : GrpObj.inv = F.map GrpObj.inv

instance CategoryTheory.Functor.Faithful.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] [F.Faithful] : F.mapCommGrp.Faithful

instance CategoryTheory.Functor.Full.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] [F.Full] [F.Faithful] : F.mapCommGrp.Full

def CategoryTheory.Functor.FullyFaithful.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) : F.mapGrp.FullyFaithful

If F : C ⥤ D is a fully faithful monoidal functor, then CommGrpCat(F) : CommGrpCat C ⥤ CommGrpCat D is fully faithful too.

Equations

• hF.mapCommGrp = { preimage := fun {X Y : Grp C} (f : F.mapGrp.obj X ⟶ F.mapGrp.obj Y) => { hom := hF.preimage f.hom, isMonHom_hom := ⋯ }, map_preimage := ⋯, preimage_map := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.mapCommGrp_preimage_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} [F.Braided] (hF : F.FullyFaithful) {X✝ Y✝ : Grp C} (f : F.mapGrp.obj X✝ ⟶ F.mapGrp.obj Y✝) : (hF.mapCommGrp.preimage f).hom = hF.preimage f.hom

@[simp]

theorem CategoryTheory.Functor.mapCommGrp_id_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) : MonObj.one = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorUnit C)) MonObj.one

@[simp]

theorem CategoryTheory.Functor.mapCommpGrp_id_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (A : CommGrp C) : MonObj.mul = CategoryStruct.comp (CategoryStruct.id (MonoidalCategoryStruct.tensorObj A.X A.X)) MonObj.mul

@[simp]

theorem CategoryTheory.Functor.comp_mapCommGrp_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (A : CommGrp C) : MonObj.one = CategoryStruct.comp (LaxMonoidal.ε (F.comp G)) ((F.comp G).map MonObj.one)

@[simp]

theorem CategoryTheory.Functor.comp_mapCommGrp_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (A : CommGrp C) : MonObj.mul = CategoryStruct.comp (LaxMonoidal.μ (F.comp G) A.X A.X) ((F.comp G).map MonObj.mul)

def CategoryTheory.Functor.mapCommGrpIdIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] : (Functor.id C).mapCommGrp ≅ Functor.id (CommGrp C)

The identity functor is also the identity on commutative group objects.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapCommGrpIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) : (mapCommGrpIdIso.inv.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Functor.mapCommGrpIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] (X : CommGrp C) : (mapCommGrpIdIso.hom.app X).hom = CategoryStruct.id X.X

def CategoryTheory.Functor.mapCommGrpCompIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] : (F.comp G).mapCommGrp ≅ F.mapCommGrp.comp G.mapCommGrp

The composition functor is also the composition on commutative group objects.

Equations

• CategoryTheory.Functor.mapCommGrpCompIso = CategoryTheory.NatIso.ofComponents (fun (X : CommGrp C) => CommGrp.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapCommGrp.obj X).X) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.mapCommGrpCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (X : CommGrp C) : (mapCommGrpCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

@[simp]

theorem CategoryTheory.Functor.mapCommGrpCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] [BraidedCategory E] {F : Functor C D} [F.Braided] {G : Functor D E} [G.Braided] (X : CommGrp C) : (mapCommGrpCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

def CategoryTheory.Functor.mapCommGrpNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (f : F ⟶ F') : F.mapCommGrp ⟶ F'.mapCommGrp

Natural transformations between functors lift to commutative group objects.

Equations

• CategoryTheory.Functor.mapCommGrpNatTrans f = { app := fun (X : CommGrp C) => Mon.Hom.mk' (f.app X.toGrp.X) ⋯ ⋯, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapCommGrpNatTrans_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (f : F ⟶ F') (X : CommGrp C) : ((mapCommGrpNatTrans f).app X).hom = f.app X.X

def CategoryTheory.Functor.mapCommGrpNatIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') : F.mapCommGrp ≅ F'.mapCommGrp

Natural isomorphisms between functors lift to commutative group objects.

Equations

• CategoryTheory.Functor.mapCommGrpNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : CommGrp C) => CommGrp.mkIso (e.app X.toGrp.X) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.mapCommGrpNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') (X : CommGrp C) : ((mapCommGrpNatIso e).inv.app X).hom = e.inv.app X.X

@[simp]

theorem CategoryTheory.Functor.mapCommGrpNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F F' : Functor C D} [F.Braided] [F'.Braided] (e : F ≅ F') (X : CommGrp C) : ((mapCommGrpNatIso e).hom.app X).hom = e.hom.app X.X

noncomputable def CategoryTheory.Functor.mapCommGrpFunctor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] : Functor (C ⥤ₗ D) (Functor (CommGrp C) (CommGrp D))

mapCommGrp is functorial in the left-exact functor.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapCommGrpFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (F : C ⥤ₗ D) : mapCommGrpFunctor.obj F = F.obj.mapCommGrp

@[simp]

theorem CategoryTheory.Functor.mapCommGrpFunctor_map_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F G : C ⥤ₗ D} (α : F ⟶ G) (A : CommGrp C) : ((mapCommGrpFunctor.map α).app A).hom = α.app A.X

noncomputable def CategoryTheory.Adjunction.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] : F.mapCommGrp ⊣ G.mapCommGrp

An adjunction of braided functors lifts to an adjunction of their lifts to commutative group objects.

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.mapCommGrp_counit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] : a.mapCommGrp.counit = CategoryStruct.comp Functor.mapCommGrpCompIso.inv (CategoryStruct.comp (Functor.mapCommGrpNatTrans a.counit) Functor.mapCommGrpIdIso.hom)

@[simp]

theorem CategoryTheory.Adjunction.mapCommGrp_unit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Braided] [G.Braided] : a.mapCommGrp.unit = CategoryStruct.comp Functor.mapCommGrpIdIso.inv (CategoryStruct.comp (Functor.mapCommGrpNatTrans a.unit) Functor.mapCommGrpCompIso.hom)

noncomputable def CategoryTheory.Equivalence.mapCommGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] : CommGrp C ≌ CommGrp D

An equivalence of categories lifts to an equivalence of their commutative group objects.

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_inverse {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] : e.mapCommGrp.inverse = e.inverse.mapCommGrp

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] : e.mapCommGrp.counitIso = Functor.mapCommGrpCompIso.symm ≪≫ Functor.mapCommGrpNatIso e.counitIso ≪≫ Functor.mapCommGrpIdIso

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_functor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] : e.mapCommGrp.functor = e.functor.mapCommGrp

@[simp]

theorem CategoryTheory.Equivalence.mapCommGrp_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] [BraidedCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] [BraidedCategory D] (e : C ≌ D) [e.functor.Braided] [e.inverse.Braided] : e.mapCommGrp.unitIso = Functor.mapCommGrpIdIso.symm ≪≫ Functor.mapCommGrpNatIso e.unitIso ≪≫ Functor.mapCommGrpCompIso