The category of groups in a cartesian monoidal category

We define group objects in cartesian monoidal categories.

We show that the associativity diagram of a group object is always cartesian and deduce that morphisms of group objects commute with taking inverses.

We show that a finite-product-preserving functor takes group objects to group objects.

class Grp_Class {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) extends Mon_Class X : Type v₁

A group object internal to a cartesian monoidal category. Also see the bundled Grp_.

• 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

  The inverse in a group object

• 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

def Mon_Class.termι : Lean.ParserDescr

The inverse in a group object

Equations

• Mon_Class.termι = Lean.ParserDescr.node `Mon_Class.termι 1024 (Lean.ParserDescr.symbol "ι")

def Mon_Class.«termι[_]» : Lean.ParserDescr

The inverse in a group object

Equations

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

@[simp]

theorem Grp_Class.left_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) [Grp_Class X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X)) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) Mon_Class.one

@[simp]

theorem Grp_Class.left_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) [Grp_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift inv (CategoryTheory.CategoryStruct.id X)) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) (CategoryTheory.CategoryStruct.comp Mon_Class.one h)

@[simp]

theorem Grp_Class.right_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) [Grp_Class X] : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv) Mon_Class.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) Mon_Class.one

@[simp]

theorem Grp_Class.right_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) [Grp_Class X] {Z : C} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) inv) (CategoryTheory.CategoryStruct.comp Mon_Class.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit X) (CategoryTheory.CategoryStruct.comp Mon_Class.one h)

structure Grp_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] extends Mon_ C : Type (max u₁ v₁)

A group object in a cartesian monoidal category.

• X : C
• one : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ self.X
• mul : CategoryTheory.MonoidalCategoryStruct.tensorObj self.X self.X ⟶ self.X
• one_mul : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.one self.X) self.mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor self.X).hom
• mul_one : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X self.one) self.mul = (CategoryTheory.MonoidalCategoryStruct.rightUnitor self.X).hom
• mul_assoc : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight self.mul self.X) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator self.X self.X self.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X self.mul) self.mul)
• inv : self.X ⟶ self.X

  The inversion operation

• left_inv : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift self.inv (CategoryTheory.CategoryStruct.id self.X)) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit self.X) self.one
• right_inv : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id self.X) self.inv) self.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit self.X) self.one

@[simp]

theorem Grp_.left_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (self : Grp_ C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift self.inv (CategoryTheory.CategoryStruct.id self.X)) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit self.X) (CategoryTheory.CategoryStruct.comp self.one h)

@[simp]

theorem Grp_.right_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (self : Grp_ C) {Z : C} (h : self.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id self.X) self.inv) (CategoryTheory.CategoryStruct.comp self.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit self.X) (CategoryTheory.CategoryStruct.comp self.one h)

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

The trivial group object.

Equations

• Grp_.trivial C = { toMon_ := Mon_.trivial C, inv := CategoryTheory.CategoryStruct.id (Mon_.trivial C).X, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Grp_.trivial_inv (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (trivial C).inv = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

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

@[simp]

theorem Grp_.trivial_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (trivial C).one = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)

@[simp]

theorem Grp_.trivial_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (trivial C).mul = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom

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

Equations

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

def Grp_.mk' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : C) [Grp_Class X] : Grp_ C

Make a group object from Grp_Class.

Equations

• Grp_.mk' X = { toMon_ := Mon_.mk' X, inv := Grp_Class.inv, left_inv := ⋯, right_inv := ⋯ }

instance Grp_.instGrp_ClassX {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (X : Grp_ C) : Grp_Class X.X

Equations

• X.instGrp_ClassX = { toMon_Class := Mon_.instMon_ClassX, inv := X.inv, left_inv' := ⋯, right_inv' := ⋯ }

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

Equations

• Grp_.instCategory = CategoryTheory.InducedCategory.category Grp_.toMon_

@[simp]

theorem Grp_.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 Grp_.comp_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {R S T : Grp_ C} (f : R ⟶ S) (g : S ⟶ T) : (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem Grp_.lift_comp_inv_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f : A ⟶ B.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f B.inv)) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A) B.one

@[simp]

theorem Grp_.lift_comp_inv_right_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f : A ⟶ B.X) {Z : C} (h : B.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp f B.inv)) (CategoryTheory.CategoryStruct.comp B.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp B.one h)

theorem Grp_.lift_inv_comp_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp_ C} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f.hom (CategoryTheory.CategoryStruct.comp A.inv f.hom)) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A.X) B.one

theorem Grp_.lift_inv_comp_right_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp_ C} (f : A ⟶ B) {Z : C} (h : B.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f.hom (CategoryTheory.CategoryStruct.comp A.inv f.hom)) (CategoryTheory.CategoryStruct.comp B.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A.X) (CategoryTheory.CategoryStruct.comp B.one h)

@[simp]

theorem Grp_.lift_comp_inv_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f : A ⟶ B.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f B.inv) f) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A) B.one

@[simp]

theorem Grp_.lift_comp_inv_left_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f : A ⟶ B.X) {Z : C} (h : B.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f B.inv) f) (CategoryTheory.CategoryStruct.comp B.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A) (CategoryTheory.CategoryStruct.comp B.one h)

theorem Grp_.lift_inv_comp_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp_ C} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp A.inv f.hom) f.hom) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A.X) B.one

theorem Grp_.lift_inv_comp_left_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp_ C} (f : A ⟶ B) {Z : C} (h : B.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp A.inv f.hom) f.hom) (CategoryTheory.CategoryStruct.comp B.mul h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A.X) (CategoryTheory.CategoryStruct.comp B.one h)

theorem Grp_.eq_lift_inv_left {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp g B.inv) h) B.mul ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g f) B.mul = h

theorem Grp_.lift_inv_left_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f B.inv) g) B.mul = h ↔ g = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h) B.mul

theorem Grp_.eq_lift_inv_right {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) : f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g (CategoryTheory.CategoryStruct.comp h B.inv)) B.mul ↔ CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f h) B.mul = g

theorem Grp_.lift_inv_right_eq {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} (f g h : A ⟶ B.X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CategoryStruct.comp g B.inv)) B.mul = h ↔ f = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift h g) B.mul

theorem Grp_.lift_left_mul_ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A : C} {B : Grp_ C} {f g : A ⟶ B.X} (i : A ⟶ B.X) (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f i) B.mul = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g i) B.mul) : f = g

@[simp]

theorem Grp_.inv_comp_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : CategoryTheory.CategoryStruct.comp A.inv A.inv = CategoryTheory.CategoryStruct.id A.X

@[simp]

theorem Grp_.inv_comp_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) {Z : C} (h : A.X ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inv (CategoryTheory.CategoryStruct.comp A.inv h) = h

instance Grp_.instIsIsoInv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : CategoryTheory.IsIso A.inv

@[simp]

theorem Grp_.inv_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : CategoryTheory.inv A.inv = A.inv

For inv ≫ inv = 𝟙 see inv_comp_inv.

theorem Grp_.mul_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Grp_ C) : CategoryTheory.CategoryStruct.comp A.mul A.inv = CategoryTheory.CategoryStruct.comp (β_ A.X A.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom A.inv A.inv) A.mul)

theorem Grp_.mul_inv_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Grp_ C) {Z : C} (h : A.X ⟶ Z) : CategoryTheory.CategoryStruct.comp A.mul (CategoryTheory.CategoryStruct.comp A.inv h) = CategoryTheory.CategoryStruct.comp (β_ A.X A.X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom A.inv A.inv) (CategoryTheory.CategoryStruct.comp A.mul h))

@[simp]

theorem Grp_.tensorHom_inv_inv_mul {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Grp_ C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom A.inv A.inv) A.mul = CategoryTheory.CategoryStruct.comp (β_ A.X A.X).hom (CategoryTheory.CategoryStruct.comp A.mul A.inv)

@[simp]

theorem Grp_.tensorHom_inv_inv_mul_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] (A : Grp_ C) {Z : C} (h : A.X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom A.inv A.inv) (CategoryTheory.CategoryStruct.comp A.mul h) = CategoryTheory.CategoryStruct.comp (β_ A.X A.X).hom (CategoryTheory.CategoryStruct.comp A.mul (CategoryTheory.CategoryStruct.comp A.inv h))

def Grp_.mulRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A.X) : A.X ≅ A.X

The map (· * f).

Equations

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

@[simp]

theorem Grp_.mulRight_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A.X) : (A.mulRight f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A.X) f)) A.mul

@[simp]

theorem Grp_.mulRight_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) (f : CategoryTheory.MonoidalCategoryStruct.tensorUnit C ⟶ A.X) : (A.mulRight f).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id A.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.toUnit A.X) (CategoryTheory.CategoryStruct.comp f A.inv))) A.mul

@[simp]

theorem Grp_.mulRight_one {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : A.mulRight A.one = CategoryTheory.Iso.refl A.X

theorem Grp_.isPullback {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : CategoryTheory.IsPullback (CategoryTheory.MonoidalCategoryStruct.whiskerRight A.mul A.X) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A.X A.X A.X).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A.X A.mul)) A.mul A.mul

The associativity diagram of a group object is cartesian.

In fact, any monoid object whose associativity diagram is cartesian can be made into a group object (we do not prove this in this file), so we should expect that many properties of group objects follow from this result.

@[simp]

theorem Grp_.inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp_ C} (f : A ⟶ B) : CategoryTheory.CategoryStruct.comp A.inv f.hom = CategoryTheory.CategoryStruct.comp f.hom B.inv

Morphisms of group objects preserve inverses.

@[simp]

theorem Grp_.inv_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp_ C} (f : A ⟶ B) {Z : C} (h : B.X ⟶ Z) : CategoryTheory.CategoryStruct.comp A.inv (CategoryTheory.CategoryStruct.comp f.hom h) = CategoryTheory.CategoryStruct.comp f.hom (CategoryTheory.CategoryStruct.comp B.inv h)

theorem IsMon_Hom.inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X Y : C} [Grp_Class X] [Grp_Class Y] (f : X ⟶ Y) [IsMon_Hom f] : CategoryTheory.CategoryStruct.comp Grp_Class.inv f = CategoryTheory.CategoryStruct.comp f Grp_Class.inv

theorem IsMon_Hom.inv_hom_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X Y : C} [Grp_Class X] [Grp_Class Y] (f : X ⟶ Y) [IsMon_Hom f] {Z : C} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp Grp_Class.inv (CategoryTheory.CategoryStruct.comp f h) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp Grp_Class.inv h)

theorem Grp_Class.toMon_Class_injective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} : Function.Injective (@toMon_Class C inst✝ inst✝¹ X)

theorem Grp_Class.ext {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} (h₁ h₂ : Grp_Class X) (H : toMon_Class = toMon_Class) : h₁ = h₂

theorem Grp_Class.ext_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {X : C} {h₁ h₂ : Grp_Class X} : h₁ = h₂ ↔ toMon_Class = toMon_Class

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

The forgetful functor from group objects to monoid objects.

Equations

• Grp_.forget₂Mon_ C = CategoryTheory.inducedFunctor Grp_.toMon_

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

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

Equations

• Grp_.fullyFaithfulForget₂Mon_ C = CategoryTheory.fullyFaithfulInducedFunctor Grp_.toMon_

instance Grp_.instFullMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (forget₂Mon_ C).Full

instance Grp_.instFaithfulMon_Forget₂Mon_ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (forget₂Mon_ C).Faithful

@[simp]

theorem Grp_.forget₂Mon_obj_one (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : ((forget₂Mon_ C).obj A).one = A.one

@[simp]

theorem Grp_.forget₂Mon_obj_mul (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] (A : Grp_ C) : ((forget₂Mon_ C).obj A).mul = A.mul

@[simp]

theorem Grp_.forget₂Mon_map_hom (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {A B : Grp_ C} (f : A ⟶ B) : ((forget₂Mon_ C).map f).hom = f.hom

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

The forgetful functor from group objects to the ambient category.

Equations

• Grp_.forget C = (Grp_.forget₂Mon_ C).comp (Mon_.forget C)

@[simp]

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

@[simp]

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

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

@[simp]

theorem Grp_.forget₂Mon_comp_forget (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] : (forget₂Mon_ C).comp (Mon_.forget C) = forget C

def Grp_.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : Grp_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) : M ≅ N

Constructor for isomorphisms in the category Grp_ C.

Equations

• Grp_.mkIso f one_f mul_f = (Grp_.fullyFaithfulForget₂Mon_ C).preimageIso (Mon_.mkIso f one_f mul_f)

@[simp]

theorem Grp_.mkIso_hom_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : Grp_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) : (mkIso f one_f mul_f).hom.hom = f.hom

@[simp]

theorem Grp_.mkIso_inv_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.CartesianMonoidalCategory C] {M N : Grp_ C} (f : M.X ≅ N.X) (one_f : CategoryTheory.CategoryStruct.comp M.one f.hom = N.one := by aesop_cat) (mul_f : CategoryTheory.CategoryStruct.comp M.mul f.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom f.hom) N.mul := by aesop_cat) : (mkIso f one_f mul_f).inv.hom = f.inv

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

Equations

• A.uniqueHomFromTrivial = A.uniqueHomFromTrivial

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

noncomputable def CategoryTheory.Functor.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] : Functor (Grp_ C) (Grp_ D)

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

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_mul {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp_ C) : (F.mapGrp.obj A).mul = CategoryStruct.comp (LaxMonoidal.μ F A.X A.X) (F.map A.mul)

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_X {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp_ C) : (F.mapGrp.obj A).X = F.obj A.X

@[simp]

theorem CategoryTheory.Functor.mapGrp_map_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] {X✝ Y✝ : Grp_ C} (f : X✝ ⟶ Y✝) : (F.mapGrp.map f).hom = F.map f.hom

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_inv {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp_ C) : (F.mapGrp.obj A).inv = F.map A.inv

@[simp]

theorem CategoryTheory.Functor.mapGrp_obj_one {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : Functor C D) [F.Monoidal] (A : Grp_ C) : (F.mapGrp.obj A).one = CategoryStruct.comp (LaxMonoidal.ε F) (F.map A.one)

noncomputable def CategoryTheory.Functor.mapGrpIdIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] : (Functor.id C).mapGrp ≅ Functor.id (Grp_ C)

The identity functor is also the identity on group objects.

Equations

• CategoryTheory.Functor.mapGrpIdIso = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (CategoryTheory.Iso.refl ((CategoryTheory.Functor.id C).mapGrp.obj X).X) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.mapGrpIdIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : Grp_ C) : (mapGrpIdIso.hom.app X).hom = CategoryStruct.id X.X

@[simp]

theorem CategoryTheory.Functor.mapGrpIdIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] (X : Grp_ C) : (mapGrpIdIso.inv.app X).hom = CategoryStruct.id X.X

noncomputable def CategoryTheory.Functor.mapGrpCompIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] {F : Functor C D} [F.Monoidal] {G : Functor D E} [G.Monoidal] : (F.comp G).mapGrp ≅ F.mapGrp.comp G.mapGrp

The composition functor is also the composition on group objects.

Equations

• CategoryTheory.Functor.mapGrpCompIso = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (CategoryTheory.Iso.refl ((F.comp G).mapGrp.obj X).X) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.mapGrpCompIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] {F : Functor C D} [F.Monoidal] {G : Functor D E} [G.Monoidal] (X : Grp_ C) : (mapGrpCompIso.inv.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

@[simp]

theorem CategoryTheory.Functor.mapGrpCompIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {E : Type u₃} [Category.{v₃, u₃} E] [CartesianMonoidalCategory E] {F : Functor C D} [F.Monoidal] {G : Functor D E} [G.Monoidal] (X : Grp_ C) : (mapGrpCompIso.hom.app X).hom = CategoryStruct.id (G.obj (F.obj X.X))

noncomputable def CategoryTheory.Functor.mapGrpNatTrans {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F F' : Functor C D} [F.Monoidal] [F'.Monoidal] (f : F ⟶ F') : F.mapGrp ⟶ F'.mapGrp

Natural transformations between functors lift to group objects.

Equations

• CategoryTheory.Functor.mapGrpNatTrans f = { app := fun (X : Grp_ C) => { hom := f.app X.X, one_hom := ⋯, mul_hom := ⋯ }, naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.mapGrpNatTrans_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F F' : Functor C D} [F.Monoidal] [F'.Monoidal] (f : F ⟶ F') (X : Grp_ C) : ((mapGrpNatTrans f).app X).hom = f.app X.X

noncomputable def CategoryTheory.Functor.mapGrpNatIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F F' : Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') : F.mapGrp ≅ F'.mapGrp

Natural isomorphisms between functors lift to group objects.

Equations

• CategoryTheory.Functor.mapGrpNatIso e = CategoryTheory.NatIso.ofComponents (fun (X : Grp_ C) => Grp_.mkIso (e.app X.X) ⋯ ⋯) ⋯

@[simp]

theorem CategoryTheory.Functor.mapGrpNatIso_hom_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F F' : Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : Grp_ C) : ((mapGrpNatIso e).hom.app X).hom = e.hom.app X.X

@[simp]

theorem CategoryTheory.Functor.mapGrpNatIso_inv_app_hom {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F F' : Functor C D} [F.Monoidal] [F'.Monoidal] (e : F ≅ F') (X : Grp_ C) : ((mapGrpNatIso e).inv.app X).hom = e.inv.app X.X

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

mapGrp is functorial in the left-exact functor.

Equations

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

@[simp]

theorem CategoryTheory.Functor.mapGrpFunctor_obj {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (F : C ⥤ₗ D) : mapGrpFunctor.obj F = F.obj.mapGrp

@[simp]

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

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

An adjunction of monoidal functors lifts to an adjunction of their lifts to group objects.

Equations

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

@[simp]

theorem CategoryTheory.Adjunction.mapGrp_unit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.Monoidal] : a.mapGrp.unit = CategoryStruct.comp Functor.mapGrpIdIso.inv (CategoryStruct.comp (Functor.mapGrpNatTrans a.unit) Functor.mapGrpCompIso.hom)

@[simp]

theorem CategoryTheory.Adjunction.mapGrp_counit {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] {F : Functor C D} {G : Functor D C} (a : F ⊣ G) [F.Monoidal] [G.Monoidal] : a.mapGrp.counit = CategoryStruct.comp Functor.mapGrpCompIso.inv (CategoryStruct.comp (Functor.mapGrpNatTrans a.counit) Functor.mapGrpIdIso.hom)

noncomputable def CategoryTheory.Equivalence.mapGrp {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] : Grp_ C ≌ Grp_ D

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

Equations

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

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_inverse {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] : e.mapGrp.inverse = e.inverse.mapGrp

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_counitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] : e.mapGrp.counitIso = Functor.mapGrpCompIso.symm ≪≫ Functor.mapGrpNatIso e.counitIso ≪≫ Functor.mapGrpIdIso

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_functor {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] : e.mapGrp.functor = e.functor.mapGrp

@[simp]

theorem CategoryTheory.Equivalence.mapGrp_unitIso {C : Type u₁} [Category.{v₁, u₁} C] [CartesianMonoidalCategory C] {D : Type u₂} [Category.{v₂, u₂} D] [CartesianMonoidalCategory D] (e : C ≌ D) [e.functor.Monoidal] [e.inverse.Monoidal] : e.mapGrp.unitIso = Functor.mapGrpIdIso.symm ≪≫ Functor.mapGrpNatIso e.unitIso ≪≫ Functor.mapGrpCompIso